Se si impara lambda calcolo, probabilmente già sapete che λxy.y arg1 * * arg2 ridurrà al arg2, dal momento che la x è sostituito dal nulla, e il resto (λy.y) è l'identità funzione.
È possibile scrivere zero in molti altri modi (ad esempio, creare una convenzione diversa), ma ci sono buoni motivi per utilizzare λxy.y. Ad esempio, vuoi che zero sia il primo numero naturale, in modo che se applichi la funzione successore ad esso, ottieni 1, 2, 3 ecc. Con la funzione λabc.b (abc), ottieni λxy.x (y), λxy.x (x (y)), λxy.x (x (x (y))) ecc., in altre parole, si ottiene un sistema di numeri interi.
Inoltre, si desidera che lo zero sia l'elemento neutro rispetto all'addizione. Con la nostra funzione successore S: = λabc.b (abc), possiamo definire n + * m * come n S m, cioè n volte l'applicazione della funzione successore m. Il nostro zero λxy.y soddisfa questo, sia 0 S m e m S 0 ridurre a m.
Questa è una domanda correlata che ho chiesto in gruppi di google: Dire che ho una funzione f. Come faccio a dimostrare che questo si traduce in un numero naturale 0? Quali altre funzioni ho bisogno per dedurre che la mia funzione f si comporta come uno 0? – unj2
Se si vuole provare che una funzione 'f' è zero sotto la solita codifica, è necessario mostrare che per tutti' g' (f g x) == x. Non hai bisogno di sapere niente al di là di questo. –