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 02-03

Typentheorie 02-03

Tekst studiegids

Werkgroep/Praktikum/Huiswerk info

Cursus literatuur

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.

Aanvullende literatuur

Philip Wadler, Proofs are Programs: 19th Century Logic and 21st Century Computing
het Curry-Howard isomorfisme in vogelvlucht
Benjamin Pierce, Types and Programming Languages, MIT Press
typen bezien vanuit een programmeer perspectief.
H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics. North Holland (Een samenvatting is hier)
de `bijbel' van de (ongetypeerde) lambda-calculus
Twan Laan, The evolution of type theory in logic and mathematics, PhD thesis
interpretatie van het onstaan van typen in een modern kader, met historische kanttekeningen
J.-Y. Girard, Y. Lafont, P. Taylor, Proof and Types, Cambridge University Press
compacte, elegante en dichte neerslag van een cursus getypeerde lambda calculus van Girard
P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis
Ook een neerslag van een cursus, ditmaal van Martin-Löf

Vorm

Iedere week kunnen er opgaven ingeleverd worden. Vanaf de vierde 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.

Inhoud

19-11-2002: historische achtergrond
- historische achtergrond: Frege Begriffschrift, Russell paradox
- analyse van probleem: funktionele abstractie, zelf applicatie
21-11-2002: ongetypeerde lambda-calculus
- Church's (ongetypeerde) lambda-calculus (Secties 1.1 en 1.3)
- alternatieve (inductieve) definitie van alpha-equivalentie
26-11-2002: reductie
- beta-reductie (Sectie 1.2)
- expressiviteit van lambda-calculus (Sectie 1.5) representatie van natuurlijke getallen (als Church_numerals) en eenvoudige operaties (0, successor)
28-11-2002: expressiviteit
- vervolg expressiviteit (Sectie 1.5): representatie van primitief recursieve functies mbv tabellen
- confluentie (de Church-Rosser eigenschap) van beta-reductie (Sectie 1.4); gevolg unieke normaalvormen (`resultaten')
3-12-2002: getypeerde lambda-calculus
- vervolg expressiviteit (Sectie 1.5): representatie van recursieve functies (minimalisatie) mbv if-then-else en de fixed-point operator
- introductie van typen
- simpel-getypeerde lambda-calculus a la Curry (Sectie 3.1)
5-12-2002: type-reconstructie (Secties 6.3 en 6.4) en
- type reconstructie: gegeven term M, zijn er context Gamma en type tau zo dat Gamma |- M : tau ?
- algoritme `verzamelt' constraints E_M op de typen tau_M van subtermen van een term, langs de afleidingsboom:
  - variabelen: leveren geen constraints op (we werken zonder basistypen)
  - \x.M heeft als constraints E_M en { tau_\x.M = tau_x -> tau_M }
  - MN heeft als constraints E_M, E_N en { tau_M = tau_N -> tau_MN }
- algoritme levert meest algemene (principal) type
- Voorbeeld van een bewijs met inductie naar een afleiding (het generation lemma 3.1.6 voor lambda-Curry)
- Definitie van lambda-Church 3.2
- Bewijs van terminatie (Sterke Normalisatie, SN) van de lambda calculus (in PDF en in PS)
12-12-2002: intuitionistische logica
- informele introductie (Sectie 2.1)
- verschillende soorten semantiek
  - axiomatische semantiek : axioma's die de semantiek karakteriseren
    (voordeel: calculeren/algebra; nadeel: modellen worden wel gekarakteriseerd, maar bestaat er ueberhaupt een niet-triviaal model?)
  - denotationele semantiek : semantiek gedefinieerd met recursie over de inductief gedefinieerde syntax; associeert functies/functionalen over een domein met syntactische operatoren
    (voordeel: inductie; nadeel: inductie; wiskundige domeinen vaak niet begrijpelijk voor gebruiker)
  - operationele semantiek : betekenis van een programma gegeven mbv de stappen die het kan doen
    (voordeel: ziet wat er gebeurt; nadeel: vaak laag abstractieniveau)
- Kripke semantiek (denotationeel) van intuitionistische logica (Sectie 2.5)
17-12-2002: afleidingssysteem voor intuitionistische logica (Sectie 2.4)
19-12-2002: correctheid en volledigheid van afleidingssysteem voor intuitionistische logica tov kripke semantiek
- correctheid: bewijs met inductie naar afleiding dat als Gamma |- phi dan Gamma ||- phi
- volledigheid (voor minimale logica): (Theorem 2.6.1)
8-1-2003:
- CH-isomorphisme (4.2)
- subformule eigenschap voor implicationele fragment van intuitionistische logica
- hilbert-frege afleidingssysteem (begin) (5.1-5.3)
- combinatorische logica (CL), termen en regels
- vertalingen van combinatorische logica naar lambda calculus en terug
- (non-)behoudseigenschappen van de vertalingen, ihb beta-reductie wordt niet noodzakelijk op CL-reductie afgebeeld, maar wel andersom, en ((M)_CL)_Lambda =_beta M, voor iedere lambda term M.
CH-isomorfisme, variatie op stellingen: expressievere lambda-calculi (System F, Goedel's T, Calculus of Constructions) en corresponderende logica's.
...

Docent (Hoorcolleges)

Vincent van Oostrom, Vincent.vanOostrom at phil.uu.nl (BG 441a, 030-2532761)

Assistent (Werkgroepen en Praktica)

Sander Bruggink, Sander.Bruggink at phil.uu.nl (BG 443, 030-2537780)
Alle gegevens over de werkgroepen en het praktikum kun je hier vinden.

Uitwerking van de eindopdracht

Coq broncode bubblesort.v voor bubblesort
- constructief bewijs van het bestaan van een in oplopende volgorde gesorteerde lijst voor iedere eindige lijst van natuurlijke getallen, zodanig dat de oorspronkelijke en de gesorteerde lijst equivalent zijn
- equivalentie van twee lijsten is gedefinieerd als: hun onderliggende multisets zijn hetzelfde. de broncode maakt alleen gebruik van een interface voor multisets, waarvan twee implementaties meegeleverd zijn (zie onder)
- coqqen van de file levert een bubblesorteer programma (de witness voor het eerste onderdeel)
Coq implementatie std_multiset.v van de multiset interface van sorteren, gebruikmakend van multisets uit de standaard coq library
Alternatieve Coq implementatie res_multiset.v van de multiset interface van sorteren, gebruikmakend van multisets gebaseerd op residu theorie zoals beschreven in het boek Term Rewriting Systems.
(zie het begin van de bubblesort.v broncode om van res ipv std gebruik te maken)
ML functioneel programma Bubblesort.ml gegenereerd door eerst coqtop en dan Load bubblesort. in te typen.
(tot coq 7.2 wordt het suffix .ml niet gegenereerd)
Haskell functioneel programma Bubblesort.hs gegenereerd als in het vorige onderdeel, na selectie van haskell als Extraction Language
(zie het einde van de bubblesort.v broncode voor de wijziging die nodig is om het Haskell ipv ML programma te laten extraheren, Haskell extractie beschikbaar vanaf coq 7.2)

Haskell functioneel testprogramma Test.hs. Wrapper voor Bubblesort.hs.
Voorbeeld van gebruik:

hugs Test
__   __ __  __  ____   ___      _________________________________________
||   || ||  || ||  || ||__      Hugs 98: Based on the Haskell 98 standard
||___|| ||__|| ||__||  __||     Copyright (c) 1994-1999
||---||         ___||           World Wide Web: http://haskell.org/hugs
||   ||                         Report bugs to: hugs-bugs@haskell.org
||   || Version: February 2000  _________________________________________

Haskell 98 mode: Restart with command line option -98 to enable extensions

Reading file "/phil/tf/share/hugs/lib/Prelude.hs":
Reading file "Test.hs":
Reading file "Bubblesort.hs":
Reading file "Test.hs":
                   
Hugs session for:
/phil/tf/share/hugs/lib/Prelude.hs
Bubblesort.hs
Test.hs
Type :? for help
Test> sort [5,10,9,8,8,6,3,2]
[2,3,5,6,8,8,9,10]
Test>