La codifica numerica della Chiesa dei numeri naturali è inutilmente complicata?

Question

Il libro Struttura e interpretazione dei programmi per computer che ho letto presenta i numeri della Chiesa definendo lo zero e una funzione di incremento

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

Mi è sembrato piuttosto complicato e mi ci è voluto molto tempo per capirlo e ricavarne uno (λf.λx. f x) e due (λf.λx. f (f x)).

Non sarebbe molto più semplice codificare i numeri in questo modo, con zero come lambda vuoto?

zero: λ
increment: λf. λ. f

Ora è banale derivarne uno (λ. λ) e due (λ. λ. λ) e così via.

Questo sembra un modo molto più immediatamente ovvio e intuitivo per rappresentare i numeri con lambda.C'è qualche problema con questo approccio e quindi una buona ragione per cui i numeri della Chiesa funzionano come funzionano?Questo approccio è già attestato?

Answer 1

La tua codifica (zero: λx.x, uno: λx.λx.x, due: λx.λx.λx.x, ecc.) rende facile definire l'incremento e il decremento, ma oltre a questo, diventa piuttosto complicato sviluppare combinatori per la tua codifica.Ad esempio, come definiresti isZero?

Un modo intuitivo di pensare alla codifica Church è che un n numerico è rappresentato dall'azione di iterare volte n.Ciò semplifica lo sviluppo di combinatori come plus utilizzando semplicemente l'iterazione codificata nel numero.Non c'è bisogno di combinatori fantasiosi per la ricorsione.

Nella codifica Church, ogni numero ha la stessa interfaccia: richiede due argomenti.Durante la codifica, ogni numero è definito dal numero di argomenti necessari, il che rende davvero difficile operare in modo uniforme.

Un altro modo per codificare i numeri sarebbe pensare ai numeri come n= 0 |S n, e usa una codifica vaniglia per le unioni.

Answer 2

The proposed syntax for numerals is not valid in lambda calculus, whereas Church numerals are indeed valid constructions in lambda calculus. So that's a possible reason why Church numerals are the way they are - the number encoding must adhere to the lambda calculus' definition in a way that also permits further operations also defined in lambda calculus (increment, for example) to operate over the encoded numbers.