The Eiffel Compiler / Interpreter (tecomp)

This article describes the use of quantified expressions and laws for quantified expressions. All the axioms and proved assertion belong to the class BOOLEAN, because only pure logic is involved.

Quantified expressions model some logic which is deeply rooted in our thinking. A universal quantification and its consequence can be expressed in the form of syllogisms.

"All humans are mortal." all(x:HUMAN) x.is_mortal "Sokrates is a human." sokrates:HUMAN -- therefore "Sokrates is mortal." sokrates.is_mortal

A similar example can be stated to express existential quantification.

"Sokrates is mortal." sokrates.is_mortal -- therefore "There exists a human which is mortal." some(x:HUMAN) x.is_mortal

We are able to reason with existential and universal quantification like

-- If "There is a human which is mortal" some(x:HUMAN) x.is_mortal -- and "All mortal humans are not eternal" all(x:HUMAN) x.is_mortal => not x.is_eternal -- then "There is a human which is not eternal" some(x:HUMAN) not x.is_eternal

Another form of reasoning is quite common

-- If "Not all cats are black" not all(c:CAT) c.is_black -- Then "There is some cat which is not black" some(c:CAT) not c.is_black -- If "All cats have four legs" all(c:CAT) c.leg_count=4 -- Then "There is no cat with not four legs" not some(c:CAT) not (c.leg_count=4)

The formalization of the above examples leads to predicate logic with quantified expressions. The following chapters give the basic rules, the axioms and some usful laws to deal with quantified expressions within programs.

Quantified expressions have the general form

all(x:T) e some(x:T) e

with the semantics that all objects of a certain type satisfy a certain property or there exists some object of a certain type which satisfies a certain property.

The variable "x" is called a bound variable, because it is valid only in the context of the quantified expression. The expression "e" usually contains the bound variable.

The name of the bound variable is not relevant. We can choose any name. However if we choose another name, we have to use the other name in the expression e as well.

(all(x:T) e) = all(y:T) e[x:=y] (some(x:T) e) = some(y:T) e[x:=y]

Note the need of parentheses in the above expressions because a quantified expression spans to the right as far as possible.

It is necessary that the renaming does not change the semantics of the expression. If the variable "y" already occurs within "e" then the above renaming is invalid. I.e. the renamed variable must be a fresh variable (a name which does not yet occur within the expression).

Valid assertions of the form

all(x:T) e

can be used to generate valid expressions by substituting the bound variable "x" by any expression of type "T". Suppose we have the general law

law: all(a,b:BOOLEAN) a => b => a and b

and we are in a context where "i" and "j" are variables of type NATURAL. Then we can use the above law to generate the valid assertion

```
ass: i<=j => i/=j => i<=j and i/=j
```

We have generated this valid assertion by the substitution

(a => b => a and b)[a,b:=i<=j,i/=j]

We say that the assertion "ass" matches the assertion "law". In general we say that an assertion "p" matches another assertion "q" if both assertions are identical or if "q" is a quantifed expression with the universal quantifier and there is a valid substitution for the bound variables of "q" which converts the expression within "q" into "p".

The expression

e[x,y,...:=xexp,yexp,...]

Is the expression "e" where all free ocurrences of "x,y,..." have been substituted by "xexp,yexp,...". The substitution is defined recursively by

-- x,y: variables -- a,b: arbitrary expressions -- unop: a unary operator -- binop: a binary operator -- f: n-ary function x[x:=xexp] = xexp y[x:=xexp] = y[x:=exp] (unop a)[x:=xexp] = unop a[x:=xexp] (a binop b)[x:=xexp] = a[x:=xexp] binop b[x:=xexp] f(a,b,...)[x:=xexp] = f(a[x:=xexp],b[x:=xexp],...)

Rule: The substitution "e[x,y,...:=xexp,yexp,...] is valid if and only if all variable occurring within "xexp,yexp,..." are not bound within "e". I.e. free variables must remain free and not captured within some internal scope.

Like generic classes, assertions can be generic as well. E.g. we can have

all[G](x:G) e all[G] some(x:G) e

which means that the assertions must be valid for any type "G". It is possible to constrain the types with

all[G:COMPARABLE](x:G) e all[G:COMPARABLE] some(x:G) e

with the meaning

"type G is COMPARABLE" => "x is of type G" => e "type G is COMPARABLE" => "there is some x of type G which satisfies e"

We can also write

some[G](x:G) e

with the obvious meaning

```
"There exists some type G and some x of type G which satisfies e"
```

The expression

all(x:X; y:Y) e

is a shorthand for

all(x:X) all(y:Y) e

Our intiuition tells us that we can exchange the universal quanitifiers. We can prove this by

(all(x:X) all(y:Y) e) => (all(y:Y) all(x:X) e) proof enter(3) -- all(x:X) all(y:Y) e -- y:Y -- x:X -- =================== -- e remove end

Since the proof contains just trivial steps the proof engine can proof this assertion automatically.

The universal quantifier distributes over "and".

all[G](a,b:BOOLEAN) check (all(x:G) a and b) => all(x:G) a proof enter(2) premise(a and b) remove end (all(x:G) a and b) => all(x:G) b proof enter(2); premise(a and b); remove end (all(x:G) a) => (all(x:G) b) => all(x:G) a and b proof enter(3) premise(a,b) remove(2) end (all(x:G) a and b) = ((all(x:G) a) and (all(x:G) b)) proof resolve end end

Existential quantification is a general disjunction. Suppose there are objects "o1", "o2", "o3", of type T then we define "some(x) e" by

(some(x:T) e) = (e[x:=o1] or e[x:=o2] or e[x:o3] or ... )

How can we proof an existentially quantified assertion? Let us first ask: How do we proof a disjunction "a or b"? We prove "a or b" if we proof one of them. This is expressed in the two introduction rules of "or" (see article "Introduction into the proof engine"):

all(a,b:BOOLEAN) check or_intro1: a => a or b or_intro2: b => a or b end

The existential quantifier has a similar introduction rule (which is an axiom).

exist_intro: all[G](e:BOOLEAN) all(w:G) e[x:=w] => some(x:G) e proof axiom end

I.e. we can prove an existentially quantified expression if we find a witness for the bound variable. We can choose any witness we like, but we have to find one. The rule says: If we are in a context in which we have an expression "w" of type G which satisfies "e[x:=w"]" then we can conclude "some(x:G) e".

The introduction rule allows us to prove a goal which is an existentially quantified expression. But we need the other way round as well. We need to infer something from an assumption which is an existentially quantified expression. For "or" we have the elimination rule

all(a,b,g: BOOLEAN) or_elim: a or b => (a=>g) => (b=>g) => g

This rule says that in order to prove a goal "g" in a context in which "a or b" is true, it is sufficient to prove that the goal is a consequence of "a" and a consequence of "b". This rule allows us to make case split. If we know that "a or b" is true we prove the goal under both cases. We assume "a" and prove the goal and we assume "b" and prove the goal.

For existential quantification we have a similar elimination rule.

exist_elim: all[G](e:BOOLEAN) some(x:G) e => (all(x:G) e => g) => g proof axiom end

I.e. if we know that there is some "x" satisfying "e" and if all "x" which satisify "e" imply that g is valid, then we can conclude the validity of "g".

Since an existentially quantified expression is a generalized disjunction we expect that "exists" distributes over "or", i.e. we expect

all[G](a,b:BOOLEAN) check (some(x:G) a) => (some(x:G) a or b) (some(x:G) b) => (some(x:G) a or b) (some(x:G) a or b) => (some(x:G) a) or (some(x:G) b) end

to be valid.

We can prove these laws by

all[G](a,b:BOOLEAN) check (some(x:G) a) => (some(x:G) a or b) proof enter premise( some(x:G) a, all(w:G) a[x:=w] => some(x:G) a or b) remove enter(2) premise(a[x:=w] or b[x:=w]) premise(a[x:=w]) remove end (some(x:G) b) => (some(x:G) a or b) proof -- similar to the previous proof end (some(x:G) a or b) => (some(x:G) a) or (some(x:G) b) proof enter premise( some(x:G) a or b, all(w:G) a[x:=w] or b[x:=w] => (some(x:G) a) or (some(x:G) b) ) remove enter(2) case_split(a[x:=w], b[x:=w]) enter; premise(some(x:G) a); premise(a[x:=w]); remove enter; premise(some(x:G) b); premise(b[x:=w]); remove end end

For all three proves we can shift an existentially quantified expression onto the assumption stack and use the elimination rule "exist_elim". The first two proofs continue with the rule "or_intro" and the third with "or_elim" (i.e. a case split).

The universal and the existential quantifier are interrelated. If we say that all objects do not satisfy a certain property we conclude that there is no object which satisfies this property. Furthermore if there is an object which does not satisfy a property we conclude that not all objects can satisfy this property.

The corresponding laws are similar to the de Morgan laws for "and" and "or". We expect the following assertions to be valid.

all[G](e:BOOLEAN) check (all(x:G) not e) => not some(x:G) e (not some(x:G) e) => all(x:G) not e (some(x:G) not e) => not all(x:G) e (not all(x:G) e) => some(x:G) not e (all(x:G) not e) = (not some(x:G) e) (some(x:G) not e) = (not all(x:G) e) end

The first one is proved by

all[G](e:BOOLEAN) check (all(x:G) not e) => not some(x:G) e proof enter premise((some(x:G) e) => False) -- proof by contradiction enter premise(some(x:G) e, -- elimination rule for "exists" all(w:G) e[x:=w] => False ) -- rename bound variable remove enter(2) premise(e[x:=w], not e[x:=w]) -- all(x:G) not e -- some(x:G) e -- w:G -- e[w:=a] -- ================= -- e[x:=w] -- not e[x:=w] remove(2) end end

The line of reasoning is the following:

- After entering the implication we have to prove "not some(x:G) e". We prove this by contradition, i.e. we use the general law "(a=>False) => not a". With one enter step we have "some(x:G) e" among the assumptions and have to prove the goal "False". We can prove this by deriving a contradiction from the assumptions.
- Having "some(x:G) e" among the assumptions gives the opportunitiy to exploit the elimination rule "exist_elim". We use this rule by a premise command.
- The first premise is "some(x:G) e" which can be removed immediately (it is identical to an assumption).
- The left hand side of the second premise "all(w:G) e[x:=w] => False" can be entered onto the assumption stack. This puts "e" onto the assumptions. Since we have already "all(x:G) not e" on the assumption stack the contradiction is obvious.

The second assertion is the first one flipped. It is proved by

all[G](e:BOOLEAN) check (not some(x:G) e) => all(x:G) not e proof rewrite(all(x:G) e, all(w:G) e[x:=w]) -- rename enter(2) contradiction(some(x:G) e) -- not some(x:G) e -- w:G -- e[x:=w] -- ================ -- some(x:G) e -- not some(x:G) e premise(e[x:=w]); remove remove end end

By entering two assumptions we put "not e" onto the goal stack. Using a proof by contradiction we assume the opposite. Having "e" among the assumptions we can prove "some(x:G) e". We can prove "not some(x:G) e" as well, because it is already on the assumption stack. Note how the introduction rule "exist_intro"

exist_intro: all[G](e:BOOLEAN) all(a:G) e[x:=a] => some(x:G) e

has been used to prove "some(x:G) e".

The remaining third and forth implication are proved by

all[G](e:BOOLEAN) check (some(x:G) not e) => not all(x:G) e proof premise((all(x:G) e) => not some(x:G) not e) rewrite(all(x:G) e, all(x:G) not not e) remove end (not all(x:G) e) => some(x:G) not e proof premise((not some(x:G) not e) => all(x:G) e) rewrite(all(x:G) e, all(x:G) not not e) remove end end

These two proofs use the laws of contraposition

all(a,b:BOOLEAN) check (a => not b) => (b => not a) (not a => b) => (not b => a) end

and the law of double negation to transform the assertion into a form equivalent to one of the first two assertions.

With the first four implications the equivalences are trivially valid.

Can we flip the existential and the universal quanitifier? In one direction yes, in the other not. The valid direction is

all[X,Y](e:BOOLEAN) (some(y:Y) all(x:X) e) => all(x:X) some(y:Y) e

I.e. if there is a "y" such that for all "x" the assertion "e" is valid then for all "x" there is a "y" such that "e" is valid. The reverse is not true. Let's assume that "e" is "x has mother y". Certainly everybody has a mother. Therefore "all(x) some(y) e" is valid. But there is no single "y" which is mother for all "x", i.e. "some(y) all(x) e" is not valid.

The valid direction is proved by

all[X,Y](e:BOOLEAN) check (some(y:Y) all(x:X) e) => all(x:X) some(y:Y) e proof enter(2) premise( some(y:Y) all(x:X) e, (all(b:Y) all(a:X) e[x,y:=a,b] => all(x:X) some(y:Y) e ) remove enter_all -- some(y:Y) all(x:X) e -- b:Y -- a:X -- e[a,b:=x,y] -- x:X -- ============ -- some(y:Y) e premise(e[a,b:=x,y]) remove end end

After the first enter command we reach the state

some(y:Y) all(x:X) e x:X ----------------------- some(y:Y) e

We have an existential quantified expression among the assumptions. Therefore the elimination rule "exist_elim" is applicable. In the above proof we have used some renaming of the bound variables to avoid confusion.

This article completes the rules of logic used by the programming language Modern Eiffel.

To have the complete set of the rules of logic please read the articles

- Introduction to the proof engine
- Proofs by contradiction
- This article

The previous article has already introduced reasoning with inductive types with some very primitive examples.

The following articles will concentrate more on data types and computation.

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: