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 00-01
Typentheorie 00-01
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
het tentamen is op woensdag 25 oktober van 9:00-12:00
in zaal 114 van Trans 1.
er is een vragenuur op maandag 23 oktober vanaf 11:00 in zaal BG 465.
Iedere week zijn er hoorcolleges Typentheorie op
maandag
(op 4-9, 11-9, 18-9, 25-9, 2-10, 9-10)
en woensdag
(op 6-9, 13-9, 20-9, 27-9, 4-10, 11-10),
op beide dagen van 11:00 tot 13:00.
Op woensdagmiddagen is er aansluitend een werkgroep van
13:00 tot 15:00.
Tevens zal er vanaf de derde week op vrijdagmiddag
(op 22-9, 29-9, 6-10, 13-10)
een praktikum zijn.
Zie het
rooster voor precieze zaalgegevens.
In de tentamenweek van blok 1 is er een tentamen, wat
geherkanst kan worden in de tentamenweek van blok 2.
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.
Wijziging d.d. 13 september :
de opgaven zullen op vrijdag bekend gemaakt worden.
De opgaven dienen (uiterlijk) aan het begin van de
daaropvolgende woensdagse werkgroep ingeleverd te worden,
duidelijk voorzien van uw naam.
Click voor informatie over de huiswerkopgaven
op de naam van de werkgroepdocent. Niet (tijdig) inleveren telt als een 0 (nul).
Er is geen herkansingsmogelijkheid voor de in te leveren opgaven.
Joost Joosten,
jjoosten@wins.uva.nl (BG 438, 030-2535579)
vanaf 29-9-2000:
Dimitri Hendriks
Huiswerkopgaven
Week 4 (in te leveren op donderdag 5 oktober)
Geef een voorbeeld van een bewijsnormalisatie stap
op een natuurlijke deduktie bewijs.
Op college is het volgende voorbeeld behandeld (overeenkomend
met de lambda-term II), waarin ... alleen ter vulling gebruikt zijn:
----------------------------(var).....------------------(var)
x : phi->phi |- x : phi->phi..........y : phi |- y : phi
--------------------------------(->I) ------------------(->I)
|- \x.x : (phi->phi)->(phi->phi)......|- \y.y : phi->phi
--------------------------------------------------------(->E)
|- (\x.x)(\y.y) : phi->phi
Normaliseert naar
------------------(var)
y : phi |- y : phi
------------------(->I)
|- \y.y : phi->phi
(we willen phi->phi bewijzen, mbv het bewijs van x : phi->phi |- x : phi->phi
waarin alle voorkomens van de (var) regel voor x vervangen zijn door
het bewijs van |- \y.y : phi->phi. Het bewijs van x : phi->phi |- x :
phi->phi bestaat slechts uit die ene var-regel dus wordt die
in z'n geheel vervangen door het bewijs van |- \y.y : phi->phi.)
Beschouw intuitionistische geldigheid van
de volgende (klassiek geldige) formules:
(p->q)->(~q->~p)
(~p->~q)->(q->p)
Geef voor beide formules een bewijs in Coq, waarbij
Classical alleen gebruikt mag worden in geval van een niet
intuitionistisch geldige formule.
Hint: schrijf ~p expliciet uit als p->False of
gebruik Unfold not voor een Goal met voorkomens van ~ die
je wilt uitvouwen of Unfold not in H voor datzelfde
in de hypothese H.
De False eliminatieregel kan aangeroepen worden door Apply False_ind.
In het geval een formule niet geldig is dient dit bewezen
te worden mbv zowel een Kripke model als mbv de subformule eigenschap.
bewijs dat (zelfs al in ongetypeerde lambda-calculus) iedere
beta normaalvorm N van de vorm \x1\x2..\xn.yN1...Nm is,
waarbij n,m >= 0, x1,...,xn,y variabelen en N1,...,Nm weer normaalvormen zijn.
Week 5 (in te leveren op woensdag 11 oktober, zie
onderaan de pagina voor info over zowel het college als het pracicum van deze
week)
Nota bene: Coq bewijzen dienen stap voor stap geleverd te worden. Auto en Tauto
e.d. zijn niet toegestaan.
bewijs dat het predikaat SC gesloten is onder reductie, dwz
als M in SC en M ->beta N dan ook N in SC
(`subject reductie voor SC').
Neem aan:
Variable A : Set.
Variable R : A->A->Prop.
Definition R_refl := (x:A)(R x x).
Definition R_symm := (x,y:A)(R x y)->(R y x).
Definition R_eucl := (x,y,z:A)(R x y)->(R x z)->(R y z).
Bewijs:
Lemma opgave3 : R_refl -> R_eucl -> R_symm.
(* Met Compute. kun je de normaalvorm laten uitrekenen;
dat betekent hier niets anders dan bovenstaande definities te expanderen.
*)
College onderwerpen (per college).
(samenvattingen verschijnen na de college's).
intro typentheorie (blz 1 t/m 8)
lambda-calculus :
variabelen v0,v1,v2,... (oneindig veel),
applicatie MN,
abstractie \x.M (we schrijven hier \ ipv een lambda)
haakjes-conventies :
associeren naar links van applicatie,
scope van abstractie zo ver mogelijk naar rechts,
buitenste haakjes weglaten
voorbeeld : z\x.yx = (z(\x.(yx)))
variabelen :
vrije/gebonden variabelen van een term,
voorbeeld : FV(z\x.y\z.\y.x) = { z,y }
herbenoemen van gebonden variabelen (alpha-conversie)
voorbeeld : \x.xx =alpha \y.yy
rekenen : de beta-regel
(\x.M)N ->beta M[x:=N]
(het uitrekenen van de applicatie van een functie (\x.M) op
z'n argument (N), bestaat uit het substitueren (M[X:=N]) van
het argument (N) voor alle voorkomens van de variabele (x)
in de functie-body (M))
voorbeeld : (\x.x+5)4 ->beta (x+5)[x:=4] = 4+5
(even aannemende dat +, 5 en 4 in de lambda-calculus zouden zitten)
voorbeeld : (\x.xx)(\x.xx) ->beta (\x.xx)(\x.xx)
reduktie als rekenen (blz. 8 t/m 14)
resultaat = normaalvorm : een term die niet verder reducteert
uniek resultaat van beta-reductie (als het bestaat)
def: diamond-property van -> :
als M -> N en M -> P, dan is er een Q zdd N -> Q en P -> Q
->beta heeft niet de diamond-property, bekijk (\x.xx)(II)
(verdubbeling) of zelfs II (lege stappen)
lemma: ->>l (parallelle beta-reductie) heeft de diamond property
lemma: ->beta bevat in ->>l bevat in ->>beta
(iedere gewone beta stap is een speciaal geval van een parallelle stap, en
iedere parallelle stap kun je simuleren door een rijtje gewonen stappen)
def: Church-Rosser (CR) eigenschap van -> :
als M ->> N en M ->> P, dan is er een Q zdd N ->> Q en P ->> Q
stelling: ->beta heeft de CR eigenschap
(want ->>beta heeft de diamond property, want ->>l heeft de
de diamond property)
gevolg: lambda-calculus is consistent
dwz niet ieder tweetal termen is beta-convertibel
def: M beta-convertibel met N als er een rijtje van voor- en achterwaartse
beta-stappen is van M naar N. notatie M =beta N
def: Strongly Normalising (SN) : een term die geen oneindige reductierij toelaat
def: Weakly Normalising (WN) : een term die naar een normaalvorm kan reduceren
dekpunten van functies: x heet een dekpunt van f als f(x) = x
voorbeeld: f(n) = n^2, heeft 0 en 1 als dekpunten, f(n) = n+1 heeft geen dekpunten
voor lambda-calculus : N heeft een dekpunt van F als F N =beta N
stelling: iedere lambda calculus term heeft een dekpunt
bewijs:
stel: we zoeken een dekpunt N van F, dwz zdd F N =beta N
merk op: N zal af moeten hangen van F, dus stel N = Y F, voor zekere Y
dan zoeken we dus een Y zdd F (Y F) =beta Y F
idee 1: zoek een Y zdd Y F ->>beta F (Y F), dwz Y krijgt als input F
en daaruit willen we F (Y F) maken
dat kan door te nemen Y = \f.f (Y f), maar het probleem is nu dat
Y mbv zichzelf gedefinieerd is, anders gezegd Y moet zichzelf kunnen reproduceren
idee 2: Y kan zichzelf reproduceren als Y bestaat uit twee identieke
delen, dwz Y = A A, waarbij de eerste kopie van A het echte werk
doet en de tweede A er alleen is om Y (= A A) te kunnen reproduceren
concreet willen we dan A A = \f.f (A A f), en dan volstaat het
om A = \a.\f.f (a a f) te nemen
voorbeeld: Y x = A A x = (\a.\f.f (a a f)) A x ->beta
(\f.f (A A f)) x ->beta x (A A x) = x (Y x)
dus Y x is een dekpunt van de variabele x
(dus zelfs variabelen hebben dekpunten)
merk op: net als (\x.xx)(\x.xx) heeft de dekpunts operator Y = AA
de vorm van een term toegepast op zichzelf
denk na over zelf-applicatie
rekenkracht van lambda-calculus (blz 14 t/m 17)
aan dekpunten kan als volgt gedacht worden:
zie termen even als bomen
knopen zijn gelabeld met variabelen x (geen zonen), abstracties
\x (een zoon) en applicaties (twee zonen)
we zoeken een `boom' N zdd F N = N.
dit kan niet want F N zal altijd groter zijn dan N
(F N heeft tenminste 2 knopen extra tov N)
het kan echter wel als N een oneindige boom mag zijn
vd vorm F(F(F(....))).
Een oneindige boom kunnen we niet direct als lambda-term
maken (want lambda-termen zijn eindig), maar
we kunnen wel een lambda-term maken die die oneindige
lambda-term genereert. dat is precies wat Y F (zie boven) doet.
voorbeeld in functionele talen zeroes = 0 : zeroes
is een definitie van de (potentieel) oneindige lijst van nullen.
Dus zeroes voldoet aan,
zeroes = (\x.0 : x) zeroes , oftwel
zeroes is een dekpunt van (\x.0 : x) ,
oftewel zeroes = Y (\x.0 : x)
let x = M in N in een functionele taal kan
(in eerste benadering) vertaald worden in de lambda-calculus als (\x.M)N
letrec x = M in N in een functionele taal kan
(in eerste benadering) vertaald worden in de lambda-calculus als (\x.N)(Y\x.M)
alle recursieve functies kunnen in de lambda-calculus uitgedrukt worden.
een recursieve functie is een functie van natuurlijke getallen
naar natuurlijke getallen die opgebouwd is mbv zgn initiele functies
natuurlijke getallen willen we representeren als
(verschillende, dus niet beta-convertibele) beta-normaalvormen
representaties van natuurlijke getallen worden numerals genoemd
een keuze om het getal n te representeren als lambda-term,
is om n te representeren/coderen als het n keer herhalen van een
functie op z'n argument : c_n = \fx.f^n(x)
waarbij we definieren f^0(x) = x en f^n+1(x) = f(f^n(x))
dus als nul krijgen we dan c_0 = \fx.f^0(x) = \fx.x
de successor (+1) functie S+ moet voldoen aan S+ c_n = c_n+1
S+ neemt een argument en is dus van de vorm
\n.... het resultaat moet weer een numeral zijn, dus weten
we dat S+ van de vorm \nfx.... moet zijn.
verder weten we dat c_n f x ->>beta f^n(x) en daaruit
kunnen we f^n+1(x) krijgen door er een f voor te zetten
zogezegd zo gedaan: S+ = \nfx.f(n f x)
optellen A+ moet voldoen aan A+ c_m c_n = c_m+n
volgens eenzelfde redenering als boven kunnen we A+ definieren als
\mnfx.m f (n f x)
in de lecture notes wordt dit verder uitgewerkt
Een voorbeeld van een lambda-definieerbare functie, de faculteit-functie.
Deze kunnen we specificeren mbv de code x! = if x=0 then 1 else x.(x-1)!
We werken deze code nu naar een lambda-term om
1 coderen we als de numeral 1, dwz \sx.sx
. coderen we als A* de vermenigvuldiging (zie reader)
if_then_else_ is een functie van drie argumenten,
een boolean en twee functies: if T then M else N = M if F then M else N = N
als we T representeren als K (= \xy.x),
F als K* (= \xy.y) en
if_then_else_ als \xyz.xyz dan werkt dat.
iha is het niet beslisbaar of twee termen beta-convertibel zijn,
maar de test of een numeral gelijk aan 0 is ( x=0 )
kan uitgevoerd worden:
de numeral nul is \fx.x en de andere numerals zijn
vd vorm \fx.f(f(...(x)...)), dus als we voor x
T kunnen invullen en voor f de konstante F functie, dan werkt dat.
Dwz x=0 kunnen we implementeren als
(\n.n (\x.F) T)x met T en F als in het voorgaande onderdeel.
de predecessor functie (x-1) is lastig om te maken.
wat we wel kunnen doen is een tabel maken die alle paren
[n,n-1] genereert: [0,0], [1,0], [2,1], [3,2], ... mbv een functie
die zo'n paar in z'n opvolger transformeert.
als we die functie dan n maal herhalen op het eerste paar
levert dat het paar [n,n-1] op, waaruit we het resultaat halen
door op het tweede argument te projecteren.
Dwz definieer
NEXT = \p.if ((pi1 p) = 0) then [1,0] else [S+ (pi1 p),(pi1 p)]
waar [M,N] staat voor (\mnz.zmn) M N,
en pi1 voor \x.xK en pi2 voor \x.xK*.
Dan kunnen we definieren P- = \n.pi2 (n NEXT [0,0]).
Een voorbeeld (gebruikmakend van vele afkortingen) :
P- 1 ->
pi2 (1 NEXT [0,0]) ->
pi2 (NEXT [0,0]) ->
pi2 (if ((pi1 [0,0] = 0) then [1,0] else [S+ (pi1 [0,0]),(pi1 [0,0])]) ->>
pi2 (if (0 = 0) then [1,0] else [S+ 0,0]) =
pi2 ((\n.n (\x.F) T) 0) then [1,0] else [S+ 0,0]) =
pi2 (if 0 (\x.F) T then [1,0] else [S+ 0,0]) ->>
pi2 (if T then [1,0] else [S+ 0,0]) =
pi2 ((\bmn.bmn) T [1,0] [S+ 0,0]) ->>
pi2 (T [1,0] [S+ 0,0]) ->>
pi2 [1,0] ->>
0
dit is niet extreem efficient, maar het werkt wel!
We kunnen nu de hele faculteit functie coderen op de recursie na, maar
die kunnen we met mbv de dekpunts-operator Y aan. x! = .... M! .... , dus ! = \x. .... M! .... , dus ! = (\fx. .... (f M) ....) ! , dus ! = Y (\fx. .... (f M) ....)
waarbij de .... staan voor het deel van de code behalve
de recursieve aanroep.
typen a la curry (blz. 41 t/m 45)
een simpel type is ofwel een basis-type uit B (denk aan natuurlijke
getallen, booleans etc.) ofwel een functie-type sigma -> tau
waar sigma en tau zelf weer simpele typen zijn.
voorbeelden : nat en nat -> (nat -> nat) en
(nat -> bool) -> bool zijn alle drie typen.
variabele hebben een willekeurig typ
in een applicatie M N is M de functie en N het argument,
dus moet M een functie-type hebben, zeg sigma -> tau en
dan moet N van type sigma zijn.
een abstractie \x.M moet een functie type, zeg sigma -> tau.
Aangezien M de body/het resultaat van de functie is moet
M dan ook type tau hebben. De voorkomens van x in
M moeten allemaal het type sigma hebben.
De algemene typerings regels kunnen in de lecture notes gevonden worden.
\x.x is typeerbaar als sigma -> sigma voor een willekeurig type sigma,
bv \x.x : nat -> nat, maar ook \x.x : (nat -> nat) -> (nat -> nat)
\x.xx is niet typeerbaar want xx is een applicatie, dus de eerste
x is van type sigma -> tau en de tweede x van type sigma voor zekere
types sigma en tau, maar x heeft slechts een type, wat zou
betekenen dat sigma -> tau = sigma, wat niet kan omdat typen
eindig zijn.
subject reductie eigenschap voor simpel getypeerde lambda-calculus:
Gamma |- M : sigma en M ->>beta N dan Gamma |- N : sigma
inductief bewijs van subject reductie met benodigde lemmas
gebruikte bewijsmethoden:
inductie naar afleiding van typering,
inductie naar termen,
inductie naar definitie van beta
gevolg : confluentie van simpel getypeerde lambda calculus
WN eigenschap voor simpel getypeerde lambda-calculus:
als Gamma |- M : sigma, dan M ->>beta N voor zekere normaalvorm N.
bewijs van WN mbv methode van Turing:
laat het type van een redex (\x.M)N het type van (\x.M) zijn,
zeg sigma -> tau
door het redex (\x.M)N te reduceren worden sommige redexen
gekopieerd, maar evt gecreeerde redexen hebben een kleiner
type dan het redex zelf:
sigma voor naar boven toe gecreeerde redexen (door `de wortel' van M) en
tau voor naar beneden toe gecreeerde redexen (`combinaties' van M en N)
als we nu steeds een binnenste redex van zo groot mogelijk type
reduceren dan stopt dit proces.
typen a la church (blz. 45 t/m 52 (53 alleen intuitief))
typen hetzelfde als voor Curry, maar in abstracties is de variabele
een type (domein van de functie wordt gespecificeerd)
meta theorie a la Church is analoog aan die voor Curry, maar
door andere syntax zijn we gedwongen alles over te doen,
hoewel alles bijna hetzelfde gaat...
oplossing: projection en lifting lemma's die beta-reducties a la Church
relateren aan beta-reducties a la Curry en vice versa
gevolg: SN en WN voor Curry impliceren SN en WN voor Church
eigenschap van Church die Curry niet heeft: uniqueness of types, dwz
iedere term heeft een uniek type wat onveranderlijk is onder beta-conversie
(dwz zowel beta-reductie (is al waar voor Curry) als beta-expansie)
vraagstellingen: (blz 89)
type-checking: Gamma |- M : sigma ?
type-inhabitation: Gamma |- ? : sigma
type-reconstruction: Gamma |- M : ?
(blz. 23 t/m 27, 34 t/m 37 + Rieger-Nishimura)
De Brouwer-Heyting-Kolmogorov interpretatie van de logische operatoren;
constructies met bewijzen.
Introductie van Intuitionistische Propositionele logica (IPC). Ook hebben
wij gezien dat dit geheel conform de BHK interpretatie is.
In klassieke propositionele logica kun je met een variabele slechts
vier niet equivalente formules maken. In een constructivistische setting
kunnen er oneindig veel niet equivalente formules worden gegeven met
slechts een variabele. De structuur van deze zinsverzameling heet het
Rieger-Nishimura rooster.
Kripke semantiek voor IPC is gegeven. De =< relatie is intuitief
zoiets als een verwijzing naar toekomstige werelden.
Kripke semantiek is gezond en volledig tov IPC
We hebben laten zien dat de volgende twee zinnen niet bewijsbaar zijn
in IPC:
(A->B)\/(B->A) en
(A\/-A)
Curry-Howard isomorfisme (blz. 63 t/m 68 en 71,72)
Drie soorten afleidingssystemen voor logica's (niet in reader, wel kennen)
natuurlijke deduktie bewijzen (als boven):
voor ieder connectief een introductie en een eliminatieregel
bewijzen zijn bomen
sequenten-calculi:
voor ieder connectief een linkse- en een rechtse introduktieregel
bewijzen zijn bomen.
linkse regel = introductie in de context, rechtse regel = introduktie
in de conclusie
frege-hilbert stijl:
axioma's voor connectieven en als enige afleidingsregel modus ponens
(voor eerste orde logica ook `voor alle' regel)
bewijzen zijn meestal lijsten van formules
introduktieregels van natuurlijke deduktie komen overeen met
de rechtse introduktie regels van sequenten calculus
bewijsnormalisatie voor natuurlijke deduktie:
een introduktie regel voor een connectief, onmiddellijk gevolgd
door een eliminatie regel voor datzelfde connectief is een
nodeloze omweg: die omweg kan ingekort/genormaliseerd worden
inkorten heet `bewijs normalisatie', en de precieze vorm hangt af
van de regels voor het desbetreffende connectief
bewijs normalisatie voor implicatie met conclusie Gamma |- psi
beginned met bewijzen Gamma,phi |- psi en Gamma |- phi
bestaat uit het substitueren van `Gamma |- phi' op alle
plaatsen in Gamma,phi |- psi waar de variabele regel voor phi wordt gebruikt
bewijs normalisatie voor implicatie komt exact overeen (is isomorf met)
met beta reductie in lambda-calculus.
Sterker : de afleidingsregels voor getypeerde lambda calculus
ontstaan uit de natuurlijke deduktie regels voor IPC door
ze te `voorzien van lambda-termen'
gevolg : bewijsnormalisatie is WN (en ook SN), want beta-reduktie
voor getypeerde lambda-calculus is dat
stelling (subformule eigenschap) : als Gamma |- phi afleidbaar is
dan is er een (normaal) bewijs waarin alleen subformules van
Gamma of phi voorkomen.
bewijs is gebaseerd op de volgende karakterisering van beta-normaalvormen:
N = \x1...xn.yN1...Nm, met n,m >= 0 en Ni weer in normaalvorm
het CH-isomorphisme tussen combinatorische logica en hilbert-frege-stijl IPC
(blz. 75 t/m 83)
combinatorische logica (CL) : termen opgebouwd uit variabelen, S, K mbv applicatie.
de equivalentie van CL-termen wordt gegenereerd door regels :
SMNP -> MP(NP)
KMN -> M
vertaling (_)_CL van lambda-termen naar CL termen mbv abstractie-algoritme :
\x.M wordt vertaald als \*x.M, waarbij \*x.M gedefinieerd wordt door
\*x.x = SKK
\*x.M = KM, als x niet in FV(M)
\*x.MN = S(\x*.M)(\x*.N), anders
er geldt niet: als M =beta N, dan (M)_CL =CL (N)_CL
bv. \x.II =beta \x.I, maar niet S(KI)(KI) =CL KI, want
CL is Church-Rosser (Stelling) en de linker- en rechterkant zijn
verschillende normaalvormen.
opmerking: convertibiliteit geldt wel als
Curry's axioma's aan de regels van CL toegevoegd worden.
vertaling (_)_Lambda van CL-termen naar lambda-termen:
(S)_Lambda = \xyz.xz(yz)
(K)_Lambda = \xy.x
(MN)_Lambda = ((M)_Lambda (N)_Lambda)
stelling : als M =CL N, dan (M)_Lambda = (N)_Lambda,
ook geldt ((M)_CL)_Lambda =beta M, voor lambda-termen M (niet op college behandeld)
Hilbert-Frege stijl bewijzen zijn opgebouwd uit axioma's en modus ponens.
Voor minimale logica zijn de axioma's van HF-stijl bewijzen:
------------------------------------------------------------(S)
|-HF S : (alpha->beta->gamma)->(alpha->beta)->(alpha->gamma)
en
---------------------------(K)
|-HF K : alpha->beta->alpha
(het zijn eigenlijk axioma schema's want willekeurige formules mogen voor
alpha, beta en gamma ingevuld worden)
stelling : als Gamma |-ND M:sigma, dan Gamma |-HF (M)_CL:sigma
bewijs: met inductie naar afleiding. de (var) en (->E)-regel zijn makkelijk.
voor de (->I)-regel moeten we de deduktie-stelling toepassen.
deduktiestelling : als Gamma,sigma |-HF tau, dan Gamma |-HF sigma->tau
bewijs: men bewijst als Gamma,x:sigma |-HF M:tau, dan Gamma |-HF \*x.M:tau,
met inductie naar M, waar \*x.M het boven beschreven abstractie-algoritme is.
het lastigste geval is wellicht nog te checken dat inderdaad
|-HF SKK : alpha -> alpha.
stelling : als Gamma |-HF M:sigma, dan Gamma |-ND (M)_Lambda : sigma
bewijs: triviale inductie naar afleiding.
conclusie : HF (Hilbert-Frege) en ND (Natuurlijke Deduktie) zijn even
krachtig qua bewijskracht
Bewijs van sterke normalisatie van simpel getypeerde lambda calculus
(Postscript,
PDF)
Coq opgaven week 5
(Postscript,
PDF) met een
toelichting
in tekst-vorm op symmetrie van Leibniz-equality.
Polymorfe lambda calculus (= System F = lambda 2)
(blz. 191 t/m 193, 196 t/m 201, 203, 204, 207 en impredikativiteit)
(dit systeem is bedacht zowel in de wereld van de logica als in de
wereld van het programmeren (lambda-calculus), vandaar de verschillende
namen. het CH-isomorfisme zegt dat deze werelden eigenlijk hetzelfde zijn.)
Polymorfe lambda calculus heeft kwantificatie over types.
dwz als alpha een type-variabele is, dan is A alpha.tau weer
een type (waarbij A staat voor `voor alle')
de lambda-term die overeenkomt met voor-alle introductie is
/\alpha.M en de lambda-term die overeenkomt met voor-alle eliminatie
is M tau
het heet polymorfe lambda calculus omdat het overeenkomt met polymorfie
in bepaalde programmeertalen. je kunt bv in C++ een procedure schrijven
die lijsten concateneert voor een willekeurig type (voor-alle introductie)
en dan vervolgens die procedure gebruiken om, zeg, lijsten van natuurlijke
getallen te concateneren (voor-alle eliminatie)
bewijs-normalisatie in deze 2de-orde logica komt overeen met de B regel:
(/\alpha.M)tau ->B M[alpha:=tau]
polymorfe lambda calculus is impredikatief in de zin dat
om de betekenis van A alpha.tau te bepalen we alle mogelijke
typen voor alpha in tau moeten invullen, maar daar zit A alpha.tau zelf
weer tussen...
iha heet een definitie van een object impredikatief als het object
gedefinieerd is mbv een verzameling waar het zelf inzit.
andere voorbeelden van impredikatieve definities:
least upperbounds, dwz het kleinste element van de verzameling
van bovengrenzen van een verzameling
de verzameling R = { x | x niet in x } (de Russell Paradox)
merk op: impredikatieve definities kunnen dus gevaarlijk zijn
polymorfe lambda calculus is nogal expressief
logische connectieven kunnen gedefinieerd worden: _|_ = A alpha.alpha,
phi /\ psi = A alpha.(phi->psi->alpha)->alpha, etc.
en de bewijstermen vertonen het gewenste normalisatie gedrag...
natuurlijke getallen kunnen gedefinieerd worden:
N = A alpha.(alpha->alpha)->alpha->alpha
lijsten over sigma kunnen gedefinieerd worden
L = A alpha.(sigma->alpha->alpha)->alpha
iha kunnen data-types gecodeerd worden door de types van de constructoren
van zo'n data-type op te sommen (en te verbinden door ->)
bv N = A alpha.(type van successor)->(type van nul)->alpha
(maar de volgorde maakt niet uit,
dus N' = A alpha.alpha->(alpha->alpha)->alpha is ook een prima type
voor N)
ook machtsverheffen kan uitgedrukt worden, dus er is (veel) meer uitdrukbaar
in system F dan in simpel getypeerde lambda calculus
werkgroep opgaven: 12.7.4, 12.7.13, 12.7.12,
is er een bijectie tussen de gesloten bewoners van
A alpha. alpha->(alpha->alpha)->alpha en
A alpha. (alpha->alpha)->alpha->alpha?
de lambda-kubus: kubus die ontstaat door te parametriseren over mogelijke
afhankelijkheden tussen termen en typen
(blz. 209 t/m 215)
een parametrisatie S bestaat uit paren (s1,s2) met (si in {*,[]}):
(*,*) termen hangen af van termen, \x.M levert
een term op bij een term als input, i.e. simpel getypeerde
lambda calculus
([],*) termen hangen af van typen, /\alpha.M levert
een term op bij een type als input, i.e. system F
(*,[]) typen hangen af van termen, \n.List(n) levert
een type op bij een term als input, onder het CH-isomorphisme
is dit predikaten-logica.
de calculus of constructions heeft alle vier afhankelijkheden
(de calculus of inductive constructions waarop Coq gebaseerd is een
uitbreiding nog weer van de calculus of constructions, oa met inductieve
types)
het enige axioma in de lambda kubus is |- *:[]. hiernaar worden alle
andere judgments herleid.
objecten mogen niet zomaar geintroduceerd worden, ze moeten ergens
in leven, dus bv om x : alpha af te leiden, moet alpha zelf weer
goed gevormd zijn, dwz alpha : * moet afgeleid worden om uiteindelijk
uit te komen op |- * : [], het enige axioma.