Funktionale Programmierung: λ-Kalkül und kombinatorische Logik

λ	Die Assembler-Sprache der funktionalen Programmierung
	Das mathematische Fundament der funktionalen Programmierung

Geschichte
19[12][0-9]	Moses Schönfinkel, Haskell Curry Kombinatorische Logik
193[0-9]	Alonzo Church, Stephen Kleene λ-Kalkül

Sprachelemente	Expr ::= a -- Variablen \| (Expr Expr) -- Applikation \| λ a . Expr -- Funktion
	Dieses ist das minimale, uninterpretierte λ-Kalkül Es gibt nur Variablen, einstellige anonyme Funktionen und Funktionsanwendungen

Häufige Erweiterung	\| Literal -- false,true,1,2,3,... \| (Expr Op Expr) -- 2-stellige Operationen \| if Expr then Expr else Expr -- Verzweigungen \| let a = Expr in Expr -- lokale Variable \| fix Expr -- Fixpunkt-Kombinator

Beispiel	λ x . x + y -- ein Ausdruck e

	x ist eine gebundene Variablen in e
	y ist eine freie Variablen in e

Definitionen
offener Term open term	ein Ausdruck mit freien Variablen
abgeschlossener Term closed term	ein Ausdruck ohne freie Variablen
Kombinator	ein abgeschlossener Term

Beispiele	λx.x -- abgeschlossen (λx.(x ((λy.y a) x))) y -- offen
	Gebundene Variablen können umbenannt werden, ohne die Bedeutung eines Ausdrucks zu ändern
	Dieses gilt nicht für jede mögliche Umbenennung!
?	Beispiel?
	λx.x y → λy.y y -- [x/y]
in Haskell	data Expr = Var Ident \| App Expr Expr \| Lambda Ident Expr \| ... type Ident = String

?	Berechnung aller freien Variablen?
	fv :: Expr -> Set Ident fv (Var i) = {i} fv (App e1 e2) = fv e1 ∪ fv e2 fv (Lambda i e) = fv e \\ {i}
?	Berechnung aller gebundenen Variablen?
	bv :: Expr -> Set Ident bv (Var i) = {} bv (App e1 e2) = bv e1 ∪ bv e2 bv (Lambda i e) = bv e ∪ {i}
?	Wo kommen in der Mathematik noch gebundene Variablen vor?
	Quantoren, Summe, Produkt, Integral, ...

Unbehagen

Im λ-Kalkül durch gebundene Variablen viele unterschiedliche
Ausdrücke mit gleicher Bedeutung

Lösung

Elimination der gebundenen Variablen durch Transformation
in einige wenige Standard-Kombinatoren

SKI-Kombinatoren

S

S = λf.(λg.(λx.(f x)(g x)))

K

K = λx.λy.x

I

I = λx. x

in Haskell

s f g x = f x (g x)
 
k x y   = x
 
i x     = x

abkürzende Schreibweise

λx.(λy.e) = λx y.e

Satz
(Schönfinkel)

Alle abgeschlossenen λ-Ausdrücke (alle Kombinatoren) lassen sich
  durch Ausdrücke nur bestehend aus S und K formulieren

Beispiel

I = SKK

	SKK
=	{ Def. S und K }
	((λx y z.(x z) (y z)) (λx y.x)) (λx y.x)
=	{ 1. äußere Applikation }
	(λy z.((λx y.x) z) (y z)) (λx y.x)
=	{ 2. äußere Applikation }
	λz.((λx y.x) z) ((λx y.x) z)
=	{ 1. innere Applikation }
	λz.(λy.z) ((λx y.x) z)
=	{ 2. innere Applikation }
	λz.z
=	{ Def. I }
	I

Rechnen

im λ-Kalkül besteht aus der Auswertung von Funktions-Anwendungen

β-Reduktion

Eine Funktions-Anwendung auswerten heißt einen Reduktionsschritt ausführen
    
(die gebundene Variable einer Funktion erstzen durch den aktuellen Wert)

SKK = I: Guter Test für eine Implementierung

ω-Kombinator

ω = λx.x x

Selbstanwendung von x

?

Typ von x?

Ω-Kombinator

Ω = ω ω = (λx.x x)(λx.x x)

Reduktion von Ω

	Ω
=	{ Def. }
	(λx.x x)(λy.y y)
=	{ β-Reduktion }
	(λy.y y)(λy.y y)
=	{ β-Reduktion }
	(λy.y y)(λy.y y)
=	{ β-Reduktion }
	...

Die Berechnung divergiert!

DIE einfachste Endlosschleife im λ-Kalkül

Reduktion	eine Funktions-Anwendung auswerten
	Auswertung eines λ-Terms (λx.e) a
	Substitution aller freien Vorkommen der Variablen x in e durch das Argument a

Notation: Substitution	(λx.e)a → [x/a]e
Substitutions-Regeln	[x/a]x → a [x/a]y → y -- x ≠ y [x/a](e1 e2) → ([x/a]e1)([x/a]e2) [x/a]λx.e → λx.e [x/a]λy.e → λy.([x/a]e) -- x ≠ y und y ∉ fv(e)

?	Warum y ∉ fv(e)?
	[y/x](λx.x y) → λx.x x
Gebundene Umbenennung	Gebundene Variablen umbennen ohne die Bindungsrelation zu verändern

Regeln	zur Reduktion und Umformung
α-Äquivalenz	λx.e = λy.[x/y]e -- y ∉ fv(e)
	gebundene Umbenennung
Beispiele	λx y.x y = λa b.a b λx y.x y = λy x.y x
?	α-Äquivalenz in Haskell?
	alphaEq :: Expr -> Expr -> Bool alphaEq e1 e2 = eq [] e1 e2 && fv e1 == fv e2 where del x env = filter ((/= x) . fst) env add x y env = (x, y) : env eq env (Var x) (Var y) = (x, y) `elem` env -- bound variable \|\| x == y -- free variable eq env (Lambda x e1) (Lambda y e2) = eq (add x y $ del x env) e1 e2 eq env (App e11 e12) (App e21 e22) = eq env e11 e21 && eq env e12 e22 eq env e1 e2 = False

β-Reduktion	ein Substitutionsschritt
	(λx.e) a → [x/a]e

η-Reduktion	λx.(e x) → e -- für x ∉ fv(e)
	Extensionalitäts-Prinzip

η-Expansion	e → λx.(e x) -- für x ∉ fv(e)
	Umkehrung der η-Reduktion

Praxis	β-Reduktion (Ersetzen aller Vorkommen von x durch das Argument) und α-Äquivalenz (gebundene Umbenennung) mittels Formeltransformation aus Effizienzgründen unpraktikabel
Lösung	Indirektstufe einführen
	Variablenbindungen in einer Tabelle (Environment) speichern und beim Auswerten einer Variablen die Variable durch den assoziierten Wert ersetzen
Reduktions-Strategie	Welcher Reduktionsschritt wird als nächster gemacht?
	Verschiedene Strategien möglich
Beispiele	(λx.x + x)((λy.y * y) 2) => (λx.x + x)(2 * 2) => (λx.x + x) 4 => 4 + 4 => 8
	leftmost innermost
	(λx.x + x)((λy.y * y) 2) => ((λy.y * y) 2) + ((λy.y * y) 2) => (2 * 2) + ((λy.y * y) 2) => 4 + ((λy.y * y) 2) => 4 + (2 * 2) => 4 + 4 => 8
	leftmost outermost
	(λx.(λy.1) x) e => (λy.1) e => 1
	partial evaluation

let-Ausdrücke	Expr ::= ... \| let x = e1 in e2
Substitutions-Regeln	let x = e1 in e2 → (λx.e2)e1 → [x/e1]e2

Rekursion	zum Wiederholen von Berechnungen
Υ-Kombinator	entdeckt von Haskell Curry
	Y = λf.(λx.(f(x x))(λx.(f(x x))))
Gesetz	Υ f = f(Υ f) -- also Υ f = f(f(f(...)))

Υ	ersetzt durch S und K
	Υ = SSK(S(K(SS(S(SSK))))K)

Fixpunkt-Ausdrücke	Expr ::= ... \| ... \| fix e
Substitutions-Regel	fix f → f (fix f)

Beispiel	let fact = fix (λf.λn . if n == 0 then 1 else n * f(n - 1)) in fact 5

rekursive let-Ausdrücke	Expr ::= ... \| ... \| let rec x = e1 in e2
	in Haskell der Default
Substitutions-Regel	let rec x = e1 in e2 → let x = fix (λx.e1) in e2

Beispiel	let rec fact = λn . if n == 0 then 1 else n * fact(n - 1))

	Υ-Kombinator: Guter Test für eine Implementierung des λ-Kalküls

λ-Kalkül und kombinatorische Logik

λ-Kalkül

Kombinatoren

Reduktion und Substitution

Erweiterungen