Sequenziamento o continuazione-passaggio in lambda-calcolo puro
Sto cercando di risolvere il seguente esercizio qui fornito .
Considera la seguente rappresentazione numerica. Come definire l'aggiunta?
|0| = λx.x
|1| = λx.λx.x
...
|n + 1| = λx.|n|
Gli operatori successori e predecessori sono facili da definire:
Succ n = λx.n
Pred n = n (λx.x)
Una soluzione "ovvia" per definire l'addizione è quella di utilizzare l'operazione successiva più il test per zero insieme al combinatore a punto fisso, qualcosa come (YF) per F indicato di seguito (l'operatore se e booleani sono definiti come al solito):
F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))
Ma definire Is0 non sembra banale. Il problema è che un numero | N | consuma N + 1 argomenti e N argomenti vengono semplicemente cancellati da esso. Quindi, se applico una tale funzione, sembra ragionevole interromperne l'applicazione quando diventa chiaro che il numero, ad esempio, non è un'identità. Immagino sia una sorta di continuazione, ma non riesco a immaginare come modellarlo nel puro lambda-calcolo. Forse qualcuno conosce qualche consiglio che potrebbe aiutare?
Un operatore di sequenziamento può anche aiutare a definire l'aggiunta. Se un'applicazione di un numero | m | è ritardato fino a quando un numero | n | viene applicato a tutti i suoi argomenti, il risultato sarà esattamente un numero | n + m | . Forse esiste una variante di un tale combinatore di sequenziamento nel lambda-calcolo puro?
La risposta fornita dall'autore dell'esercizio utilizza un'operazione non pura (ovvero IsProcedure che verifica se il suo argomento è una funzione).
UPD: Non è difficile eseguire un CPS in lambda-calcolo (i dettagli per CBV possono essere trovati qui ). Sembra che non sia sufficiente per risolvere il problema.
UPD : Se abbiamo una versione delle funzioni quote-eval per il puro lambda-calcolo, allora deve esserci una funzione$eq$, che riconosce se le espressioni lambda quotate sono sintatticamente uguali e possiamo costruire Is0 usando$eq$. Ma ne dubito$eq$è definibile. Il motivo è "lemma di genericità" (libro di Barendregt, lemma 14.3.24). Se fossimo in grado di testare l'uguaglianza sui termini lambda citati, allora ($eq$( Citazione $\Omega$) ( Citazione $\lambda x.x$)) ritornerebbe $False$e la genericità implica che ($eq$( Citazione $\lambda x.x$) ( Citazione $\lambda x.x$)) tornerebbe anche $False$. Ciò contraddice la possibilità di costruire Quote nel puro lambda-calcolo?
Risposte
Non credo che troverai quello che stai cercando nel puro lambda calcolo. La chiave è questa affermazione che hai fatto:
Un operatore di sequenziamento può anche aiutare a definire l'aggiunta. Se un'applicazione di un numero | m | è ritardato fino a quando un numero | n | si applica a tutti i suoi argomenti, ...
Bene, i modelli del lambda calcolo dovrebbero essere come:
$$U \cong U^U$$
E il punto di questo è che ogni valore semantico$u \in U$può essere applicato a qualcosa. Quindi non ha senso parlare di qualcosa che viene "applicato a tutti i suoi argomenti". Non esiste alcun valore che non possa essere applicato a più argomenti nel puro lambda calcolo.
Non conosco un modello / argomento che questa rappresentazione dei naturali renda impossibile da implementare IsZero, anche se a pensarci bene sembra improbabile. Tuttavia, se deve essere possibile nel puro lambda calcolo, dovrà avere senso semanticamente e non basarsi su nozioni che sono solo sintattiche.
Modifica: ecco uno schizzo di un argomento. Una definizione di$\mathsf{IsZero}$ alla fine deve ridursi come:
$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$
Il motivo è che l'applicazione a un certo numero di valori è l'unico meccanismo nel lambda calcolo per distinguere effettivamente tra i numeri. Deve essere il caso che:$$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ Tuttavia, per ogni $\overrightarrow v$ è il caso che: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (dove $|\overrightarrow v|$ è la lunghezza di $\overrightarrow v$). Ma solo$|1| = \mathsf{false}$(se questa è la convenzione scelta). In inglese, non esiste alcun limite al numero di termini richiesti per ottenere un booleano applicando un numero. Quindi non può esserci un file$\overrightarrow v$ che soddisfa le equazioni per tutti i numeri, e quindi $\mathsf{IsZero}$ non può essere definito.