An example of a non adequate numeral system

Abstract

A numeral system is defined by three closed $\lambda$-terms : a normal $\lambda$-term $d_0$ for Zero, a $\lambda$-term $S_d$ for Successor, and a $\lambda$-term for Zero Test, such that the $\lambda$-terms $({S_d}^i{d}_0)$ are normalizable and have different normal forms. A numeral system is said adequate iff it has a closed $\lambda$-term for Predecessor. This Note gives a simple example of a non adequate numeral system.

Cited by in corpus (1)

• Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés