Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Typentheorie 01-02
Typentheorie 01-02
Inhoud
In het college typentheorie worden typen geintroduceerd aan de hand van
het Curry-Howard (CH) isomorphisme.
Het CH-isomorphisme geeft een correspondentie
tussen typen en formules.
Aangezien we al weten wat formules zijn, weten we
dus ook wat typen zijn ...
Het CH-isomorphisme geeft niet alleen een correspondentie
tussen typen en formules, maar ook tussen de dingen die
een type hebben en de bewijzen van formules.
We behandelen dit voor twee gevallen:
lambda-termen corresponderen met
natuurlijke deduktie bewijzen,
combinatorische logica termen corresponderen met
Hilbert-stijl bewijzen,
en breiden de eerste correspondentie uit van
propositielogica naar hogere logica's.
Gebruikt materiaal:
M H Sorensen and P Urzyczyn,
Lectures on the Curry-Howard Isomorphism,
DIKU Rapport 98/14, 1998.
(Schrik niet, er zal slechts een gering gedeelte op
het college behandeld gaan worden.) Coq.
Vorm
In de tentamenweek van blok 2 is er een tentamen
(waarschijnlijk op vrijdag 21 november 2001, van 9:00 tot 12:00), wat
geherkanst kan worden in de tentamenweek van blok 3.
Het tentamen bepaalt 80% van het eindcijfer.
Iedere week kunnen er opgaven ingeleverd worden.
De opgaven bepalen 30% van het eindcijfer.
Vanaf de derde week maken praktische opgaven deel uit van
de in te leveren opgaven.
de opgaven zullen op vrijdag bekend gemaakt worden.
De opgaven dienen (uiterlijk) aan het begin van de
daaropvolgende werkgroep ingeleverd te worden,
duidelijk voorzien van uw naam.
Niet (tijdig) inleveren telt als een 0 (nul).
Er is geen herkansingsmogelijkheid voor de in te leveren opgaven.
russell paradox (de verzameling R = {x | x not in x })
codering russell's paradox voor het systeem van Frege
idee van RTT (ramified theory of types)
verschil tussen simpele en vertakkende typen
systeem van Frege complex
lambda calculus als calculus die de basis operaties
abstractie en applicatie bevat
idee van simpele typen voor de lambda calculus
vrijdag 2 november: lambda calculus
grammatica van lambda calculus
gevolg: unique reading, inductie en recursie voor lambda termen
vb: lengte van lambda-term, vrije en gebonden variabelen
definitie van alpha equivalentie (corresponderende variabelen
worden op corresponderende plekken gebonden):
M =a N als []M =a []N
[]x =a []x
[kx]x =a [ly]y
[kx']x =a [ly']y als [k]x =a [l]y, x =/= x' en y =/= y'
[k](M1M2) =a [l](N1N2) als [k]M1 =a [l]N1 en [k]M2 =a [l]N2
[k](\x.M) =a [l](\y.N) als [kx]M =a [ly]N
alpha-equivalentie is een equivalentie relatie
(reflexief, symmetrisch, transitief)
lambda termen modulo alpha-equivalentie
definitie van substitutie van een term voor alle vrije
voorkomens van een variabele in een andere term:
x[x:=N] = N
y[x:=N] = y
(MP)[x:=N] = (M[x:=N]P[x:=N])
(\y.M)[x:=N] = (\y.M[x:=N]), met y niet vrij in N
mogen we aannemen vanwege alpha equivalentie
Huiswerk:
Bewijs dat als M =a N dan FV(M) = FV(N)
opgave 1.7.2
opgave 1.7.3
opgave 1.7.6
bewijs dat =a zoals hiergedefinieerd overeenkomt met
alpha-conversie zoals gedefinieerd in def. 1.1.15
dinsdag 6 november : beta reductie in lambda calculus
definitie van beta reductie
dinsdag 13 november : rekenkracht van lambda calculus
(enige) opgaven voor het werkcollege van vrijdag 16 november
Bewijs dat \nfx.f (n f x) en \nfx.n f (f x) beide
de successor functie voor church-numerals in de
lambda calculus coderen.
Formuleer daartoe eerst precies wat dit betekent.
Bewijs dat YF ->> F(YF) voor iedere lambda term F,
waarbij Y een fixed point combinator gedefinieerd door
Y = AA, met A = \xf.f(xxf).
Huiswerk : 1.7.17, 1.7.20, 1.7.21, 1.7.22
(enige) opgaven voor het werkcollege van vrijdag 23 november
Bewijs dat als de termen N1,..,Nk all SN zijn,
dan is de term xN1..Nk dat
ook voor een willekeurige variabele x.
Huiswerk:
Bewijs dat de diamond property confluentie impliceert
Bewijs het substitutie lemma, dwz bewijs dat
M[x:=N][y:=P] = M[y:=P][x:=N[y:=P]]
(met x niet in P), voor getypeerde lambda calculus.
Bewijs dat ieder herschrijf systeem dat
lokaal confluent en terminerend is confluent is.