Function Theory
〈v:D→b〉 “map v in D to b”
body (may use v ) domain, type (a bunch)
variable, parameter (a fresh name) v: D is a local axiom within b
n: nat n+1 00 11 22 33 :4
:
:
:
1/22
Renaming
〈n:nat→n+1〉 = 〈m:nat→m+1〉
Domain
f
〈n: nat → n+1〉
“domain of f ”
= nat
Application
f x
f (x) (f)x
〈n:nat→n+1〉3 = 3+1 = 4
“ f applied to x ” or “ f of x ” ¬x
f (x+1) –x
2/22
two variables
max = 〈x:xrat→〈y:xrat→ifx≥ythenxelseyfi〉〉 max3 = 〈y:xrat→if3≥ythen3elseyfi〉
max 3 5 = if 3≥5 then 3 else 5 fi = 5
max(3, 5) = max 3, max 5
predicate function with binary result even = 〈i: int → i/2: int〉
relation function with predicate result divides = 〈n: nat+1 → 〈i: int → i/n: int〉〉
even = divides 2
3/22
selective union
f|g “f otherwise g” (f|g)= f,g
(f | g) x = if x: f then f x else g x fi
abbreviated function notations
〈x:xrat→〈y:xrat→ifx≥ythenxelseyfi〉〉 = 〈x,y:xrat→ifx≥ythenxelseyfi〉 〈n:nat→n+1〉 = 〈n→n+1〉
〈n: 2 → 3〉 = 2→3 scope brackets go with variable
〈x: int → 〈y: int → x+3〉〉 = x+3 ? but we can’t apply it
4/22
local
nonlocal
bound, hidden, private
introduction is inside the expression (formal)
global, free, visible, public
introduction is outside the expression (formal or informal)
〈x→ x y 〉( x y )
Scope and Substitution
5/22
Scope and Substitution local bound, hidden, private
introduction is inside the expression (formal)
nonlocal global, free, visible, public
introduction is outside the expression (formal or informal)
〈x→ x 〈x→ x 〉 x 〉3 = ( 3 〈x→ x 〉 3 )
6/22
local
nonlocal
〈y→ = 〈y→
= (
bound, hidden, private
introduction is inside the expression (formal)
global, free, visible, public
introduction is outside the expression (formal or informal)
x y 〈x→ x y 〉 x y 〉x
x y 〈z→ z y 〉 x y 〉x x x 〈z→ z x 〉 x x )
renameinnerxtoz nowapply
Scope and Substitution
7/22
A quantifier is an operator that applies to a function.
It is defined from a two-operand symmetric associative operator.
∀p is defined from ∧ ∃p is defined from ∨ Σf is defined from + Πf is defined from ×
abbreviations
∀r: rat· r<0 ∨ r=0 ∨ r>0 Σn: nat+1· 1/2n
∀〈r: rat → r<0 ∨ r=0 ∨ r>0〉 ∃〈n: nat → n=0〉
Σ〈n: nat+1 → 1/2n〉
Π〈n: nat+1 → (4×n2)/(4×n2–1)〉
Quantifiers
∀x,y:rat·x=y+1 ⇒ x>y = ∀x:rat·∀y:rat·x=y+1 ⇒ x>y Σn, m: 0,..10· n×m = Σn: 0,..10· Σm: 0,..10· n×m
8/22
∀v: null· b = ⊤
∀v:x·b = 〈v:x→b〉x
∀v:A,B·b = (∀v:A·b)∧(∀v:B·b)
∃v: null· b = ⊥
∃v:x·b = 〈v:x→b〉x
∃v:A,B·b = (∃v:A·b)∨(∃v:B·b)
Σv: null· n = 0
Σv:x·n = 〈v:x→n〉x
(Σv: A,B· n) + (Σv: A‘B· n) = (Σv: A· n) + (Σv: B· n)
Πv: null· n = 1
Πv:x·n = 〈v:x→n〉x
(Πv:A,B·n)× (Πv:A‘B·n) = (Πv:A·n)× (Πv:B·n)
9/22
build your own
MAX x: rat· 4×x – x2 = 4
MAX v: null· n = –∞
MAXv:x·n = 〈v:x→n〉x
MAX v: A,B· n = max (MAX v: A· n) (MAX v: B· n)
x∧⊤=x x∨⊥=x
x+ 0 = x x×1=x
max x (–∞) = x
10/22
Solution Quantifier
§p is the (bunch of) solutions of predicate p
§v: null· b = null
§v:x·b = if〈v:x→b〉xthenxelsenullfi §v: A,B· b = (§v: A· b), (§v: B· b)
{ §i: int· i2=4 } = {–2, 2 }
{ §n: nat· n<3 } = {0,..3 }
11/22
An expression talks about its nonlocal variables.
∃n: nat· x = 2×n says
“ x is an even natural”
12/22
partial:
total: deterministic: nondeterministic:
〈n: nat· n, n+1〉
〈n: nat· n, n+1〉 3 =
3, 4
sometimes no result
always at least one result always at most one result sometimes more than one result
total and nondeterministic
00
11
22
33
Function Fine Points
:4
:
:
:
13/22
distribution
(f,g)x = f(x,y) =
double = double 2 double (2, double (2,
fx,gx fx,fy
〈n: nat → n+n〉 = 4
3) ⧧ (2, 3) + (2, 3) =
3) = double 2, double 3 =
tiny = 〈S: nat → $S < 3〉 tiny {null} = ⊤
tiny {0, 1, 2, 3} = ⊥
tiny null = null
4, 6 4, 5, 6
14/22
function inclusion
f:g = g: f∧∀x: g·fx:gx A→B = 〈a:A→B〉
A→B is a function whose domain is A and whose result is B . f:A→B = A: f ∧ ∀a:A·fa:B
A→B is all those functions whose domain is at least A and whose result is at most B . A→B is antimonotonic in A and monotonic in B .
suc: nat→nat
= nat: suc ∧ ∀n: nat· suc n: nat
= nat: nat ∧ ∀n: nat· n+1: nat = ⊤
function inclusion definition of suc
reflexivity and definition of nat 15/22
function inclusion
f:g = g: f∧∀x: g·fx:gx
suc: nat→nat
even: int→bin
max: xrat→xrat→xrat
A:B ∧ f:B→C ∧ C:D ⇒ f:A→D
(0,..10): nat ∧ suc: nat→nat ∧ nat: int ⇒ suc: (0,..10)→int
〈f: (0,..10)→int· ∀n: 0,..10· even (f n)〉 suc
= ∀n: 0,..10· even (suc n)
= ⊥
16/22
function equality
f=g = f= g ∧ ∀x: f·fx=gx
17/22
function composition
If¬f: gthen
(g f) = §x: f· fx: g
(g f) x = g (f x)
(even suc)
= §x: suc· suc x: even
= §x: nat· x+1: int = nat
(even suc) 3 = even (suc 3)
= even 4
= ⊤
(–suc) 3 = –(suc 3) = –4 (¬even) 3 = ¬(even 3) = ¬⊥
= ⊤
18/22
function composition
Suppose x, y: int
f, g: int→int
h: int→int→int Then
h fxg y
= (((h f) x) g) y
= ((h(fx))g)y
= (h (f x)) (g y)
= h (f x) (g y)
19/22
list as function
If m: 0,..#L then
〈n:0,..#L→Ln〉m = Lm
function ≈ list application ≈ indexing
function composition ≈ list composition – [3; 5; 2] = [–3; –5; –2]
suc[3;5;2] = [4;6;3]
1→21 | [10; 11; 12] = [10; 21; 12] ΣL = Σn: 0,..#L· Ln
20/22
limit
f: nat→rat
f0; f1; f2; ... is a sequence of rationals
(MAX m· MIN n· f(m+n)) ≤ (LIM f) ≤ (MIN m· MAX n· f(m+n))
LIM n· 1/(n+1) = 0 –1 ≤ (LIM n· (–1)n ) ≤ 1
(MIN f) ≤ (LIM f) ≤ (MAX f)
xreal = LIM (nat→rat)
21/22
limit
p: nat→bin
p0; p1; p2; ... is a sequence of binary values
∃m· ∀n· p(m+n) ⇒ LIM p ⇒ ∀m· ∃n· p(m+n)
∃m· ∀i· i≥m ⇒ pi ⇒ ∃m· ∀i· i≥m ⇒ ¬pi ⇒
LIM n· 1/(n+1) = 0 =
LIM p
¬ LIM p
⊥
22/22