Warum sind Lambda-Abstraktionen die einzigen Begriffe, die Werte im untypisierten Lambda-Kalkül sind?

7

Ich bin verwirrt über die folgende Behauptung: "Die einzigen Werte im untypisierten Lambda-Kalkül sind Lambda-Abstraktionen".

Warum sind die anderen Begriffe keine Werte? Was bedeutet es für eine Lambda-Abstraktion, ein Wert zu sein? Das erste, was mir in den Sinn kam, war, dass vielleicht Lambda-Abstraktionen die einzig möglichen Normalformen sind, aber das trifft natürlich nicht zu, zB .(λx.x)y→y

Kann mich jemand aufklären?

logic lambda-calculus codd
quelle
Wo hast du das gesehen? Die Definition des Wertes kann variieren.
jmad
2
(λx.x) y ist keine Lambda-Abstraktion, es ist eine Anwendung, nämlich die Anwendung von (λx.x) zu y.
Dave Clarke
1
@ DaveClarke: Ich denke, Jeroen hat das gemeint ywar eine normale Form (um zu widerlegen, dass ein Wert eine Abstraktion ist) und nicht, dass eine Abstraktion war (um zu widerlegen, dass eine Abstraktion ein Wert ist). (λx.x)y
jmad
2
Variablen sind in jedem Kalkül immer Werte.
Fabio F.
2
@ DaveClarke: Ich habe gerade Pierces Buch überprüft. Die Verwirrung entstand, weil die operative Semantik des Lambda-Kalküls zuerst informell angesprochen wird. In einer Fußnote heißt es, dass die einzigen Werte des Kalküls Lambda-Abstraktionen sind. Später, wenn die Semantik formal definiert ist, wird klar, dass nur geschlossene Begriffe berücksichtigt werden.
Codd

Antworten:

10

Hier ist eine Reihe von Dingen im Gange:

  • Die Sprache, über die Sie sprechen, hat keine zusätzlichen Datentypen, da es sonst andere Arten von Werten geben würde.
  • Die Reduktionsstrategie der Sprache reduziert nicht die Lambda-Abstraktionen. Dies entspricht sowohl Call-by-Value als auch Call-by-Name. Andernfalls wäre nicht jede Lambda-Abstraktion normal.
  • Man betrachtet geschlossene Ausdrücke im Allgemeinen als Programme, daher gibt es keine freien Variablen, daher wird das von Ihnen präsentierte Beispiel nicht berücksichtigt.

Andere Begriffe sind keine Werte, da sie reduziert werden können oder in geschlossenen Programmen nicht vorkommen.

Dass eine Lambda-Abstraktion ein Wert ist, bedeutet, dass sie (abhängig von der Reduktionsstrategie) nicht weiter reduziert werden kann.

Bei offenen Begriffen sind Variablen auch Werte.

Dave Clarke
quelle
1
Das macht Sinn. Die Hauptsache, die ich daraus mache, ist, dass nur geschlossene Begriffe berücksichtigt werden sollten. Ich werde anhand der Originalquelle prüfen, ob dies Teil der formalen Definition der operativen Semantik ist.
Codd