Minimal forms inλ-cakulus computations
Corrado Böhm, Silvio Micali · Journal of Symbolic Logic · 1980
Abstract The notion of a minimal form is defined as an extension of the notion of a normal form inλ-β-calculus and its meaning is discussed in a computational environment. The features of the Knuth-Gross reduction strategy are used to prove that to possess a minimal form, for a generic term, is a semidecidable predicate.