Intensional Semantics of System T of Gödel
Pierre Valarcher · Electronic Notes in Theoretical Computer Science · 2000
This paper is a contribution to the development of a theory of behaviour of programs. We study an intensional behaviour of system T of Gödel that is devoted to capturing not which function is computed but how it is computed. This intensional behaviour is captured by a denotational semantics in the domain of lazy natural numbers. It is shown that all sequential algorithms definable in system T are intensional behaviours. This leads us to obtain a general representation theorem asserting that we may compute every definable function of system T with the behaviour of a sequential algorithm using a higher-order term.