a Practical Theory
of Programming
2021-3-15 edition Eric C.R. Hehner
Department of Computer Science University of Toronto Toronto ON M5S 2E4 Canada
The first edition of this book was published by Springer-Verlag Publishers, New York, 1993 ISBN 0-387-94106-1 QA76.6.H428
The current edition is available free at
www.cs.utoronto.ca/~hehner/aP ToP
An on-line course based on this book is at
www.cs.utoronto.ca/~hehner/FMSD
The author’s website is
www.cs.utoronto.ca/~hehner
You may copy all or part of this book freely as long as you include this page.
The cover picture is an inukshuk, which is a human-like figure made of piled stones. Inukshuks are found throughout arctic Canada. They are built by the Inuit people, who use them to mean “You are on the right path.”.
231
11 Reference
11.4 Laws 11.4.0 Binary
Let a , Binary
b , ⊤
¬⊥
c ,
d , and
e
be binary.
a⇐b =b⇒a ¬¬a = a
Excluded Middle (Tertium non Datur)
Duality (deMorgan)
¬(a∧b) = ¬a∨¬b
¬(a∨b) = ¬a∧¬b
Exclusion
a⇒¬b =b⇒¬a
a=¬b = a⧧b = ¬a=b
Inclusion
a ⇒ b = ¬a ∨ b (Material Implication) a⇒b =(a∧b =a)
a⇒b =(a∨b =b)
a ∨ ¬a Noncontradiction
¬(a ∧ ¬a)
¬(a ∧ ⊥) a∨⊤ a⇒⊤ ⊥⇒a
Identity ⊤∧a=a
⊥∨a=a ⊤⇒a=a ⊤=a=a
Idempotent a∧a=a
a∨a=a
Reflexive
a⇒a a=a
Indirect Proof
¬a ⇒ ⊥ = a
¬a ⇒ a = a Specialization
a∧b⇒a
Associative a∧(b∧c) =
a∨(b∨c) = a = (b = c) = a⧧(b⧧c) = a = (b ⧧ c) =
Base
(Reductio ad Absurdum)
(a ∧ b) ∧ c (a ∨ b) ∨ c (a = b) = c (a ⧧ b) ⧧ c (a = b) ⧧ c
a∧(b∧c) =
a∧(b∨c) =
a∨(b∧c) =
a∨(b∨c) =
a∨(b⇒c) = (a∨b)⇒(a∨c) a∨(b=c) = (a ∨ b) = (a ∨ c) a⇒(b∧c) = (a⇒b)∧(a⇒c) a⇒(b∨c) = (a⇒b)∨(a⇒c) a⇒(b⇒c) = (a⇒b)⇒(a⇒c) a ⇒ (b = c) = (a ⇒ b) = (a ⇒ c)
Mirror
Double Negation
Absorption
a∧(a∨b) =a
a∨(a∧b) =a
Direct Proof
(a ⇒ b) ∧ a ⇒ b
(a ⇒ b) ∧ ¬b ⇒ ¬a
(a∨b) ∧ ¬a ⇒ b(Disjunctive Syllogism)
Transitive
(a ∧ b) ∧ (b ∧ c) ⇒ (a ∧ c)
(a ⇒ b) ∧ (b ⇒ c) ⇒ (a ⇒ c) (a = b) ∧ (b = c) ⇒ (a = c)
(a ⇒ b) ∧ (b = c) ⇒ (a ⇒ c) (a = b) ∧ (b ⇒ c) ⇒ (a ⇒ c)
Distributive (Factoring)
(a∧b)∧(a∧c) (a ∧ b) ∨ (a ∧ c) (a∨b)∧(a∨c) (a∨b)∨(a∨c)
(Modus Ponens)
(Modus Tollens)
Symmetry (Commutative) a∧b =b∧a a∨b =b∨a a=b =b=a a⧧b =b⧧a
Antisymmetry (Double Implication) (a⇒b)∧(b⇒a) = a=b
Discharge
a∧(a⇒b) =a∧b
a⇒(a∧b) =a⇒b Antimonotonic
a⇒b ⇒ (b⇒c)⇒(a⇒c)
Monotonic
a⇒b ⇒c∧a⇒c∧b a⇒b ⇒c∨a⇒c∨b a⇒b ⇒ (c⇒a)⇒(c⇒b)
= (a⇒c)∨(b⇒c) = (a⇒c)∧(b⇒c)
=a⇒(b⇒c) = a ⇒ ¬b ∨ c
Resolution
Case Creation
a = ifbthenb⇒aelse¬b⇒afi a = ifbthenb∧aelse¬b∧afi
a = ifbthenb=aelseb⧧afi
Case Analysis
ifathenbelsecfi = (a∧b)∨(¬a∧c) ifathenbelsecfi=(a⇒b)∧(¬a⇒c)
Case Absorption
ifathenbelsecfi = ifathena∧belsecfi ifathenbelsecfi = ifathena⇒belsecfi ifathenbelsecfi = ifathena=belsecfi ifathenbelsecfi = ifathenbelse¬a∧cfi ifathenbelsecfi = ifathenbelsea∨cfi ifathenbelsecfi = ifathenbelsea⧧cfi
One Case
ifathen⊤elsebfi = a∨b
ifathen⊥elsebfi = ¬a∧b ifathenbelse⊤fi = a⇒b ifathenbelse⊥fi = a∧b ifathenbelse¬bfi = a=b ifathen¬belsebfi = a⧧b
Case Distributive (Case Factoring)
¬ifathenbelsecfi = ifathen¬belse¬cfi ifathenbelsecfi∧d = ifathenb∧delsec∧dfi
and similarly replacing ∧ by any of ∨ = ⧧ ⇒ ⇐ ifathenb∧celsed∧efi = ifathenbelsedfi∧ifathencelseefi
and similarly replacing ∧ by any of ∨ = ⧧ ⇒ ⇐
11 Reference Generalization
a⇒a∨b
Antidistributive
a∧b⇒c a∨b⇒c
Portation
a∧b⇒c a∧b⇒c
232
a⧧b = (a∧¬b)∨(¬a∧b) a∧c ⇒ (a∨b)∧(¬b∨c) = (a∧¬b)∨(b∧c) ⇒ a∨c
Conflation
(a⇒b)∧(c⇒d) ⇒a∧c⇒b∧d (a⇒b)∧(c⇒d) ⇒ a∨c⇒b∨d
Contrapositive
a⇒b =¬b⇒¬a
Equality and Difference
a=b = (a∧b)∨(¬a∧¬b)
End of Binary
233 11 Reference
11.4.1 Generic
The operators = ⧧ if then else fi apply to every type of expression (but the first operand of if then else fi must be binary), with the laws
x=x
x=y = y=x
x=y ∧ y=z ⇒ x=z x=y ⇒ fx=fy x⧧y = ¬(x=y)
x≤x
¬(x
x≤y = x
irreflexivity exclusivity inclusivity transitivity transitivity
mirror
totality
totality, trichotomy
reflexivity symmetry transitivity transparency unequality
if ⊤ then x else y fi = x if⊥thenxelseyfi = y
if a then x else x fi = x
ifathenxelseyfi = if¬athenyelsexfi
case reversal The operators < ≤ > ≥ apply to numbers, characters, strings, and lists, with the laws
Let d be a sequence of (zero or more) digits, and let x , y , and z be numbers.
d0+1 = d1 d1+1 = d2 d2+1 = d3 d3+1 = d4 d4+1 = d5 d5+1 = d6 d6+1 = d7 d7+1 = d8 d8+1 = d9 d9+1 = (d+1)0 x+0 = x
x+y = y+x
x+(y+z) = (x+y)+z
–∞
–∞ ≤ x ≤ ∞
11.4.3 Bunches
x/∞ = 0 = x/–∞ x0=1
11 Reference
234
Let x and y be elements (binaries, numbers, characters, sets, strings and lists of elements).
x: y = x=y
x:A,B = x:A ∨ x:B A,A = A
A,B = B,A
A,(B,C) = (A,B),C
A‘A = A
A‘B = B‘A
A‘(B‘C) = (A‘B)‘C A,B:C = A:C ∧ B:C A:B‘C = A:B ∧ A:C A: A,B
A‘B: A
A: A
A:B∧B:A =A=B A:B ∧ B:C ⇒ A:C ¢null = 0
¢x=1
¢ nat = ∞
¢(A, B) + ¢(A‘B) =
elementary compound idempotence symmetry associativity idempotence symmetry associativity antidistributivity distributivity generalization specialization reflexivity antisymmetry transitivity
size size size size
¢A + ¢B
End of Numbers
235
11 Reference
¬ x: A ⇒ ¢(A‘x) = 0 A:B ⇒ ¢A≤¢B A,(A‘B) = A
A‘(A,B) = A
A:B = A,B=B = A=A‘B A,(B,C) = (A,B),(A,C) A,(B‘C) = (A,B)‘(A,C) A‘(B,C) = (A‘B), (A‘C) A‘(B‘C) = (A‘B)‘(A‘C)
A:B ∧ C:D ⇒ A,C:B,D A:B ∧ C:D ⇒ A‘C:B‘D null: A
A, null = A
size
size
absorption
absorption
inclusion
distributivity distributivity distributivity distributivity
conflation, monotonicity conflation, monotonicity induction
identity
base
size
A ‘ null = null
¢A = 0 = A = null
x:int ∧ y:xint ∧ x≤y ⇒ (i:x,..y = i:int ∧ x≤i
floor: real→int
info: prob→§r: xreal· r≥0 int (the integers)
LIM (limit quantifier)
log: (§r: xreal· r≥0)→xreal
max: xrat→xrat→xrat MAX (maximum quantifier)
min: xrat→xrat→xrat MIN (minimum quantifier)
mod: real→(§r: real· r>0)→real nat (the naturals)
nil (the empty string)
null (the empty bunch)
odd: int→bin
ok (the empty program)
prob (probability)
rand (random number)
rat (the rationals)
real (the reals)
suc: nat→(nat+1)
xint (the extended integers) xnat (the extended naturals) xrat (the extended rationals) xreal (the extended reals)
abs r = if r≥0 then r else –r fi bin = ⊤, ⊥
r ≤ ceil r < r+1
char = ..., “a”, “A”, ...
div x y = floor (x/y)
divides n i = i/n: int
entro p = p × info p + (1–p) × info (1–p) even i = i/2: int
even = divides 2
floor r ≤ r < floor r + 1
info p = – log p
int = nat, –nat
see Laws
log (2x) = x
log (x×y) = log x + log y
max x y = if x≥y then x else y fi
– max a b = min (–a) (–b)
see Laws
min x y = if x≤y then x else y fi
– min a b = max (–a) (–b)
see Laws
0 ≤ mod a d < d
a = div a d × d + mod a d
0, nat+1: nat
0,B+1:B ⇒ nat:B
↔nil = 0
nil;S = S = S;nil
nil ≤ S
¢null = 0
null,A = A = A,null
null: A
odd i = ¬ i/2: int
odd = ¬even
ok = σʹ=σ
ok.P = P = P.ok
prob = §r: real· 0≤r≤1
rand n: 0,..n
rat = int/(nat+1)
r: real = r: xreal ∧ –∞
assert chan
do od ensure exit when for do od frame
go to
true
false
not
and
or
implies
implies
follows from, is implied by follows from, is implied by equals, if and only if equals, if and only if differs from, is unequal to less than
greater than
less than or equal to
greater than or equal to
plus
minus
times, multiplication
divided by
bunch union
union from (incl) to (excl) bunch intersection
string join
list join
join from (incl) to (excl)
is in, are in, bunch inclusion includes
assignment
label, target of go to
dep’t (sequential) composition quantifier abbreviation
output
input
77
138
71
77
71
74
67
75
√ 133 ()4
input check
parentheses for grouping
set brackets
list brackets
function (scope) brackets
power
bunch size, cardinality
set size, cardinality
string size, length
list size, length
selective union, otherwise
indep’t (parallel) composition contents of a set or list
repetition of a string
domain of a function
function arrow
element of a set
subset
set union
set intersection
index with a pointer
for all, universal quantifier
there exists, existential quantifier sum of, summation quantifier product of, product quantifier those, solution quantifier
xʹ is final value of state var x “hi” is a text or string of chars exponentiation
string indexing indexing,application,composition string modification
infinity
11 Reference
242
17 20 23 17 14 17 18 20 20,24 118 17,20 18 23 23 17 17 17 17 22 26 26 26 26 28 34 13,19 12 18 20,31
{} [] 〈〉
¢
$
↔
#
| || ~ *
→ ∈ ⊆ ∪ ∩ @ ∀ ∃ Σ Π § ʹ
“ ”
ab
if then else fi
ivar 126 or 77 result 78 var 66 wait until 76 while do od 69
ab
a b
⊲⊳ 18 ∞ 12
4
End of Symbols
243 11 Reference
11.7 Precedence
0 ⊤ ⊥ ( ) { } [ ] 〈 〉 if fi do od number text name
superscript
subscript
1 @ juxtaposition
2 prefix–¢$↔#*~ →√
3 ×/∩
4 + infix– ∪
5 ;;..;;‘
6 ,,..|⊲⊳
7 =⧧<>≤≥:::∈⊆
8¬ 9∧
10 ∨
11 ⇒⇐
12 :=!?
13 exit when
14 . || result
15 ∀· ∃· Σ· Π· §· LIM· MAX· MIN· var· ivar· chan· frame·
16 =⇒⇐
go to
wait until
assert
ensure or
Superscripting and subscripting serve to bracket all operations within them.
Juxtaposition associates from left to right, so a b c means the same as (a b) c . The infix operators @ / – associate from left to right. The infix operators * → associate from right to left. The infix operators × ∩ + ∪ ; ;; ‘ , | ∧ ∨ . || are associative (they associate in both directions).
On levels 7, 11, and 16 the operators are continuing. For example, a=b=c neither associates to the left nor associates to the right, but means the same as a=b ∧ b=c . On any one of these levels, a mixture of continuing operators can be used. For example, a≤b