Ist die Kodierung natürlicher Zahlen durch die Kirche unnötig kompliziert?

Question

Das Buch Struktur und Interpretation von Computerprogrammen , das ich gelesen habe, enthält Kirchennummern, indem Null und eine Inkrementfunktion definiert werden

zero: λf. λx. x
increment: λf. λx. f ((n f) x)

Das schien mir ziemlich kompliziert zu sein und ich habe sehr lange gebraucht, um es herauszufinden und eins (λf.λx. f x) und zwei (λf.λx. f (f x)) abzuleiten.

Wäre es nicht viel einfacher, stattdessen Zahlen auf diese Weise zu codieren, wobei Null das leere Lambda ist?

zero: λ
increment: λf. λ. f

Jetzt ist es trivial, eins (λ. λ) und zwei (λ. λ. λ) usw. abzuleiten.

Dies scheint eine viel unmittelbarere und intuitivere Möglichkeit zu sein, Zahlen mit Lambdas darzustellen.Gibt es ein Problem mit diesem Ansatz und damit einen guten Grund, warum die Ziffern der Kirche so funktionieren, wie sie es tun?Ist dieser Ansatz bereits bestätigt?

Answer 1

Ihre Codierung (null: λx.x, eins: λx.λx.x, zwei: λx.λx.λx.x usw.) macht es einfach, Inkremente und Dekremente zu definieren, aber darüber hinaus wird es ziemlich schwierig, Kombinatoren für Ihre Codierung zu entwickeln.Wie würden Sie beispielsweise isZero definieren?

Eine intuitive Möglichkeit, über die Kodierung der Kirche nachzudenken, besteht darin, dass ein generischer Codacetagcode durch die Aktion des Iterierens von n-Zeiten dargestellt wird.Dies macht es einfach, Kombinatoren wie n zu entwickeln, indem nur die in der Zahl codierte Iteration verwendet wird.Keine Notwendigkeit für ausgefallene Kombinatoren für die Rekursion.

In der Church-Codierung hat jede Nummer dieselbe Schnittstelle: Sie benötigt zwei Argumente.Während Ihrer Codierung wird jede Zahl durch die Anzahl der Argumente definiert, die erforderlich sind, was es wirklich schwierig macht, einheitlich zu arbeiten.

Eine andere Möglichkeit, Zahlen zu codieren, besteht darin, sich Zahlen als n= 0 | vorzustellenS n und verwenden Sie eine Vanille-Codierung für Gewerkschaften.

Answer 2

Die vorgeschlagene Syntax für Ziffern ist in der Lambda-Rechnung nicht gültig, wohingegen Kirchenzahlen in der Tat gültige Konstruktionen in der Lambda-Rechnung sind.Das ist also ein möglicher Grund, warum Kirchennummern so sind, wie sie sind - die Zahlenkodierung muss dem Lambda-Kalkül entsprechen ' Definition auf eine Weise, die es auch ermöglicht, dass weitere Operationen, die auch im Lambda-Kalkül (z. B. Inkrement) definiert sind, über die codierten Zahlen ausgeführt werden.