## Wednesday, October 5, 2011

### EQ 9 Quantification

(1) Monoids And Abelian Monoids

Binary Operator $$\star$$ is associative and has an identity $$\equiv$$ it is a monoid. If it is also symmetric, it is an abelian monoid.

In the following the $$\star$$ represents an operator that is an abelian monoid. All theorems don't strictly need the "abelian-ness", but the operators we deal with are all abelian, so the assumption does no harm.

(2) General Form of Quantification

( $$\star$$ x:type1, y:type2 ..) | Range:$$\mathcal{B}$$ : Predicate:type3)

x,y,... are bound variables or 'dummmies'
the Predicate is also known as the "body".

(3) Definition of 'free'

(a) The *occurrence* of i, in an expression i is free
(b) If an occurrence of a variable i in expression E is free, then so is the occurrence in (E), function application arguments f(....E...) [note: binary operators are considered function applications)[, ($$\star$$x|E:P) and ($$\star$$x|R:E) (as long as i is not one of the variables in the dummy list x.)

(4) Definition of 'bound'

(a) If an occurrence of a variable i in expression E is free, then that occurrence is bound to dummy i in ($$\star$$x|E:P) and ( $$\star$$x|R:E) if i occurs in dummy list x.

(b) If an occurrence of i is bound in expression E, then it is also bound to the same dummy in (E), function application arguments f(....E...) [note: binary operators are considered function applications)], ($$\star$$x|E:P) and ($$\star$$x|R:E)

(5) Definition of occurs-free and not-occurs-free

occurs-free(v,e) is defined to mean that at least one variable from the list-of-variables v occurs free in at least one expression in list of expressions v

not-occurs-free(v,e) $$\equiv$$ $$\neg$$occurs-free(v,e) $$\equiv$$ no variable in list-of-variables v occurs free in any of the expressions in list-of-expressions e

(6) Textual Substitution

Extending textual substitution to quantified statements

( $$\star$$ x | R : P)[y := F] $$\hspace{0.2 cm}\equiv\hspace{0.2 cm}$$ $$(\star$$ x | R[y := F] : P[y := F]),

given not-occurs-free(x,[y,F])), iow none of the bound variables is free on either side of the := . If a bound variable does occur free on either side of :=, replace *the bound variable* with a fresh variable j. This ensures that a free variable in the textual substitution y := F does not become bound.

Extending Leibniz inference rule to handle substitution of either side of an equality into a quantified statement

(7) Leibniz 1

$$\frac{A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R [z:=A]: P ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R [z:=B]: P )}$$

(8) Leibniz 2

$$\frac{R\hspace{0.2 cm}\Rightarrow\hspace{0.2 cm}A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R : P[z:=A] ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R : P [z:=B])}$$

(9) Axiom: Empty Range: ( $$\star$$ x | false : P ) $$\hspace{0.2 cm} \equiv\hspace{0.2 cm}$$ u (the identity of $$\star$$)

(10) Axiom: One Point Range: ( $$\star$$ x | x = E : P ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ P[ x := E ]
provided not-occurs-free (x,E)

(11) Axiom: Distributivity: ( $$\star$$ x | R : P ) $$\star$$ ( $$\star$$ x | R : Q ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ x | R : P $$\star$$ Q )
provided each quantification is defined (quantifications with finite ranges are always defined as are quantifications with $$\star$$ being either $$\wedge$$ or $$\vee$$. if $$\star$$ is +, then you have to check for convergence of the summation, etc)

(12) Axiom: Range Split 1: ( $$\star$$ x | R $$\vee$$ S: P ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ x | R : P ) $$\star$$ ( $$\star$$ x | S : P )
provided (R $$\wedge$$ S) is false $$\wedge$$ each quantification is defined

(13) Axiom: Range Split 2: ( $$\star$$ x | R $$\vee$$ S: P ) $$\star$$ ( $$\star$$ x | R $$\wedge$$ S: P ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ x | R : P ) $$\star$$ ( $$\star$$ x | S : P )
provided each quantification is defined

(14) Axiom: Range Split 3: ( $$\star$$ x | R $$\vee$$ S: P ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ x | R : P ) $$\star$$ ( $$\star$$ x | S : P )
provided $$\star$$ is idempotent $$\wedge$$ each quantification is defined

Note: Definition of idempotent: $$\star$$ is idempotent $$\equiv$$ ( a $$\star$$ a $$\equiv$$ a)

(15) Axiom: Interchange of Dummies: ( $$\star$$ x | R :( $$\star$$ y | S : P) ) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ y | S :( $$\star$$ x| R : P) )
provided not-occurs-free(x,S) $$\wedge$$ not-occurs-free(y,R) $$\wedge$$ each quantification is defined

iow "nested quantifications with the same operator can be interchanged"

(16) Axiom: Dummy Nesting: ($$\star$$ x,y | R $$\wedge$$ S : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ( $$\star$$ x | R :( $$\star$$ y | S : P) )
provided not-occurs-free(y,R)

iow " a single quantification over a list of dummies can be viewed as nested quantification"

(17) Axiom: Dummy Renaming: ($$\star$$x | R : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\star$$y | R[x := y] : P[x := y])
provided not-occurs-free (y, [R,P])

iow "one dummy can be replaced consistently by another dummy"

(18) Theorem: Change of Dummy (Generalization of Dummy Renaming) ($$\star$$x | R : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\star$$x | R [x := f.y] : P[x := f.y])

provided not-occurs-free (y,[R,P]) $$\wedge$$ f is an invertible function such that x = $$f.y$$ and y = $$f^{-1}.x$$

Example: Consider (+ $$i$$ | 2 $$\leq$$ $$i$$ $$\leq$$ 10 : $$i^2$$ ) and we need to have a range starting with zero

the reqd range is (2 - 0) $$\leq$$ $$i - 2$$ $$\leq$$ (10 - 2)

let k = (i - 2) this is new dummy expressed in terms of old = $$f^{-1}.i$$ = k = i - 2

so i = k + 2 this is old dummy expressed in terms of new = $$f.k$$ = i = k + 2

$$\hspace{2 cm}$$(+ $$i$$ | 2 $$\leq$$ $$i$$ $$\leq$$ 10 : $$i^2$$ )
= $$\hspace{0.5 cm}$$ Dummy Renaming Theorem. Rename the dummy from i to k with i = f.k = k - 2
$$\hspace{2 cm}$$(+ $$k$$ | 2 $$\leq$$ $$k+2$$ $$\leq$$ 10 : $$(k+2)^2$$ )
= $$\hspace{0.5 cm}$$ arithmetic a $$\leq$$ b $$\leq$$ c $$\equiv$$ a-2 $$\leq$$ b-2 $$\leq$$ c-2
$$\hspace{2 cm}$$(+ $$k$$ | 0 $$\leq$$ $$k$$ $$\leq$$ 8 : $$(k+2)^2$$ )

(19) Theorem: Split off term 1
($$\star i$$ | $$0 \leq i \lt n+1$$ : P) $$\equiv$$ ($$\star i$$ | $$0 \leq i \lt n$$ : P) $$\star$$ P[i := n ]

(20) Theorem: Split off term 2
($$\star i$$ | $$0 \leq i \lt n+1$$ : P) $$\equiv$$ P[i := 0 ] $$\star$$ ($$\star i$$ | $$0 \lt i \lt n + 1$$ : P)