Lambda-Kalkül: Erstellen Sie eine Funktion, die bei jeder Iteration mehr Argumente benötigt

Question

Ich versuche eine Funktion zu erstellen, die eine bestimmte Anzahl von Argumenten akzeptiert und immer den gleichen Wert zurückgibt.

Dies ist ein Teil einer Hausaufgabe. Es gibt einen Hinweis zur Verfügung gestellt ist:

Die "k-Wege-T" ist eine Funktion, die Argumente k und gibt immer T. A "0-Wege-T" nimmt nur T.

Wo k wird als Kirchenzahl angegeben und T ist der Lambda-Ausdruck für True (\ x. \ yx).

Die vollständige Aufgabe besteht darin, einen Lambda-Ausdruck bereitzustellen, der eine k-Wege-ODER-Funktion berechnet. Die Anzahl der 'booleschen' Argumente wird vor den 'booleschen' Argumenten angegeben. z:

((OR 3) F T F) 

Aber jetzt k Argumente und kehrt Ich versuche, das braucht immer T zu erstellen. Die k wird als erstes Argument zur Verfügung gestellt.

Also im Grunde möchte ich eine Funktion erstellen, die für jede Kirchenziffer 'Iteration' noch ein Argument hat.

Aber irgendwie bin ich völlig festgefahren.

Kann ich das nur mit einer Kirchenziffer machen? Oder brauche ich Rekursion (Y-Combinator)?

Allgemein: Gibt es gute Tools (z. B. zur Visualisierung), die die Erstellung von Lambda-Ausdrücken unterstützen?

Ich bin wirklich erstaunt über die Kraft des Lambda-Kalküls und ich möchte es wirklich lernen. Aber ich weiß nicht, wie ...

Vielen Dank im Voraus

Answer 1

Ich werde zeigen, wie die TRUE Funktion zu implementieren. Da k nicht festgelegt ist, benötigen Sie einen Festkomma-Kombinator (Y würde tun, aber es ist nicht der einzige Festkomma-Kombinator). Zuerst ein paar Worte über die Notation, die ich unten verwendet habe: iszero (nimmt eine Kirchennummer, prüft, ob es Church Zero ist und gibt einen Church boolean zurück), T (der Church-codierte wahre boolesche Wert), pred (die Vorgängerfunktion für Kirchenziffern) und Y (ein Festkomma-Kombinator).

let TRUE = Y (λr. λn. (iszero n) T (λx. (r (pred n)))) 

Beachten Sie, dass let ist nicht Teil der Lambda-Kalkül Syntax, es Metasyntax ist einen Namen einzuführen (für uns).

Dies funktioniert wie folgt: YArt wandelt das r Argument in „Selbst“ - wenn eine Funktion r nennt es nennt sich.Um dies zu veranschaulichen, werde ich das obige in rekursive Form umschreiben (Warnung: es ist nur für illustrative Zwecke, Lambda-Kalkül erlaubt dies nicht; da alle Funktionen anonym sind, können Sie sie nicht mit ihren Namen aufrufen - gibt es nur für diese keine Möglichkeit):

let TRUE = λn. (iszero n) T (λx. (TRUE (pred n))) 

ich den λr. Teil abgezogen habe und ersetzt r durch TRUE (auch hier bitte diese in Ihren Hausaufgaben nicht machen, es ist nicht gültig Lambda-Kalkül).

Und diese Definition ist leichter zu verstehen: wenn TRUE wie diese TRUE 0 genannt wird T nur zurückgibt, sonst ist es eine Funktion ein Argument gibt, die sich um eine Funktion von (n - 1) wickelt Argumente, im Wesentlichen eine Funktion der Repräsentation n Argumente.

Wie für Ihre Frage zu Tools: Eine Möglichkeit wäre, Scheme/Racket zu verwenden - es würde helfen, überprüfen Sie Ihre "Lambda-Kalkül-Code" läuft wie es sollte. Zum Beispiel, hier ist eine Implementierung von TRUE in Racket:

(define (Y f) 
    ((lambda (x) (x x)) 
    (lambda (x) (lambda (a) ((f (x x)) a))))) 

(define TRUE 
    (Y (lambda (r) 
     (lambda (n) 
     (if (zero? n) 
      #t 
      (lambda (x) (r (sub1 n)))))))) 

;; tests 
> (TRUE 0) 
#t 
> ((TRUE 1) #f) 
#t 
> (((TRUE 2) #f) #f) 
#t 
> ((((((TRUE 5) #f) #f) #f) #f) #f) 
#t 

Ich sollte hinzufügen, dass ich hier built-in verwendet booleans, ganzen Zahlen, wenn Ausdruck, sub1, zero? statt Church-codierten diejenigen. Sonst würde es dieses Beispiel viel größer (oder unvollständig) machen.