Gödelisation in the lambda-Calculus (Extended Version)

Abstract

Gödelisation is a meta-linguistic encoding of terms in a language.
While it is impossible to define an operator in the lambda-calculus which
encodes all closed lambda-expressions, it is possible to construct restricted
versions of such an encoding operator modulo normalisation. In this
paper, we propose such an encoding operator for proper combinators.

Keywords: Programming Calculi; lambda-Calculus; G¨odelisation.