CS计算机代考程序代写 flex Function Theory

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