Oppstart 23/8-05 i B 62, Niels henrik Abels hus.
Tid: Tirsdag 12.15 - 15.00
Det er nå lagt ut deler av kompendiet på følgende adresser:
Full vesjon. Her finner dere nå
kompendiet i den form det vil ha de nærmeste ukene.
Jeg har nå ingen planer om å gjøre andre endringer enn
å rette opp trykkfeil.
Kapittel 1 Utypet λ-kalkyle.
Kapittel 2 En λ-kalkyle for endelige typer.
Kapittel 3 Gödels T.
Kapittel 4 System F.
Kapittel 5 Domeneteoriens ene opprinnelse.
Kapittel 6 Plotkins PCF.
Kapittel 7 Kleene-Kreisels funksjonaler.
Kapittel 8 En modell for System F.
[Dette kapitlet er ikke rettet opp til sin endelige versjon.]
Innledning Her vil innholdsfortegnelse, tittelside og forord ligge i sist oppdaterte versjon. Disse sidene er nå foreldet.
Bibliografi og register. Her vil et til enhver tid oppdatert register og bibliografien foreligge. Det vil være feil i dette registeret i forhold til siste versjon.
Tillegg. Dette kapitlet vil ha tilleggstoff som ikke vil bli del av pensum.
30/8 innførte vi Church numeraler og λ-definerbarhet, og viste at etterfølger, definisjon ved tilfeller og forgjengerfunksjonen er λ-definerbare.
6/9 gikk vi først gjennom avsnittet om kombintorer, og definerte
deretter hva vi mener med en typeteori over endelige typer.
Vi har nådd frem til normaliseringsteoremet.
13/9 gikk vi gjennom beviset for sterk normalisering for kjerneeksemplet
av en kalkyle over de endelige typene.
Vi oppdaget at avslutningen av beviset ikke var kommet med i
manuskriptet. Dette blir nå rettet opp, og beviset er med i den versjonen
som legges ut i løpet av dagen (14/9-05).
Vi rakk ikke å gå gjennom noen oppgaver.
20/9 beskrev vi den naive mengdeteoretiske semantikken for endelig typeteori. Deretter begynte vi på motivasjonen for Gödels T.
27/9 ga vi den formelle innføringen i Gödels T. Vi så også på hvordan typer på et nivå kan embeddes inn i de rene typene av minst samme nivå.
4/10 så vi på begreper som konsistens, adekvathet og full abstraksjon, og viste at det finnes en fullt abstrakt modell for T.
11 - 25/10 gikk vi igjennom Kapittel 4 om System F.
25/10 startet vi på Kapittel 5.
1/11 startet vi på domeneteorien, frem til definisjonene av kontinuerlige og algebraiske domener.
8/11 gikk vi igjennom idealkompletteringen av en partiell ordning, og vi gikk igjennom konstruksjonen av funksjonsrom for begrenset komplette algebraiske domener.
Sist oppdatert av Dag Normann 14/11-05