Grundlagen der funktionsorientierten Programmierung mit SCHEME/Der Lambda-Kalkül

Wiki-Quelltext dieser Seite.

<language>SchemeJS</language>
== Einführung ==

[[Datei:Church.jpg|miniatur|Alonzo Church]]

Der &lambda;-Kalkül fasst berechenbare Funktionen zu einer abstrakten Klasse zusammen.<br /><br />

Er wurde um 1936 durch '''Alonzo Church''' (* 14. Juni 1903; † 11. August 1995; US-amerikanischer Mathematiker, Logiker und Philosoph; Mitbegründer der theoretischen Informatik) entwickelt und bildet die theoretische Grundlage funktionaler bzw. funktionsorientierter Programmiersprachen.<br />
'''Hinweis:'''<br />
Der &lambda;-Kalkül und die [http://de.wikipedia.org/wiki/Turingmaschine Turingmaschine] (theoretisches Fundament imperativer Programmiersprachen) beschreiben äquivalente Klassen berechenbarer Funktionen.
Damit sind funktionale bzw. funktionsorientierte Programmiersprachen (z.B. Haskell, Scheme, Logo) und imperative Programmiersprachen (z.B. Visual Basic, Delphi, C++) "gleich mächtig".<br /><br />

Die ''Grundidee'' des &lambda;-Kalküls besteht darin, die Klasse der ''&lambda;-Ausdrücke'' zu bilden,
* die aus gegebenen Grundbausteinen aufbaut werden und
* für die bestimmte Rechenregeln bestehen.<br /><br />

== Definition der &lambda;-Ausdrücke ==

<code id="4b65bb7a9fe6c" hidden>
(define pi (* 4 (atan 1)))

(define sqr
  (lambda (x)
    (* x x)))
</code>

<ol>
<li>
Der Vorrat an Grundbausteinen ist eine (abzählbar) unendliche Menge von Variablen
$\{x_1, x_2, x_3, ...\}$, die selbst &lambda;-Ausdrücke sind.<br />

'''Beispiele:'''

<table>
<tr>
<td><run id="4b656369f02d3">pi</run></td>
<td><run id="4b656369f125b">car</run></td>
</tr>
</table>
</li>
<li>
Durch Anwendung des &lambda;-Ausdrucks $M$ auf den &lambda;-Ausdruck $N$ entsteht wieder ein &lambda;-Ausdruck, geschrieben als $(M N)$.<br />

'''Beispiele:'''

<table>
<tr>
<td><run id="4b656369f21f9">(sqrt pi)</run></td>
<td><run id="4b656369f31a0">(car '(a b))</run></td>
</tr>
</table>
</li>
<li>
&lambda;-Ausdrücke können durch funktionale Abstraktion erzeugt werden:
Mit der Variablen $x$ und dem &lambda;-Ausdruck $M$ ist auch 
$(\lambda (x) M)$ ein &lambda;-Ausdruck.<br />

'''Beispiele:'''

<table>
<tr>
<td><run id="4b656369f4137">(lambda (x) (* 2 x))</run></td>
<td><run id="4b65649f54168">(lambda (ls) (car ls))</run></td>
</tr>
<tr>
<td><run id="4b65636a01e46">((lambda (x) (* 2 x)) 12)</run></td>
<td><run id="4b65649f550f3">((lambda (ls) (car ls)) '(a b))</run></td>
</tr>
</table>
</li>
</ol>

== Rechenregeln ==

<code id="4b70ad855c47f" hidden>
(define super-element?
  (lambda (el ls)
    (cond
      [(not (list? ls)) (if (eqv? el ls) #t #f)]
      [(null? ls) #f]
      [(list? (car ls)) (or (super-element? el (car ls)) (super-element? el (cdr ls)))]
      [(eqv? el (car ls)) #t]
      [else
       (super-element? el (cdr ls))])))

(define super-streichen
  (lambda (el ls)
    (cond
      [(not (list? ls)) ls]
      [(null? ls) ls]
      [(list? (car ls)) (cons (super-streichen el (car ls)) (super-streichen el (cdr ls)))]
      [(eqv? el (car ls)) (super-streichen el (cdr ls))]
      [else
       (cons (car ls) (super-streichen el (cdr ls)))])))

(define super-ersetzen
  (lambda (el1 ls el2)
     (cond
      [(not (list? ls)) ls]
      [(null? ls) ls]
      [(list? (car ls)) (cons (super-ersetzen el1 (car ls) el2) (super-ersetzen el1 (cdr ls) el2))]
      [(eqv? el1 (car ls)) (cons el2 (super-ersetzen el1 (cdr ls) el2))]
      [else
       (cons (car ls) (super-ersetzen el1 (cdr ls) el2))])))

(define operator-liste?
  (lambda (ausdr)
    (and (list?  ausdr) (not (null? ausdr)) (or (symbol? (car ausdr)) (procedure? (eval (car ausdr)))))))

(define lambda-term?
  (lambda (ausdr)
    (and (list? ausdr) (= (length ausdr) 3) 
         (eqv? (car ausdr) 'lambda)
         (list? (cadr ausdr)) (= (length (cadr ausdr)) 1) (symbol? (caadr ausdr))
         (or (symbol? (caddr ausdr)) (number? (caddr ausdr)) (operator-liste? (caddr ausdr))))))

(define lambda-anwendung?
  (lambda (ausdr)
    (and (list? ausdr) (= (length ausdr) 2)
         (lambda-term? (car ausdr)))))

(define lambda-ausdruck?
  (lambda (ausdr)
    (or (symbol? ausdr)
        (operator-liste? ausdr)
        (lambda-term? ausdr))))

(define beta-left
  (lambda (term)
    (let ([var (caadar term)] [ausdr1 (caddar term)] [ausdr2 (cadr term)])
      (super-ersetzen var ausdr1 ausdr2))))

;Beta-Reduktion
(define beta
  (lambda (term)
    (cond
      [(not (list? term)) term]
      [(null? term) term]
      [(lambda-anwendung? term) (beta (beta-left term))]
      [(list? (car term))
       (cons (beta (car term)) (beta (cdr term)))]
      [else
       (cons (car term) (beta (cdr term)))])))

(define alphabet '(a b c d e f g h i j k l m n o p q r s t u v w x y z))

(define suche-var
  (lambda (var term ausdr alphabet)
    (cond
      [(and (not (super-element? var term)) (not (super-element? var ausdr))) var]
      [(null? alphabet) var]
      [else
       (suche-var (car alphabet) term ausdr (cdr alphabet))])))

(define alpha-test
  (lambda (term ausdr)
    (cond
      [(not (list? term)) term]
      [(null? term) term]
      [(lambda-term? term)
       (let ([var (caadr term)] [neuterm (caddr term)])
         (cond
           [(super-element? var ausdr)
            (let ([neuvar (suche-var var term ausdr alphabet)])
              (super-ersetzen var term neuvar))]
           [(lambda-term? neuterm) (list 'lambda (list var) (alpha-test neuterm ausdr))]
           [else
            term]))]          
      [(list? (car term))
       (cons (alpha-test (car term) ausdr) (alpha-test (cdr term) ausdr))]
      [else
       (cons (car term) (alpha-test (cdr term) ausdr))])))

(define alpha-ersetzen
  (lambda (term alphabet)
    (cond
      [(not (lambda-term? term)) term]
      [(null? alphabet) term]
      [(eqv? (car alphabet) (caadr term)) (alpha-ersetzen term (cdr alphabet))]
      [(super-element? (car alphabet) (cddr term)) (alpha-ersetzen term (cdr alphabet))]
      [else
       (super-ersetzen (caadr term) term (car alphabet))]))) 

(define lambda-ersetzen 
  (lambda (term var)
    (if (lambda-term? term)
        (let ([geb-var (caadr term)] [op-term (caddr term)])
          (cond
            [(super-element? var op-term) term]
            [(lambda-term? op-term) (list 'lambda (list geb-var) (lambda-ersetzen op-term var))]
            [else
              (super-ersetzen geb-var term var)]))
        term)))

;Alpha-Konvention
(define alpha
  (lambda (term)
    (cond
      [(not (list? term)) term]
      [(null? term) term]
      [(lambda-anwendung? term)
       (let ([var (caadar term)] [lambda-term (car term)] [ausdr (cadr term)])
         (list (alpha-test lambda-term ausdr) ausdr))]
      [(list? (car term))
       (cons (alpha (car term)) (alpha (cdr term)))]
      [else
       (cons (car term) (alpha (cdr term)))])))

(define eta-einf
  (lambda (term)
    (if (lambda-term? term)
        (let ([var (caadr term)] [ausdr (eta-einf (caddr term))])
          (cond
            [(lambda-term? ausdr) 
             (eta-einf (list 'lambda (list var) ausdr))]
            [(lambda-anwendung? ausdr)
             (list (eta-einf (car ausdr)) (eta-einf (cadr ausdr)))]
            [(and (list? ausdr) (= (length ausdr) 2))
             (let ([ausdr-li (eta-einf (car ausdr))] [ausdr-re (eta-einf (cadr ausdr))])
               (if (eqv? var ausdr-re)
                   ausdr-li
                   (list ausdr-li ausdr-re)))]
            [else
             term]))
        term)))

(define eta-mehrf
  (lambda (term)
    (cond
      [(not (list? term)) term]
      [(null? term) term]
      [(lambda-term? term) (eta-einf term)]
      [(lambda-anwendung? term) (list (eta-mehrf (car term)) (eta-mehrf (cadr term)))]
      [(list? (car term))
       (cons (eta-mehrf (car term)) (eta-mehrf (cdr term)))]
      [else
       (cons (car term) (eta-mehrf (cdr term)))])))

;Eta-Umwandlung
(define eta
  (lambda (term)
    (let ([term-neu (eta-mehrf term)])
      (if (equal? term term-neu)
          term
          (eta term-neu)))))
</code>

=== &beta;-Reduktion ===

Sind $E$ und $M$ &lambda;-Ausdrücke, wobei $M$ in $E$ nicht gebunden vorkommen darf, und $x$ eine Variable, so beschreibt
<blockquote>$((\lambda (x) E) M)\stackrel{\beta}{\longrightarrow}E[M/x]$</blockquote>
<blockquote>(sprich: "$E$ mit $M$ für $x$")</blockquote>
das Ergebnis der Anwendung von $(\lambda (x) E)$ auf $M$.<br />
Dabei werden im Ausdruck $E$ alle Variablen $x$ durch den Ausdruck $M$ ersetzt.<br />

'''Beispiele:'''

<run id="4b65fa256c8fe">
(beta '((lambda (x) (* 2 x)) 12))
</run>

<run id="4b65fa256d89a">
(beta '((lambda (x) (+ (* x x) 2)) ((lambda (y) (- y 5)) 3)))
</run>

'''Beachte:'''<br />
Der &lambda;-Kalkül fordert eine sogenannte ''leftmost reduction'' bzw. ''normal order reduction'', d.h. der jeweils links stehende Ausdruck $(\lambda (x) E)$ wird zuerst reduziert.

=== &alpha;-Konvention ===

Wenn $x'$ in $E$ nicht frei vorkommt, gilt:
<blockquote>
$(\lambda (x) E)\stackrel{\alpha}{\longleftrightarrow}(\lambda (x') E[x'/x])$
</blockquote>
<blockquote> 
(sprich: "Ersetze alle $x$ in $(\lambda (x) E)$ durch $x'$")</blockquote>

'''Beispiele:'''

<run id="4b65e583945d7">
(alpha-ersetzen '(lambda (x) (* y x)) '(x y z))
</run>

<run id="4b845c1b206d8">
(alpha '(((lambda (op) (lambda (y) (op y))) y) w))
</run>

=== &eta;-Umwandlung ===

Vereinfachungsregel, mit:
<blockquote>$(\lambda (x) (E x))\stackrel{\eta}{\longrightarrow}E$</blockquote>

'''Beispiele:'''

<run id="4b65eafff086f">
(eta '(lambda (x) (sqrt x)))
</run>

<run id="4b65eafff17f8">
(eta '((lambda (x) (sqrt x)) ((lambda (y) (sin y)) 1)))
</run>

== Aufgaben ==

<code id="4b69ebeb48146" hidden>
(define listequal?
  (lambda (ls1 ls2)
    (cond
      [(and (null? ls1) (null? ls2)) #t]
      [(or (null? ls1) (null? ls2)) #f]
      [(and (list? (car ls1)) (list? (car ls1)))
         (and (listequal? (car ls1) (car ls2)) (listequal? (cdr ls1) (cdr ls2)))]
      [else 
       (and (equal? (car ls1) (car ls2)) (listequal? (cdr ls1) (cdr ls2)))])))
</code>

<ol>
<li>
Implementieren Sie die Prozedur <tt>super-ersetzen</tt>, die in einer verschachtelten Liste das Element 1 durch das Element 2 ersetzt.

<code id="4b69ebeb490d7">
(define super-ersetzen
  (lambda (el1 ls el2)
    ...))
</code>

<check>
(and (listequal? (super-ersetzen 'a '(a b a c a d) 'x) '(x b x c x d))
     (listequal? (super-ersetzen 'x '(lambda (x) (* 2 x)) 'z) '(lambda (z) (* 2 z))))
</check>

<run id="4b69f75ea6ea2">
(super-ersetzen 'x '(lambda (x) (+ (* 2 x) y)) 'z)
</run>
</li>
<li>
Schreiben Sie das Prädikat <tt>lambda-term?</tt>, das prüft, ob eine vorgegebene Liste ein &lambda;- Ausdruck der Form $(\lambda (x) E)$ ist.

<code id="4b69f75ea5f07">
(define lambda-term?
  (lambda (ausdr)
    ...))
</code>

<check>
(and (lambda-term? '(lambda (x) (* 2 x)))
     (lambda-term? '(lambda (z) (* (sin z) y)))
     (not (lambda-term? '(- x y z))))
</check>

<run id="4b69f75ea7e43">
(lambda-term? '(lambda (x) (+ (* 2 x) y)))
</run>
</li>
Implementieren Sie die nächste Aufgabe unter ''DrScheme''.
Denken Sie an die Definition geeigneter Hilfsprozeduren.
<li>
Schreiben Sie die Prozedur <tt>(lambda-ersetzen &lt;term&gt; &lt;var&gt;)</tt>, die in einem &lambda;-Term (vgl. Aufgabe 2) alle gebundenen Variablen durch die Variable <tt>var</tt> ersetzt. Natürlich darf <tt>var</tt> in diesem &lambda;-Term nicht frei vorkommen.<br />
Beachten Sie dabei, dass &lambda;-Terme selbst beliebige &lambda;-Terme enthalten können
(Repräsentation als verschachtelte Listen).
</li>
</ol>

== Zum Weiterarbeiten ==

=== Currying ===

Der &lambda;-Kalkül gestattet nur die Definition einstelliger Funktionen. In Scheme haben wir darüber hinaus nullstellige, mehrstellige und variabelstellige Prozeduren kennen gelernt.<br />
Um mehrstellige Prozeduren auf einstellige zurückzuführen, greifen wir die Idee der Prozeduren höherer Ordnung auf:

<code id="4b8ab8b74a977">
(define summe-curry
  (lambda (x)
    (lambda (y)
      (if (<= y 0)
        x
        ((summe-curry (+ x 1)) (- y 1))))))
</code>

<run id="4b8ab8b74b901">
((summe-curry 3) 5)
</run>

Diese Technik lässt sich auf beliebige n-stellige Prozeduren erweitern.
Sie bezeichnet man als ''Currying'' oder ''Curryfication'', benannt nach dem US-amerikanischen Logiker und Mathematiker '''Haskell Brooks Curry''' (* 12. September 1900; † 1. September  1982).

=== Y-combinator ===

Die Sonderform <tt>define</tt> ist im &lambda;-Kalkül ebenfalls nicht vorgesehen.
Zunächst scheint das kein Problem zu sein, da in Scheme unbenannte Prozeduren zur Anwendung kommen können. Doch wie lassen sich dann ''rekursive'' Prozeduren definieren?<br />
Wir benötigen dazu eine spezielle Funktion $Y$, die als "Rekursivmacher" fungiert.<br />
Von einer derartigen Funktion muss die sogenannte Fixpunkt-Eigenschaft erfüllt werden:

<blockquote>$(Y f) = (f (Y f))$</blockquote>

Ohne an dieser Stelle den Nachweis zu führen, erfüllt die Definition des ''Y-combinators'' diese Forderung:

<code id="4b8ad0a8e7a6f">
(define Y
  (lambda (f)
    ((lambda (x) (f (lambda (y) ((x x) y))))
     (lambda (x) (f (lambda (y) ((x x) y)))))))
</code>  

Wir nutzen zunächst die Kurzform <tt>Y</tt> zur rekursiven Definition der Fakultätsfunktion:

<run id="4b8bf8fcdcf23">
(Y
 (lambda (fak)
   (lambda (n)
     (if (= n 0)
         1
         (* n (fak (- n 1)))))))
</run>

Natürlich lässt sich diese Fakultätsfunktion auch anwenden. Wir berechnen z.B. $5!=120$:

<run id="4b8ad0a8e89f8">
((Y
  (lambda (fak)
    (lambda (n)
      (if (= n 0)
          1
          (* n (fak (- n 1))))))) 5)
</run>

Abschließend ersetzen wir <tt>Y</tt> durch den entsprechenden &lambda;-Ausdruck.
Nun benötigen wir für rekursive Definitionen tatsächlich kein <tt>define</tt>!

<run id="4b8ad0a8e9a16">
(((lambda (f)
    ((lambda (x) (f (lambda (y) ((x x) y))))
     (lambda (x) (f (lambda (y) ((x x) y))))))
  (lambda (fak)
    (lambda (n)
      (if (= n 0)
          1
          (* n (fak (- n 1))))))) 5)
</run>