Programming Notes – Quantifying Sequences

 

 

Axiom 1: P {skip} R º P {(;x|false:B[x])} R

 

Axiom 2: (RÇS = ÆÙ (iÎR Ù jÎS º B[i]<B[j])) Þ

(;x|RÈS:B[x]) = (;x|R:B[x]);(;x|S:B[x])

 

Axiom 3: P {(;x|x=E:B[x])} R º P {B[E]} R

 

Axiom 4: A((;x|E:r[x])) º (;x|E:A(r[x]))

 

Theorem 1: P {(;x|m£x£n:skip)} R º P {skip} R

case n<m

(prove LHS º RHS)

P {(;x|m£x£n:skip)} R    

º(algebra)

P {(;x|false:skip)} R    

º(Axiom 1)

P {skip} R   

End of Proof (Case n < m)

 

Case m=n

(prove LHS º RHS)

P {(;x|m£x£n:skip)} R

º(given)   

P {(;x|m£x£m:skip)} R

º(algebra) 

P {(;x|x=m:skip)} R

º(Axiom 3)

P {skip} R   

End of Proof (Case n = m)

 

Case m < n

(Case n=m can serve as the first case.

Assume true for Case n=k, show true for n=k+1)

P {(;x|m£x£k+1:skip)} R

º(Axiom 2)

P {(;x|m£x£k:skip);(;x|k+1£x£k+1:skip)} R

º(algebra) 

P {(;x|m£x£k:skip);(;x|x=k+1:skip)} R

º(Axiom 3)

P {(;x|m£x£k:skip);skip) R

º(Right Identity of Program Sequence)

P {(;x|m£x£k:skip)} R

º(Assumption of induction)

P {skip} R

End of Proof (Case m < n)

End of Proof

 

Theorem 2: ("n|k£n: ("i|k£i£n: H[i-1] {r[i]} H[i]) Þ

            H[k-1] {(;i|k£i£n: r[i])} H[n] )

(prove LHS Þ RHS by induction)

Case n=k

      ("i|k£i£k: H[i-1] {r[i]} H[i])

º(Algebra, one point rule)

      H[k-1] {r[k]} H[k]

º(Algebra, Axiom 3)

      H[k-1] {(;i|k£i£k:r[i])} H[k]

End of Proof (case n=k)

 

Case n=m, m+1

(Given true for n=m, prove true for n=m+1)

      ("i|k£i£m+1: H[i-1] {r[i]} H[i])

º(Split off term)

      ("i|k£i£m: H[i-1] {r[i]} H[i]) Ù (H[m] {r[m+1]} H[m+1])

º(Given true for n=m)

      H[k-1] {(;i|k£i£m:r[i])} H[m] Ù (H[m] {r[m+1]} H[m+1])

Þ(Program Sequence Theorem 4)

      H[k-1] {(;i|k£i£m:r[i]);r[m+1]} H[m+1])

º(Axiom 2)

      H[k-1] {(;i|k£i£m+1:r[i])} H[m+1])

End of Proof Case n=m,m+1

End of Proof

 

Theorem 3: ("i|k£i£n:("B|("A|A {r[i]} B º A {s[i]} B:A):B)) Þ

      ("B|("A|A {(;i|k£i£n:r[i])} B º A {(;i|k£i£n:s[i])} B:A):B)

 

Part 1 (Case n=k)

(Prove LHS º RHS, which proves LHS Þ RHS)

("i|k£i£k:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

º(Algebra)

("i|k=i:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

º(one point rule)

("B|("A|A {r[k]} B º A {s[k]} B:A):B)

º(one point rule)

("B|("A|A {(;i|k=i:r[i])} B º A {(;i|k=i:s[i])} B:A):B)

º(Algebra)

("B|("A|A {(;i|k£i£k:r[i])} B º A {(;i|k£i£k:s[i])} B:A):B)

End of Part 1 Proof

 

Part 2 (Case n=m, m+1)

(Given that the theorem is true for n=m, prove true for n=m+1)

("i|k£i£m+1:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

º(Split off term)

("i|k£i£m:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

      Ù

("i|m+1£i£m+1:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

Þ(given true for n=m)

("B|("A|A {(;i|k£i£m:r[i])} B º A {(;i|k£i£m:s[i])} B:A):B)

      Ù

("i|m+1£i£m+1:("B|("A|A {r[i]} B º A {s[i]} B:A):B))

º(Algebra, one point rule)

("B|("A|A {(;i|k£i£m:r[i])} B º A {(;i|k£i£m:s[i])} B:A):B)

      Ù

("B|("A|A {r[m+1]} B º A {s[m+1]} B:A):B)

Þ(Program Sequence Theorem 11)

("B|("A|A {(;i|k£i£m:r[i]);r[m+1]} B º A {(;i|k£i£m:s[i]);s[m+1]} B:A):B)

º(Axiom 2)

("B|("A|A {(;i|k£i£m+1:r[i])} B º A {(;i|k£i£m+1:s[i])} B:A):B)

End of Part 2 Proof

End of Proof

 

Theorem 4: ("B|("A|A {r} B º A {s} B:A):B) Þ

      ("B|("A|A {(;i|k£i£n:r)} B º A {(;i|k£i£n:s)} B:A):B)

(Prove LHS Þ RHS)

      ("B|("A|A {r} B º A {s} B:A):B)

º(Introduce quantified variable, Ù is reflexive)

      ("i|k£i£n:("B|("A|A {r} B º A {s} B:A):B))

Þ(Theorem 3)

("B|("A|A {(;i|k£i£n:r)} B º A {(;i|k£i£n:s])} B:A):B)

End of Proof

 

References:

 

Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall

 

Fejer, Peter A., 1991, Mathematical foundations of computer science, New York, NY: Springer-Verlag

 

Gries, David, 1981, The Science of Programming, New York, NY: Springer-Verlag

 

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag

 

http://www.anaesthetist.com/mnm/javascript/index.htm Chapter 2 contains an excellent description of boolean operations in JavaScript.