Lambda-Kalkül

Übersicht BlitzMax, BlitzMax NG Codearchiv & Module

Neue Antwort erstellen

Vertex

Betreff: Lambda-Kalkül

 BeitragSa, Nov 10, 2012 2:04
Antworten mit Zitat
Benutzer-Profile anzeigen
In der FH ist das Lambda-Kalkül gerade Thema. Um nicht die Übungsaufgaben per Hand auf Papier zu rechnen,
habe ich in BMax die Abstrakte-Syntax, die Relationen und einen Interpreter geschrieben. Das ganze ist inspiriert von http://www.youtube.com/watch?v=brmpy3TnYJk.

Funktionsumfang:
- Lambda-Terme können als abstrakte Syntax erstellt werden, z. B. Code: [AUSKLAPPEN]
\x -> xy
wird zu BlitzMax: [AUSKLAPPEN] 
Ab("x", App(Vr("x"), Vr("y")))

- Alpha-Äquivalenz BlitzMax: [AUSKLAPPEN] 
AlphaEq(t1, t2)
testest auf Gleichheit beider Terme t1, t2. Beispiel: Code: [AUSKLAPPEN]
\x.x =alpha \y.y
und in BMax:BlitzMax: [AUSKLAPPEN] 
Local t1 : Term = Ab("x", Vr("x"))
Local t2 : Term = Ab("y", Vr("y"))
AlphaEq(t1, t2) ' = True

- Beta-Relation: Testest auf Gleichheit beider Terme t1, t2, wobei t1 ein Redex ist und nach Auswerten Alpha-Äquivalent mit t2 sein muss. Vergleichbar mit Code: [AUSKLAPPEN]
(5 + 3) ->beta 8
Beispiel: Code: [AUSKLAPPEN]
(\x.x)y -> beta y
und in BMax: BlitzMax: [AUSKLAPPEN] 
Local t1 : Term = App(Ab("x", Vr("x")), Vr("y"))
Local t2 : Term = Vr("y")
Beta1(t1, t2) ' = True

- Auswertung des i-ten Redex: BlitzMax: [AUSKLAPPEN] 
Eval : Term(t : Term, i : Int)


Hier noch ein paar Hilfsfunktionen, um im Lambda-Kalkül auch zu Programmieren:
BlitzMax: [AUSKLAPPEN] 
' Selektiert die i-te Komponente in einem Paar: \t -> t(\d1\d2 -> di)
Function LambdaPairSelector : Term(i : Int)
	Return Ab("t", App(Vr("t"), Ab("d1", Ab("d2", Vr("d" + i)))))
End Function

' Konstruiert ein Paar: \s -> sD1D2
Function LambdaPair : Term(d1 : Term, d2 : Term)
	Return Ab("s", App(App(Vr("s"), d1), d2))
End Function

' \x\y -> x
Global LambdaTrue : Term = Ab("x", Ab("y", Vr("x")))
' \x\y -> y
Global LambdaFalse : Term = Ab("x", Ab("y", Vr("y")))

' Peano-Zahl 0: \x -> x
Local LambdaZero : Term = Ab("x", Vr("x"))

' Nachfolger-Zahl n -> n + 1
Function LambdaSucc : Term(n : Term)
	Return LambdaPair(LambdaFalse, n)
End Function

' Vorgänger-Zahl n -> n - 1
Function LambdaPred : Term(n : Term)
	Return App(LambdaPairSelector(2), n)
End Function

' n -> If n = 0 Then LambdaTrue Else LambdaFalse
Global LambdaIsZero : Term = LambdaPairSelector(1)

' If c Then t else e
Function LambdaIf : Term(c : Term, t : Term, e : Term)
	Return App(App(c, t), e)
End Function

' Let x = e1 In e2
Function LambdaLet : Term(x : String, e1 : Term, e2 : Term)
	Return App(Ab(x, e2), e1)
End Function

' Fixpunktoperator Theta f --beta--> f (Theta f)
Local LambdaThetaHalf : Term = Ab("x", Ab("y", App(Vr("y"), App(App(Vr("x"), Vr("x")), Vr("y")))))
Global LambdaTheta : Term = App(LambdaThetaHalf, LambdaThetaHalf)

' Rekursive Funktionsdefinition
Function LambdaRec : Term(f : String, b : Term)
	Return App(LambdaTheta, Ab("t", Subst(b, f, Vr("t"))))
End Function

' n -> Not n
Function LambdaNot : Term(n : Term)
	Return LambdaIf(n, LambdaFalse, LambdaTrue)
End Function

' (a,b) -> a And b
Function LambdaAnd : Term(a : Term, b : Term)
	Return LambdaIf(a, b, LambdaFalse)
End Function

' (a,b) -> a Or b
Function LambdaOr : Term(a : Term, b : Term)
	Return LambdaIf(a, LambdaTrue, b)
End Function

Rem
	\a\b -> a + b
	add a b = If b == 0 Then a Else add a ((b - 1) + 1)
End Rem
Global LambdaAdd : Term = LambdaRec("add",..
  Ab("a", Ab("b", LambdaIf(App(LambdaIsZero, Vr("b")), ..
                           Vr("a"), ..
                           LambdaSucc(App(App(Vr("add"), Vr("a")), LambdaPred(Vr("b"))))))))

Rem
	\a\b -> a * b
	mult a b = If b == 0 Then 0 Else add a (mult a (b - 1))
End Rem
Global LambdaMult : Term = LambdaRec("mult",..
  Ab("a", Ab("b", LambdaIf(App(LambdaIsZero, Vr("b")), ..
                           LambdaZero, ..
                           App(App(LambdaAdd, Vr("a")), App(App(Vr("mult"), Vr("a")), LambdaPred(Vr("b"))))       ))))

Rem
	Auswertung von t, bis kein Redex mehr ausgewertet werden kann.
	Auswertungsstrategie: Left-Outermost (sollte immer terminieren)
End Rem
Function EvalLeftOutermost : Term (t : Term)
	Print t.toString()
	Local t2 : Term
	Repeat
		t2 = t
		t = Eval(t2, 0)
		Print t.toString()
	Until AlphaEq(t, t2)

	Return t2
End Function


Folgendes Programm sei im Lambda-Kalkül umzusetzen:
Code: [AUSKLAPPEN]
t = (if true then 0 else 0 + 1)


In BMax ist das:
BlitzMax: [AUSKLAPPEN] 
Local t : Term = LambdaIf(LambdaTrue, LambdaZero, LambdaSucc(LambdaZero))
Print "t: " + t.toString()

' Ersten Redex auswerten
Local t2 : Term = Eval(t, 0)
Print "t2: " + t2.toString()

' Zweiten Redex auswerten
Local t3 : Term = Eval(t2, 0)
Print "t3: " + t3.toString()


Herauskommt "(\#1.#1)", was Alpha-Äquivalent zu "\x.x" ist, also LambdaZero. Wenn man statt LambdaTrue LambdaFalse in die Condition einsetzt, kommt auch LambdaSucc(LambdaZero) heraus.

Hier die Bibliothek:
BlitzMax: [AUSKLAPPEN] 
SuperStrict

Framework BRL.Blitz
Import BRL.StandardIO
Import BRL.LinkedList

' Counter für FreshName
Global counter : Int = 0

' Lambda-Term
Type Term Abstract
	Method toString : String() Abstract
End Type

' Referenz auf Variable name
Type Variable Extends Term
	Field name : String
	
	Method toString : String()
		Return name
	End Method
End Type

' Applikation von operator auf operand
Type Application Extends Term
	Field operator : Term
	Field operand : Term
	
	Method toString : String()
		Return "(" + operator.toString() + operand.toString() + ")"
	End Method
End Type

' Abstraktion \parameter -> body
Type Abstraction Extends Term
	Field parameter : String
	Field body : Term
	
	Method toString : String()
		Return "(\" + parameter + "." + body.toString() + ")"
	End Method
End Type

' "Konstruktor" für Variable
Function Vr : Variable(name : String)
	Local v : Variable = New Variable
	v.name = name
	Return v
End Function

' "Konstruktor" für Application
Function App : Application(operator : Term, operand : Term)
	Local app : Application = New Application
	app.operator = operator
	app.operand = operand
	Return app
End Function

' "Konstruktor" für Abstraction
Function Ab : Abstraction(parameter : String, body : Term)
	Local abst : Abstraction = New Abstraction
	abst.parameter = parameter
	abst.body = body
	Return abst
End Function

' Fügt element zur Menge set hinzu, falls es nicht bereits zur Menge gehört
Function AddSingleton(element : Object, set : TList)
	Local exist : Int = False
	For Local e : Object = EachIn set
		If e = element Then
			exist = True
			Exit
		EndIf
	Next
	
	If Not exist Then set.addLast(element)
End Function

' s2' = Vereinigungsmenge von s1 und s2
Function Union(s1 : TList, s2 : TList)
	For Local e : Object = EachIn s1
		AddSingleton(e, s2)
	Next
End Function

' "{x, y, z}"
Function SetToString : String(s : TList)
	Local str : String = "{"
	For Local e : String = EachIn s
		str = str + (e + ", ")
	Next
	If s.count() > 0 Then str = str[..(str.length - ", ".length)]
	str :+ "}"
	Return str
End Function

' Free Variables
Function FV : TList (t : Term)
	If Variable(t) Then
		Local v : Variable = Variable(t)
		Local s : TList = New TList
		AddSingleton(v.name, s)
		Return s
	ElseIf Application(t) Then
		Local app : Application = Application(t)
		Local s1 : TList = FV(app.operator)
		Local s2 : TList = FV(app.operand)
		Union(s2, s1)
		Return s1
	ElseIf Abstraction(t) Then
		Local abst : Abstraction = Abstraction(t)
		Local s : TList = FV(abst.body)
		s.remove(abst.parameter)
		Return s
	EndIf
End Function

' Bounded Variables
Function BV : TList (t : Term)
	If Variable(t) Then
		Local s : TList = New TList
		Return s
	ElseIf Application(t) Then
		Local app : Application = Application(t)
		Local s1 : TList = BV(app.operator)
		Local s2 : TList = BV(app.operand)
		Union(s2, s1)
		Return s1
	ElseIf Abstraction(t) Then
		Local abst : Abstraction = Abstraction(t)
		Local s : TList = BV(abst.body)
		AddSingleton(abst.parameter, s)
		Return s
	EndIf
End Function

Function SwapString : String(x : String, y : String, v : String)
	If v = x Then
		Return y
	ElseIf v = y Then
		Return x
	Else
		Return v
	EndIf
End Function

' Vertauscht Variablenname x mit y in t
Function Swap : Term(x : String, y : String, t : Term)
	If Variable(t) Then
		Local v : Variable = Variable(t)
		Return Vr(SwapString(x, y, v.name))
	ElseIf Application(t) Then
		Local a : Application = Application(t)
		Return App(Swap(x, y, a.operator), Swap(x, y, a.operand))
	ElseIf Abstraction(t) Then
		Local a : Abstraction = Abstraction(t)
		Return Ab(SwapString(x, y, a.parameter), Swap(x, y, a.body))
	EndIf
End Function

' Alpha-Äquivalenz
Function AlphaEq : Int (t1 : Term, t2 : Term)
	If Variable(t1) And Variable(t2) Then
		Local var1 : Variable = Variable(t1)
		Local var2 : Variable = Variable(t2)
		Return var1.name = var2.name
	ElseIf Application(t1) And Application(t2) Then
		Local app1 : Application = Application(t1)
		Local app2 : Application = Application(t2)
		Return AlphaEq(app1.operator, app2.operator) And AlphaEq(app1.operand, app2.operand)
	ElseIf Abstraction(t1) And Abstraction(t2) Then
		Local abs1 : Abstraction = Abstraction(t1)
		Local abs2 : Abstraction = Abstraction(t2)
		If abs1.parameter = abs2.parameter Then
			Return AlphaEq(abs1.body, abs2.body)
		ElseIf Not FV(abs1.body).contains(abs2.parameter) Then
			Return AlphaEq(Swap(abs1.parameter, abs2.parameter, abs1.body), abs2.body)
		Else
			Return False
		EndIf
	Else
		Return False
	EndIf
End Function

' Generiert neuen Variablennamen
Function FreshName : String()
	counter :+ 1
	Return "#" + counter
End Function

' Substituion A[x := N]
Function Subst : Term (a : Term, x : String, n : Term)
	If Variable(a) Then
		Local vr : Variable = Variable(a)
		If vr.name = x Then
			Return n
		Else
			Return vr
		EndIf
	ElseIf Application(a) Then
		Local ap : Application = Application(a)
		Return App(Subst(ap.operator, x, n), Subst(ap.operand, x, n))
	ElseIf Abstraction(a)
		Local abst : Abstraction = Abstraction(a)
		If abst.parameter = x Then
			Return abst
		Else
			If FV(n).contains(abst.parameter) Then
				Local z : String = FreshName()
				Return Ab(z, Subst(Swap(abst.parameter, z, abst.body), x, n))
			Else
				Return Ab(abst.parameter, Subst(abst.body, x, n))
			EndIf
		EndIf
	EndIf
End Function

' Beta-Relation
Function Beta1 : Int (t1 : Term, t2 : Term)
	If Application(t1) Then
		Local ap : Application = Application(t1)
		If Abstraction(ap.operator) Then
			Local ab : Abstraction = Abstraction(ap.operator)
			Return AlphaEq(Subst(ab.body, ab.parameter, ap.operand), t2)
		Else
			Return False
		EndIf
	Else
		Return False
	EndIf
End Function

' Ist der Term ein Reduceable Expression der Form (\x -> B)A?
Function IsRedex : Int (t : Term)
	If Application(t) Then
		Local ap : Application = Application(t)
		If Abstraction(ap.operator) Then
			Return True
		Else
			Return False
		EndIf
	Else
		Return False
	EndIf
End Function

' Für t = (\x -> B)A wird B[x := A] zurückgegeben
Function Eval1 : Term (t : Term)
	If Application(t) Then
		Local ap : Application = Application(t)
		If Abstraction(ap.operator) Then
			Local ab : Abstraction = Abstraction(ap.operator)
			Return Subst(ab.body, ab.parameter, ap.operand)
		Else
			Throw "in t = FA is F not an abstraction"
		EndIf
	Else
		Throw "t is not an application"
	EndIf
End Function

' Werte den pos-ten Redex aus
Function Eval : Term (t : Term, pos : Int = 0)
	If pos = 0 And IsRedex(t) Then
		Return Eval1(t)
	Else
		Local t2 : Term = CopyTerm(t)
		InnerEval(t2, 0, pos)
		Return t2
	EndIf
End Function

' Kopiert Rekursiv den Term t
Function CopyTerm : Term (t : Term)
	If Variable(t) Then
		Local v : Variable = Variable(t)
		Return Vr(v.name)
	ElseIf Application(t) Then
		Local a : Application = Application (t)
		Return App(CopyTerm(a.operator), CopyTerm(a.operand))
	ElseIf Abstraction(t) Then
		Local a : Abstraction = Abstraction(t)
		Return Ab(a.parameter, CopyTerm(a.body))
	EndIf
End Function

' Teil von Eval
Function InnerEval : Int (t : Term, accu : Int, pos : Int)
	If Variable(t) Then
		Return accu
	ElseIf Application(t) Then
		Local ap : Application = Application(t)
		Local f : Term = ap.operator
		If IsRedex(f) Then
			If accu = pos Then
				ap.operator = Eval1(f)
				accu :+ 1
			Else
				accu = InnerEval(f, accu + 1, pos)
			EndIf
		Else
			accu = InnerEval(f, accu, pos)
		EndIf
		Local a : Term = ap.operand
		If IsRedex(a) Then
			If accu = pos Then
				ap.operand = Eval1(a)
				accu :+ 1
			Else
				accu = InnerEval(a, accu + 1, pos)
			EndIf
		Else
			accu = InnerEval(a, accu, pos)
		EndIf
		Return accu
	ElseIf Abstraction(t) Then
		Local abst : Abstraction = Abstraction(t)
		Local x : String = abst.parameter
		Local b : Term = abst.body
		If IsRedex(b) Then
			If accu = pos Then
				abst.body = Eval1(b)
				accu :+ 1
			Else
				accu = InnerEval(b, accu + 1, pos)
			EndIf
		Else
			accu = InnerEval(b, accu, pos)
		EndIf
		Return accu
	EndIf
End Function

' Ausgabe des Syntaxbaums
Function PrintTree(t : Term, d : String = "")
	If Variable(t) Then
		Print d + "Var " + t.toString() + " | 0"
	ElseIf Application(t) Then
		Local ap : Application = Application(t)
		Print d + "App " + ap.toString() + " | " + IsRedex(t)
		PrintTree(ap.operator, d + " ")
		PrintTree(ap.operand, d + " ")
	ElseIf Abstraction(t) Then
		Local abstr : Abstraction = Abstraction(t)
		Print d + "Abs " +  t.toString()  + " | 0"
		PrintTree(abstr.body, d + " ")
	EndIf
End Function


Ciao Olli
  • Zuletzt bearbeitet von Vertex am Mo, Nov 26, 2012 1:14, insgesamt einmal bearbeitet

Vertex

 BeitragMo, Nov 26, 2012 0:06
Antworten mit Zitat
Benutzer-Profile anzeigen
Habe noch die Funktionen LambdaLet, LambdaRec, LambdaNot, LambdaAnd, LambdaOr und EvalLeftOutermost hinzugenommen.

Edit: Noch LambdaAdd, LambdaMult hinzugefügt, um mit den Peano-Zahlen zu rechnen.

Hier noch ein paar weitere Beispiele:
1) Let
Code: [AUSKLAPPEN]
Let x = True In Not x
wird zu:
BlitzMax: [AUSKLAPPEN] 
Local t : Term = LambdaLet("x", LambdaTrue, LambdaNot(Vr("x")))
EvalLeftOutermost(t)

das gibt folgendes aus:
Code: [AUSKLAPPEN]
((\x.((x(\x.(\y.y)))(\x.(\y.x))))(\x.(\y.x)))
(((\x.(\y.x))(\x.(\y.y)))(\x.(\y.x)))
((\y.(\x.(\y.y)))(\x.(\y.x)))
(\x.(\y.y))
(\x.(\y.y))

Was alpha-äquivalent zu LambdaFalse = \x\y.y ist.

2) einfache Rekursion
Code: [AUSKLAPPEN]
Let even n = If n == 0 Then True
             Else Not even(n - 1) In
    even 3
wird zu:

BlitzMax: [AUSKLAPPEN] 
Local even : Term = Ab("n", LambdaIf(App(LambdaIsZero, Vr("n")), .. ' n == 0
                              LambdaTrue, .. ' True
                              LambdaNot(App(Vr("even"), LambdaPred(Vr("n")))))) ' Not even(n - 1)

Local three : Term = LambdaSucc(LambdaSucc(LambdaSucc(LambdaZero)))

Local four : Term = LambdaSucc(three)

Local t : Term = App(LambdaRec("even", even), three)
EvalLeftOutermost(t)


Wird zu folgendem ausgewertet:
Code: [AUSKLAPPEN]
...
((((\y.y)(\x.(\y.x)))(\x.(\y.y)))(\x.(\y.x)))
(((\x.(\y.x))(\x.(\y.y)))(\x.(\y.x)))
((\y.(\x.(\y.y)))(\x.(\y.x)))
(\x.(\y.y))

Was alpha-äquivalent zu LambdaFalse = \x\y.y ist.

3) Wechselseitige Rekursion
Code: [AUSKLAPPEN]
Let
    even = If n == 0 Then True Else odd(n - 1)
  And
    odd = If n == 0 Then False Else even(n - 1)
  In even 3


In BMax würde man schreiben:
BlitzMax: [AUSKLAPPEN] 
Function even : Int (n : Int)
	If n = 0 Then
		Return True
	Else
		Return odd(n - 1)
	EndIf
End Function

Function odd : Int (n : Int)
	If n = 0 Then
		Return False
	Else
		Return even(n - 1)
	EndIf
End Function

Print even(3)


Und mit dem Lambda-Kalkül:
BlitzMax: [AUSKLAPPEN] 
' n -> If ISZERO(n) Then LambdaTrue Else odd(n - 1)
Local even : Term = Ab("n", LambdaIf(App(LambdaIsZero, Vr("n")), ..
                              LambdaTrue, ..
                              App(Vr("odd"), LambdaPred(Vr("n")))))
' n -> If ISZERO(n) Then LambdaFalse Else even(n - 1)
Local odd : Term = Ab("n", LambdaIf(App(LambdaIsZero, Vr("n")), ..
                              LambdaFalse, ..
                              App(Vr("even"), LambdaPred(Vr("n")))))

Local rec : Term = LambdaRec("t", ..
                     LambdaLet("even", App(LambdaPairSelector(1), Vr("t")), ..
                     LambdaLet("odd", App(LambdaPairSelector(2), Vr("t")), ..
                       LambdaPair(even, odd))))

Local three : Term = LambdaSucc(LambdaSucc(LambdaSucc(LambdaZero)))

Local four : Term = LambdaSucc(three)

Local t : Term = App(rec, Ab("even", Ab("odd", App(Vr("even"), three))))

EvalLeftOutermost(t)


Und gibt folgendes aus:
Code: [AUSKLAPPEN]
...
(\x.(\y.y))

Also LambdaFalse

Hingegen wird
BlitzMax: [AUSKLAPPEN] 
Local t : Term = App(rec, Ab("even", Ab("odd", App(Vr("odd"), three))))

zu LambdaTrue ausgewertet.

Für wechselseitige Rekursion mit mehr als 2 Funktionen müssten dann LambdaPair zu LambdaTuple bzw. LambdaPairSelector zu LambdaTupleSelector umgebaut werden.

4) Addition
Code: [AUSKLAPPEN]
2 + 3
wird zu:
BlitzMax: [AUSKLAPPEN] 
Local one : Term = LambdaSucc(LambdaZero)
Local two : Term = LambdaSucc(one)
Local three : Term = LambdaSucc(two)
Local four : Term = LambdaSucc(three)
Local five : Term = LambdaSucc(four)
Local six : Term = LambdaSucc(five)

Local t : Term = App(App(LambdaAdd, two), three)
Local res : Term = EvalLeftOutermost(t)
Print AlphaEq(five, res)

Und das letzte Print bestätigt, dass res alpha-äquivalent zu five ist.

4) Multiplikation
Code: [AUSKLAPPEN]
2 * 3
wird zu:
BlitzMax: [AUSKLAPPEN] 
Local t : Term = App(App(LambdaMult, two), three)
Local res : Term = EvalLeftOutermost(t)
Print AlphaEq(six, res)

Auch hier bestätigt das letzte Print, dass res alpha-äquivalent zu six ist.

5) Fakultät
Code: [AUSKLAPPEN]
Let fact n = If n == 0 Then 1
             Else n * fact(n - 1)
  In fact 3
Wird zu:

BlitzMax: [AUSKLAPPEN] 
Local fact : Term = LambdaRec("fact", ..
                    Ab("n", LambdaIf(App(LambdaIsZero, Vr("n")), ..
                              LambdaSucc(LambdaZero), ..
                              App(App(LambdaMult, Vr("n")) , App(Vr("fact"), LambdaPred(Vr("n")))))))

Local t : Term = App(fact, three)
Local res : Term = EvalLeftOutermost(t)
Print AlphaEq(six, res)


Achtung: Ich würde das Print in EvalLeftOutermost auskommentieren, sonst brauch er Ewigkeiten zum Auswerten.

Auch hier zeigt sich, dass res alpha-äquivalent zu six ist.

Ciao Olli

Neue Antwort erstellen


Übersicht BlitzMax, BlitzMax NG Codearchiv & Module

Nach Oben

Gehe zu:

Powered by phpBB © 2001 - 2006, phpBB Group