Answering a question by Honsell and Plotkin, we show that there are two equations between λ-terms, the so-called subtractive equations, consistent with λ-calculus but not satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of λ-calculus. © Alberto Carraro and Antonino Salibra.
On the equational consistency of order-theoretic models of the lambda-calculus
CARRARO, ALBERTO;SALIBRA, Antonino
2012-01-01
Abstract
Answering a question by Honsell and Plotkin, we show that there are two equations between λ-terms, the so-called subtractive equations, consistent with λ-calculus but not satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of λ-calculus. © Alberto Carraro and Antonino Salibra.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2012-carraro-salibra.CSL2012.pdf
accesso aperto
Tipologia:
Documento in Pre-print
Licenza:
Accesso gratuito (solo visione)
Dimensione
5.01 MB
Formato
Adobe PDF
|
5.01 MB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
