zbMATH — the first resource for mathematics

Recursive definitions in type theory. (English) Zbl 0579.68019
Logics of programs, Proc. Conf., Brooklyn/N.Y. 1985, Lect. Notes Comput. Sci. 193, 61-78 (1985).
Summary: [For the entire collection see Zbl 0562.00009.]
We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor ($$\to)$$ to those with only positive occurrences of the defined typed. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott’s domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory.

MSC:
 68Q65 Abstract data types; algebraic specification 03B15 Higher-order logic; type theory (MSC2010) 03F65 Other constructive mathematics