Numeri della Chiesa: come codificare zero nel lambda calcolo?

Question

Sto imparando lambda calcolo, ma non posso sembra di capire la codifica per il numero 0.

come è " funzione che prende in una funzione ed un secondo valore e applica la funzione zero volte sull'argomento " uno zero? C'è un altro modo per codificare a zero? qualcuno qui mi può aiutare codificare 0?

Answer 1

"Funzione che prende in una funzione ed un secondo valore e si applica la funzione zero volte sull'argomento"

A è, naturalmente, non è zero. Si tratta di un encoding di zero. Quando avete a che fare con la pianura lambda calcolo, è necessario codificare i numeri (così come altri tipi primitivi) in qualche modo, e ci sono alcuni requisiti dettati per ciascuno di questi tipi. Per esempio, un requisito per i numeri naturali, è quello di essere in grado di aggiungere 1 a un dato numero, e un altro è quello di essere in grado di distinguere lo zero dai numeri più grandi (se volete saperne di più, cercare "Peano Arithmetic"). La codifica popolare che Dario ha citato ti dà queste due cose, ed è anche che rappresenta un intero N da una funzione che fa qualcosa (codificato come argomento f) N volte -. Che è una sorta di un modo naturale per usare naturali

Ci sono altre codifiche che sono possibili - per esempio, una volta che si possono rappresentare le liste, è possibile rappresentare N come un elenco di N elementi. Queste codifiche hanno i loro pro e contro, ma quello di cui sopra è di gran lunga il più popolare.

Answer 2

wikipedia :

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

Se si impara lambda calcolo, probabilmente già sanno che λxy.y arg1 * * arg2 si ridurrà a arg2 , dal momento che la x è sostituito dal nulla, e la resto (λy.y) è la funzione identità.

Si potrebbe scrivere a zero in molti altri modi (cioè venire con una convenzione diversa), ma ci sono buone ragioni per usare λxy.y. Ad esempio, si desidera zero tramite il primo numero naturale, in modo che se si applica la funzione successore ad esso, si ottiene 1, 2, 3 ecc Con la funzione λabc.b (abc), si ottiene λxy.x (y ), λxy.x (x (y)), λxy.x (x (x (y))), ecc, in altre parole, si ottiene un intero sistema di numerazione.

Inoltre, si vuole a zero per essere l'elemento neutro rispetto alla somma. Con la nostra funzione successore S: = λabc.b (abc), possiamo definire n + * m * come n S m , vale a dire, n volte l'applicazione della funzione successore di m . I nostri soddisfa a zero λxy.y questo, entrambi 0 S m e m S 0 riducono a m .