The Eiffel Compiler / Interpreter (tecomp)
Inductive types are very powerful because they allow to write recursively defined functions which are guaranteed to terminate and to reason about them by induction. Recursively defined functions an proofs by induction are closely related. As an introductory example we use the class
case class UNARY_NATURAL create zero succ(pred: UNARY_NATURAL) feature plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end end
and assume that we want to prove the assertion
all(a) zero + a = a
We can proof this assertion informally with the following argument.
The assertion is obviously true if "a" has been created with the creator "zero". The definition of "plus" says in the first case clause that "anything+zero" yields "anything" and this anything might be "zero" as well.
Now let us consider the case that "a" has been created with "succ" and that the assertion is valid for the predecessor of "a", i.e. we have the assumptions
-- "a" has been created by the creator "succ" zero + a.pred = a.pred -- induction hypothesis
Now we prove the assertion "zero+a=a" under these premises. If "a" has been created with "succ" the second case clause of the definition of "plus" tells us
zero + a = succ(zero+a.pred)
From our assumption we know that "zero+a.pred=a.pred. We can use this fact to derive
zero + a = succ(a.pred)
The expression "succ(a.pred)" must be equivalent to "a" and this gives us
zero + a = a
which is identical to our assertion to be proved.
This "inductive" reasoning is possible because and UNARY_NATURAL is an inductive type. If we do not yet have an object of UNARY_NATURAL the only way to construct one is to use the "zero" creator. If we already have a UNARY_NATURAL (say "n") we can use the creator "succ" to create "succ(n)". Then if "zero" satisfies a certain property and every number "n" carries over this property to its successor "succ(n)" then we conclude that the property is valid for all number constructed in this manner.
Modern Eiffel's proof engine supports inductive proofs like the one informally described. The following chapter prepares the basic machinery which enable us to do inductive proofs efficiently using the proof engine. It explains how we state that some object has been constructed in a certain manner, what equality means for inductive types and which rewrites are allowed, how we satisfy preconditions to access an attribute and how we do proofs by induction.
The class UNARY_NATURAL is not efficient to do arithmetics. Nobody should do actual calculations in a program using this class. However it is an excellent vehicle to model natural numbers and demonstrate the basic reasoning techniques.
The basic reasoning techniques which rely on inductive data types are best explained with simple examples. In addition to the type UNARY_NATURAL we use the types COLOR, OPTIONAL[G] and EMPTY to explain the basic rules and the techniques.
case class COLOR create red green blue end
case class OPTIONAL[G] create none value(value:G) end
case class EMPTY end
The class OPTIONAL is a generic class which takes one type parameter. This generic class can construct e.g. the type OPTIONAL[CHARACTER]. Objects of type OPTIONAL[CHARACTER] have no value if they have been created with "none" or have a value of type CHARACTER if they have been created with "value('a')".
Note that feature names in Modern Eiffel need not be unique. The class OPTIONAL has two features, a creator named "value" and an attribute named "value". These two features have different signatures. The creator takes one argument and the attribute returns a value. In Modern Eiffel the feature name together with the signature must uniquely address a feature.
The class EMPTY has no creator. Therefore it is not possible to create objects of this type.
An object of inductive type is immutable, i.e. its value is fixed at creation time and cannot be changed. We need a way to express the fact that an object attached to a variable has been created with a certain creator. E.g. for a UNARY_NATURAL "a" we want to make statements like "a has been created with the zero creator" or "a has been created with the succ creator". This is expressed in Modern Eiffel as a match expression.
a as zero -- a has been created with "zero" a as succ(_) -- a has been created with "succ" a as succ(succ(_)) -- a has been created by double application of "succ"
We use the anonymous variable "_" to express that we are not interested in the value of the argument. "a as succ(_)" expresses the fact that "a" has been constructed with the creator "succ" with some argument.
Match expressions are boolean expressions. We can combine them with boolean operators
not (a as zero) not (a as succ(_) a as zero and b as succ(_)
The opterator "as" has the same precedence as the relational operators "=", "<=", ... I.e. it has higher precedence than "and", "or", ... and lower precedence than "not".
For immutable type objects equality is a rather strong property. If two immutable type objects "o1" and "o2" are equal, i.e. "o1=o2" or "o1.is_equal(o2)" then they are indistiguishable. There is no construct in Modern Eiffel to distinguish two instances of an immutable type object if they are equal.
This means that immutable type objects are treated like numbers. E.g. the number "5" is always the number "5" and has the same properties (e.g. "5" is a prime number) regardless where it is stored.
We say that immutable type objects do not have identity.
Mutable type objects have an identity. We can build a mutable type which models a car. Two instances of CAR are different objects even if they are equal. E.g. you can have a car which is equal to your neighbour's car. Both cars are from the same car company, are the same model, have the same color, have the same extras. But they are different cars. They are mutable, because their state can change, e.g. their velocity. Changes of the state of one does not change the state of the other. As opposed to this there is no way to change the number "5". It is possible to assign to a variable a different number, but the number cannot change.
We need two different operators to express these different concepts. The equality operator "=" expresses equality and the identity operator "~" expresses identity. Of course identity implies equality. An object is always equal to itself.
Here we discuss objects of inductive types. An inductive type is an immutable type and for immutable types there is no difference between equality and identity. The identity of an immutable type object is its value. I.e. equality implies identity (which is not true for mutable objects).
Whenever we have two expression "e1" and "e2" of immutable type we can substitute one for the other. This property is called referentially transparency. Expressions returning immutable type objects are referentially transparent.
In order to exploit the property that two equal objects of immutable type are indistinguishable we introduce the command "rewrite(e1,e2)". E.g.
-- state before: x=y, ... : 2+x=2*y rewrite(x,y) -- state after: x=y, ... : 2+y=2*y
If the proof engine encounters the command "rewrite(e1,e2)" it checks whether the type of "e1" and "e2" is an immutable type and if the equality "e1=e2" is either on the assumption stack or it it matches an already proved assertion. If yes, it substitutes within the current goal all expressions of the form "e1" by the expression "e2".
If the type of "e1" and "e2" is mutable, then it searches for a match of "e1~e2" instead of "e1=e2".
The rewrite command can have more than two arguments. The command "rewrite(e1,e2,e3,...)" is semantically equivalent to the sequence of commands "rewrite(e1,e2); rewrite(e2,e3); ...".
In many cases the rewrite command does not encounter a match for "e1=e2" but a match for "a=>(e1=e2)" (or a cascaded implication like "a=>b=>...=>(e1=e2)"). In this case the proof engine loads all premises "a", ... onto the goal stack and issues for each of them a "remove" and then does the rewriting of the current goal.
Equalities are expressed by the equality operator "=" and inequalities are expressed by the inequality operator "/=". The expression "a/=b" is a shorthand for "not (a=b)".
Two objects of inductive type are equal if and only if
Furthermore inductive types are constructive.
There must be at least one basic creator to create "first" objects of this type. A basic creator either doesn't have arguments (like "zero" in the type UNARY_NATURAL) or has arguments of objects which are not based on objects of the same inductive type.
Then there might be recursive creators (like "succ") which involve other objects of the same type. These creators create an object which is different from all objects involved in its construction.
I.e. it is not possible to have any cycles in the process of object creation.
The attributes of the objects are identical to the corresponding arguments of the creators.
These rules can be summarized by the following assertions (here for the example UNARY_NATURAL).
different_creator: succ(x) /= zero injection: x /= succ(x) equal_intro: x=y => succ(x)=succ(y) equal_elim: succ(x)=succ(y) => x=y reconstruction: x = succ(x.pred) retrieval: x = succ(x).pred
The proof engine uses these assertions as axioms. I.e. the command "remove" can discharge goals which match the above equalities or inequalities and the command "premise" can exploit the above implications.
The general case where "c", "c1", "c2", ... are different creators looks like
different_creator: c1(...) /= c2(...) injection: a /= c1(a,...) equal_intro: a1~b1 => a2~b2 => c(a1,a2,...)=c(b1,b2,...) equal_elim: c(a1,a2,...)=c(b1,b2,...) => a1~b1 reconstruction a = c(a.attr1, a.attr2, ...) retrieval a ~ c(a,b,...).attr1
In the general case some of the arguments of the creators might be mutable type objects. For these types the corresponding identities are guaranteed. Remember that for immutable type objects there is no difference between equality and identity.
An attribute of an object of inductive type is available only if the object has been constructed with a creator which introduced the attribute.
The attribute "value" of an object of type OPTIONAL[CHARACTER] can be accessed only if the object has been created with the creator "value". If the object has been created with "none", then the attribute "value" does not exist, i.e. cannot be accessed.
A similar condition applies to an object of type UNARY_NATURAL. The attribute "pred" (the predecessor) can be accessed only if the number has been created with the creator "succ". For a number created with "zero" the attribute "pred" is not accessible.
I.e. the access of an attribute has a precondition.
a,b: UNARY_NATURAL o: OPTIONAL[UNARY_NATURAL] -- expression precondition(s) o.value o as value(_) a.pred a as succ(_) a.pred=b a as succ(_) o.value=a.pred o as value(_), a as succ(_)
The above expressions can be combined to form boolean expressions. All binary boolean operators are short circuited. Therefore the following rules apply:
-- expression precondition(s) o=none and a=b.pred o=none => b as succ(_) o.value=a and a=b.pred o as value(_), o.value=a => b as succ(_) o.value=a => a=b.pred o as value(_), o.value=a => b as succ(_) o=none or a=b.pred o/=none => b as succ(_)
In the general case we get the preconditions:
-- assumptions: -- expression e has preconditions e_p1, e_p2, ... -- e1 has preconditions e1_p1, e1_p2, ... -- e2 has preconditions e1_p1, e1_p2, ... -- function f has preconditions f_p1, f_p2, ... -- expression precondition(s) f(e) e_p1, e_p2,..., f_p1(e), f_p2(e),... e1 => e2 e1_p1, e1_p2,..., e1=>e2_p1, e1=>e2_p2,... e1 and e2 e1_p1, e1_p2,..., e1=>e2_p1, e1=>e2_p2,... e1 or e2 e1_p1, e1_p2,..., not e1 => e2_p1, not e1 => e2_p2,...
An assertion to be proved is an expression which might have preconditions according to the above defined rules. If the proof engine enters a proof of an assertion "ass" with preconditions it does the following.
This rule requires that all preconditions of an assertion must be provable with "resolve". The programmer has to make sure that this is possible by providing enough assertions as lemmas.
The function "plus" within the class UNARY_NATURAL is defined recursively as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end
Keep in mind that Modern Eiffel is object oriented, i.e. if "a" and "b" are variables of type UNARY_NATURAL, then the two expressions
a.plus(b) a + b
are equivalent because the operator "+" has been defined to be an alias for the feature named "plus". The special entity "Current" describes the current object (like "this", "self", ... in other object oriented languages). The inspect expression inspects how "o" has been created. There has to be a case clause for each possible creator.
The first case clause applies if "o" has been created with the "zero" creator. The second case clause applies if "o" has been created with the "succ" creator. Since "succ" requires one argument, the fresh variable "p" is introduced to describe the predecessor of the newly created object.
Due to the nature of inductive types the compiler can check that the case clauses are exhaustive. Furthermore the compiler can check that the recursion does indeed terminate. It does this check in verifying that each recursive call has at least one "decreasing" argument. In this case the second argument is decreasing because it is called with the predecessor of "o" in the recursive branch.
The following two case clauses are equivalent:
case succ(p) then succ(Current+p) -- is equivalent to case succ(_) then succ(Current+o.pred)
The first form is usually preferable. Remember that the expression "succ(Current+o.pred)" has according to the above described rule the precondition "o as succ(_)". Since the case clause is only entered if the precondition is valid, the whole inspect expression is valid.
The definition of the function "plus" is an equality. We can give an equivalent definition which makes this fact more transparent.
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL ensure Result = inspect o case zero then Current case succ(p) then succ(Current+p) end end
The local variable "Result" represents the expression "Current+o" or "Current.plus(o)".
In the first case "Result" is equal to "Current" and in the second case it is equal to "succ(Current+o.pred)". I.e. we can rewrite the definition as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL ensure o as zero => (Result = Current) o as succ(_) => (Result = succ(Current+o.pred)) end
If we abstract this definition even more we get
all(a,b:UNARY_NATURAL) check a+zero = a b as succ(_) => a+b = succ(a+b.pred) end
The last form describes how the proof engine views this function definition. Therefore the proof engine allows the command "rewrite(a+zero,a)" for any variable "a". Furthermore command "rewrite(a+b, succ(a+b.pred))" is allowed by the proof engine if it can discharge "b as succ(_)" immediately by "remove" (this is possible if "b as succ(_)" is already on the assumption stack).
The proof engine creates for each inductive type and induction principle.
Let us look at the example COLOR. An object of type COLOR can be constructed only with one of the three constructors "red", "green" or "blue". If we want to proof an assertion of the form
it is sufficient to prove "f(c)" for each possible construction of "c". For the type COLOR the proof engine derives the induction principle
all(e:BOOLEAN) e[c:=red] => e[c:=green] => e[c:=blue] => all(c:COLOR) e
where e[x:=exp] is the expression obtained by substituting within "e" all free occurrences of the variable "x" by the expression "exp".
With this principle we can start a proof like
all(c:COLOR) f(c) proof induction(f(red), f(green), f(blue)) ... end
The command "induction" like the command "premise" replaces the curent goal by its premises according to the derived induction principle.
For the type OPTIONAL[G] the following induction principle is generated
all(e:BOOLEAN) e[o:=none] => (all(o:OPTIONAL[G]) o as value(_) => e) => all(o:OPTIONAL[G]) e
This allows us to start a proof as
all(o:OPTINAL[CHARACTER]) f(o) proof induction( f(none), all(o:OPTIONAL[G]) o as value(_) => f(o) ) ... end
The principle should be clear. If we want to prove a universally quantified assertion of the form "all(x:T) f(x)" we have to proof one premise for each creator. If the creator is argumentless then the variable is substituted by the creator. If the creator has arguments then a universally quantified premise is generated with an implication. The implication has as its premise that the value has been constructed with the specific creator.
What induction principle is generated for the type EMPTY? The type EMPTY has no creators, i.e. there are no premises. This corresponds to the fact that we cannot create an object of type EMPTY because we have no creator. No creator means no premise. Therefore the induction principle looks like
all(e:BOOLEAN) all(u:EMPTY) e
which basically says that "e" is valid for all objects of type EMPTY. But since there are no objects of type EMPTY, this principle cannot be used to actually prove anything (unless we achieve the impossible and create an object of type EMPTY!).
The generated induction principle gets interesting if the inductive type is recursive. For the type UNARY_NATURAL the proof engine generates the induction principle
all(e:BOOLEAN) e[n:=zero] => (all(n:UNARY_NATURAL) n as succ(_) => e[n:=n.pred] -- induction hypothesis => e ) => all(n:UNARY_NATURAL) e
with a possible proof template
all(n:UNARY_NATURAL) f(n) proof induction( f(zero), all(n) n as succ(_) => f(n.pred) => f(n) ) ... end
As opposed to the induction principles for COLOR, OPTIONAL, etc. this induction principle has an induction hypothesis which gives us more context when shifted onto the assumption stack.
The induction principle states:
If a statement is true for the number "zero" and every number carries the truth of the statement over to its successor, then the statement is true for all numbers.
In this chapter we focus on the type UNARY_NATURAL. It is defined like
case class UNARY_NATURAL create zero succ(pred:UNARY_NATURAL) feature -- functions ... -- properties ... end
The function "plus" is defined as
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then Current case succ(p) then succ(Current+p) end
We first prove that zero is a right neutral element of addition.
all(a:UNARY_NATURAL) check a + zero = a proof rewrite(a+zero,a); remove end end
The rewrite command is justified by the non recursive branch of the inspect expression. If the second operand in the addition is "zero" then the result is the first operand.
The proof "zero is left neutral" requires a proof by induction.
all(a:UNARY_NATURAL) zero + a = a proof induction( zero+zero=zero, all(a) a as succ(_) => zero+a.pred=a.pred => zero+a=a ) rewrite(zero+zero,zero); remove enter(3) rewrite( zero+a, succ(zero+a.pred), -- definition of "plus" succ(a.pred) ) -- induction hypothesis remove -- reconstruction end
The initial step requires us to proof that "zero+a=a" is valid if we substitute "a" by zero. A simple rewrite based on the nonrecursive branch of the definition of "plus" let us remove the goal.
The induction step requires us to prove that "zero+a=a" is valid under the assumption that "a" has been created with "succ" and the statement is already valid for the predecessor of "a".
Since "a" has been created with "succ" we can rewrite "zero+a" by "succ(zero+a.pred)" (based on the recursive branch of the definition of "plus"). Then we can rewrite this to "succ(a.pred)" based on the induction hypothesis. Based on the rules of equality we can discharge the remaining goal "succ(a.pred)=a" immediately by "remove".
Addition must be commutative. We can prove commutativity by induction. But the proof needs another assertion to work smoothly. First we have to prove the fact that "a+b=succ(a.pred+b)". This equality is needed for rewriting within the proof of commutativity.
all(a,b:UNARY_NATURAL) check lemma: a as succ(_) => a+b = succ(a.pred+b) proof generalize(b) induction( a as succ(_) => a+zero = succ(a.pred+zero), all(b) b as succ(_) => a as succ(_) => a+b.pred = succ(a.pred+b.pred) => a+b = succ(a.pred+b) ) rewrite(a.pred+zero,a.pred); rewrite(a+zero,a); remove enter(4) rewrite( a+b, succ(a+b.pred), -- definition "plus" succ(succ(a.pred+b.pred)), -- induction hypothesis succ(a.pred+b) ) -- definition "plus" end commutativiy: a+b = b+a proof generalize(a) induction( zero+b = b+zero, all(a) a as succ(_) => a.pred+b = b+a.pred => a+b = b+a ) rewrite(zero+b,b); rewrite(b+zero,b); remove enter(3) rewrite( b+a, succ(b+a.pred), -- definition "plus" succ(a.pred+b), -- induction hypothesis a+b ) -- lemma remove end end
The rewritings should be easy to follow. But I have used the not yet introduced command "generalize" which needs some explanation. Remember that we had already assertions of the form
all(x:X; y:Y; ...) check ass1 proof ... end ass2 proof ... end ... end
where the "check ... end" block had been used to group a number of assertions which needed the same variables. In Modern Eiffel this is just a shorthand for
all(x:X; y:Y; ...) ass1 proof enter(n) ... end all(x:X; y:Y; ...) ass2 proof enter(n) ... end ...
I.e. the assertions "ass1", "ass2" are treated as individual assertions each with its own quantifier. Remember also that an assertion of the form
is the implicit implication
"x has type X" => e
where the typing judgement can be shifted onto the assumption stack. If we prove an assertion within the "check ... end" block, all typing judgements of the surrounding quantifier have already been shifted onto the assumption stack. This means that the variables are now free variables.
However a proof by induction needs an assertion of the form "all(x:X) e". The command "generalize(x)" regeneralizes the assertion with respect to the variable "x", i.e. it puts an allquantor before the expression within the current goal. This generalization replaces the current goal with a stronger (or equivalent) goal.
The command "generalize(a,b,...)" is equivalent to "...; generalize(b); generalize(a)". Therefore it gives us the possibility to reorder the variables within the allquantor.
The proof engine accepts the command "generalize" only for variables which already occur as free variables in the current goal.
In the following a proof of the associativity of "plus" is given.
all(a,b:UNARY_NATURAL) check lemma_1: b as succ(_) => (a+b) as succ(_) proof enter rewrite(a+b, succ(a+b.pred)) -- definition of "plus" remove -- match expression end lemma_2: b as succ(_) => a+b.pred = (a+b).pred proof enter premise(succ(a+b.pred) = succ((a+b).pred)) -- eq elim rewrite(succ(a+b.pred), a+b) -- definition of "+" rewrite(succ(a+b).pred, a+b) -- argument retrieval remove end associativity: a+b+c = a+(b+c) proof generalize(c) induction( a+b+zero = a+(b+zero) all(c) c as succ(_) => a+b+c.pred = a+(b+c.pred) => a+b+c = a+(b+c) ) resolve enter(3) rewrite( a+b+c, succ(a+b+c.pred), -- definition of "plus" succ(a+(b+c.pred)), -- induction hypothesis succ(a+(b+c).pred), -- lemma_2 a+(b+c) ) -- definition of "plus" remove end
Some comments to understand the proofs:
Multiplication is defined recursively as well.
times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then zero case succ(p) then Current*p + Current end
For multiplication we expect the following properties:
all(a,b,c,d: UNARY_NATURAL) check zero_1: a*zero = zero zero_2: zero*a = zero lemma: a+b+(c+d) = a+c + (b+c) distributivity: (a+b)*c = a*c + b*c end
all(a,b,c: UNARY_NATURAL) check lemma_1: a + b + c = a + c + b lemma_2: b as succ(_) => b.pred*a+a = b*a commutativity: a*b = b*a -- hint use definition of "*" and "+" before -- using the induction hypothesis end
The proof of these properties is left as an excercise to the reader. It is not difficult to perform these proofs.
Sometimes it is difficult to find the needed lemmas to proof an expected law. If one starts e.g. to prove distributivity without the mentioned lemmas an induction proof soon gets stuck because one cannot make some necessary rewriting. The best thing to do is to state the lemma which allows the rewriting and see if it is possible to complete the proof. Then of course the lemma has to be proved as well which might need other lemmas to support the proof.
It is not recommended to try nested proofs by induction. It is possible to perform nested proofs but one gets lost easily.
We introduced the basic reasoning techniques for inductive types.
Inductive types have special axioms for equality. The commands "remove" and "premise" are powerful enough to exploit this properties. Furthermore term rewriting can be done based on equality.
Inductive types have attributes which might have preconditions. The proof engine verifies that all preconditions are valid.
For each inductive type an induction principle is generated by the proof engine. The additional commands "generalize" and "induction" have been introduced to perform proofs by induction.
all(a:UNARY_NATURAL) check zero_1: a*zero = zero proof rewrite(a*zero,zero); remove end zero_2: zero*a = zero proof generalize(a) induction( zero*zero=zero, all(a) a as succ(_) => zero*a.pred=zero => zero*a=zero ) resolve enter(2) rewrite( zero*a, zero*a.pred + zero, zero*a.pred, zero ) remove end end
all(a,b,c,d: UNARY_NATURAL) check lemma: a+b+(c+d) = a+c + (b+c) proof rewrite( a+b+(c+d), a+b+c+d, a+(b+c)+d, a+(c+b)+d, a+c+b+d, a+c + (b+d) ) remove end distributivity: (a+b)*c = a*c + b*c proof generalize(c) induction( (a+b)*zero = a*zero + b*zero, all(c) c as succ(_) => (a+b)*c.pred = a*c.pred + b*c.pred => (a+b)*c = a*c + b*c ) resolve enter(3) rewrite( (a+b)*c, (a+b)*c.pred + (a+b), a*c.pred+b*c.pred + (a+b), a*c.pred+a + (b*c.pred+b), a*c + b*c ) remove end end
all(a,b,c: UNARY_NATURAL) check lemma_1: a + b + c = a + c + b proof rewrite( a+b+c, a+(b+c), a+(c+b), a+c+b ) end lemma_2: b as succ(_) => b.pred*a+a = b*a proof generalize(a) induction( b as succ(_) => b.pred*zero+zero = b*zero, all(a) a as succ(_) => (b as succ(_) => b.pred*a.pred+a.pred = b*a.pred) => b as succ(_) => b.pred*a+a = b*a ) resolve enter(4) rewrite( b.pred*a + a, b.pred*a.pred + b.pred + a, succ(b.pred*a.pred + b.pred + a.pred), -- def "+" succ(b.pred*a.pred + a.pred + b.pred), -- lemma_1 succ(b*a.pred + b.pred), -- induction hypothesis b*a.pred+b, -- def "+" b*a ) -- def "*" end commutativity: a*b = b*a proof generalize(b) induction( a*zero = zero*a all(b) b as succ(_) => a*b.pred = b.pred*a => a*b = b*a ) resolve enter(3) rewrite( a*b, a*b.pred+a, b.pred*a+a, b*a ) remove end end
Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: