equationeel programmeren 2015 01 05 college 1
schema
praktische zaken opmerkingen vooraf lambda termen materiaal
schema
praktische zaken opmerkingen vooraf lambda termen materiaal
wie
• hoorcolleges:
Femke van Raamsdonk f.van.raamsdonk at vu.nl T446 • werkcolleges en practica:
Christian Ouwehand en Roy Overbeek
lessen • hoorcolleges:
week 2–5 maandag 11.00-12.45 in F654 donderdag 11.00-12.45 in hoofdgebouw 02A06 • werkcolleges:
week 2–5 dinsdag 11.00-12.45 in hoofdgebouw 04A05 vrijdag 11.00-12.45 in P647 • practica:
week 2–5 maandag 13.30-17.00 in P323 donderdag 13.30-17.00 in P323 zaalreservering (check welke zaal) voor ma, di, do, vr middag
toetsing • 3 (of 4) inleveropgaven programmeren • 4 inleveropgaven theorie • schriftelijk tentamen
vrijdag 30 januari 2015 • minimaal 5,5 voor de deelcijfers • geldigheid
deelcijfers zijn alleen dit jaar (2014-2015) geldig • eindcijfer
een 30% programmeeropgaven, 70% tentamen, ten hoogste 0,5 bonus voor theorie-opgaven op tentamencijfer
materiaal
• dictaat, slides, opdrachten • webpage van het vak • via web • extra
soms extra materiaal via slides en links (niet voor tentamen)
schema
praktische zaken opmerkingen vooraf lambda termen materiaal
equationeel programmeren
grondslagen van functioneel programmeren
functioneel programmeren
een functioneel programma is een expressie, en wordt uitgevoerd door de expressie te evalueren (gebruik definities van links naar rechts) focus op het wat en minder op het hoe de functies zijn puur (wiskundig) eenzelfde input geeft altijd dezelfde output
voorbeeld
in Haskell: sum [1 .. 100] in Java: total = 0; for (i = 1; i <= 10; ++i) total = total + i;
functioneel programmeren: eigenschappen
hoog abstractieniveau (meer) vertrouwen in correctheid (lezen, checken, correct bewijzen)
Lisp
Lisp John McCarthy (1927-2011), Turing Award 1971
ML
ML Robin Milner (1934-2010), Turing Award 1991, et al
Haskell
Haskell een groep met onder andere Philip Wadler en Simon Peyton Jones
functionele programeertalen
getypeerd
ongetypeerd
strict
ML
Lisp
lazy
Haskell
functioneel programmeren en lambda calculus
Based on the lambda calculus, Lisp rapidly became ... (uit: wikipedia page John McCarthy) Haskell is based on the lambda calculus, hence the lambda we use as a logo. (uit: the Haskell website) Historically, ML stands for metalanguage: it was conceived to develop proof tactics in the LCF theorem prover (whose language, pplambda, a combination of the first-order predicate calculus and the simply typed polymorphic lambda calculus, had ML as its metalanguage). (uit: wikipedia page of ML)
functioneel programmeren en algebra¨ısche specificaties
Programming languages with algebraic data types: Haskell, OCaml (geparafraseerd van wikipedia page van algebraic data type)
andere functionele programmeertalen
F# (Microsoft) Erlang (Ericsson) Scala (Java plus ML)
equationeel programmeren
• lambda calculus • algebra¨ısche specificaties • opdrachten functioneel programmeren: Haskell
schema
praktische zaken opmerkingen vooraf lambda termen materiaal
lambda calculus
bedenker: Alonzo Church (1936) fundament van de wiskunde fundering begrip ‘berekenbaar’ beperken tot functies basis van functioneel programmeren
notatie voor functies • wiskundig:
f : nat → nat f (x) = square(x) • ook wiskundig:
f : nat → nat f : x 7→ square(x) • lambda notatie:
λx. square x
lambda termen: intuitie
abstractie: λx. M is de functie die x afbeeldt op M λx. square x is de functie die x afbeeldt op square x applicatie: F M is de toepassing (niet het resultaat van het toepassen) van de functie F op zijn argument M
lambda termen: inductieve definitie
• variabele
x • constante
c • abstractie
(λx. M) • applicatie
(F M)
termen als bomen: voorbeeld
@ @
x
@ @
λx x
y
termen als bomen: algemeen
beroemde termen
I = λx. x K = λx. λy . x S = λx. λy . λz. x z (y z) Ω = (λx. x x) (λx. x x)
haakjes
• (M N P) in plaats van ((M N) P)
applicatie is associatief naar links • (λx. λy . M) in plaats van (λx. (λy . M)) • (λx. M N) in plaats van (λx. (M N)) • (M λx. N) in plaats van (M (λx. N))
nog meer notatie-vereenvoudigingen
• λxy . M in plaats van λx. λy . M • meer in het algemeen
λx1 . . . xn . M in plaats van λx1 . . . . λxn . M
lambda termen: voorbeelden
(λxyz. y (x y z)) λvw . v w (λxy . x x y ) (λzu. u (u z)) λw . w
inductieve definitie van termen
• definities met recursie naar de definitie van termen
voorbeeld: definitie van vrije variabelen van een term, straks • bewijzen met inductie naar de definitie van termen
voorbeeld: elke term heeft eindig veel vrije variabelen
lambda notatie • van verzameling naar predikaat: karakteristieke functie
χS (x) =
true als x ∈ S false als x 6∈ S
• van predikaat naar verzameling
P(x) = {x | P(x) = true} • Russell’s Paradox
R = {x | x 6∈ x} • Russell’s Paradox in lambda notatie
R = λx. ¬(x x) dan R R =β ¬(R R)
getypeerd en ongetypeerd
getypeerde lambda-calculus oa om paradoxen te vermijden hier: eerst ongetypeerd, later (simpel) getypeerd Haskell (en ML): getypeerd
termen in Haskell: getypeerd
zoals lambda termen maar getypeerd, bijvoorbeeld: sum : natlist → nat [1, 2] : natlist sum [1, 2] : nat
plus : nat → (nat → nat) 2 : nat plus 2 : nat → nat plus 2 5 : nat
3 : nat
termen in Haskell: meer primitieven
zoals lambda termen maar meer primitieven, bijvoorbeeld: 2 + 3 →δ 5 let x = s in t
gebonden variabelen: intuitie
x in de scope van λx is gebonden voorbeelden: de onderstreepte x is gebonden in λx. x λx. x x (λx. x) x λx. y x
vrije variabelen: definitie
• notatie:
FV(M) voor de verzameling van vrije variabelen in M • definitie:
FV(x) FV(c) FV(λx. M) FV(F P)
= = = =
{x} ∅ FV(M)\{x} FV(F ) ∪ FV(P)
• een voorkomen van een variabele is gebonden als het niet vrij is
alpha conversie
• alpha conversie:
gebonden variabelen mogen herbenoemd worden • voorbeeld:
λx. x =α λy . y • vergelijk:
f : x 7→ x 2 is f : y 7→ y 2 ∀x. P(x) is ∀y . P(y ) • identificatie van alpha-equivalente termen
we werken met equivalentieklassen modulo α
beta reductie: voorbeelden
• (λx. x) y →β y • (λx. x x) y →β y y • (λx. x z) y →β y z • (λx. z) y →β z
beta reductie regel: definitie
• (λx. M) N →β M[x := N] • hier is:
x een variabele M een term, en N ook [x := N] de substitutie van N voor x (moet gedefinieerd)
substitutie
• M[x := N] betekent:
vervang in M alle vrije voorkomens van x door N • α-conversie
wordt gebruikt om te voorkomen dat vrije variabelen in N gevangen worden • definitie met inductie naar termopbouw
substitutie: formele definitie
x[x y [x (λy . M0 )[x (M1 M2 )[x
:= N] := N] := N] := N]
= = = =
N y met x 6= y λy . (M0 [x := N]) met x 6= y en y 6∈ FV(N) (M1 [x := N]) (M2 [x := N])
beta reductie: definitie
een toepassing van de beta-reductie-regel ergens in een term
reductietheorie
redex sub-term van de vorm (λx. M) N reductiestap toepassing van beta-reductieregel in term reductierij 0, 1 of meer reductiestappen achter elkaar normaalvorm term waar geen β-reductie mogelijk is oftewel: term zonder redex
δ-reductie
• voor de voorbeelden gebruiken we soms contanten
voor sommige constanten zijn δ-regels • redexen:
β-redex (λx. M) N δ-redex plus 3 5 • reductiestappen:
(λx. f x x) y →β f y y plus 3 5 →δ 8
hoe moet je reduceren?
hoe vind je een normaalvorm (als die bestaat) ? hoe vind je een oneindige reductierij (als die bestaat) ? hoe vind je de kortste reductierij naar normaalvorm ? hoe voorkom je het kopi¨eren van redexen ?
schema
praktische zaken
opmerkingen vooraf
lambda termen
materiaal
materiaal
• dictaat hoofdstuk 1 • Haskell pagina
extra materiaal
• paper: Why functional programming matters
door John Hughes • paper: History of Lambda-calculus and Combinatory Logic
door Felice Cardone en J.Roger Hindley
