Strictness analysis of the untyped \(\lambda\)-calculus (Q1114667)

The author defines ``strictness'' and ``eager evaluation'' over the untyped lambda-calculus as follows: \({\mathcal E}\) is a primitive recursive function that reduces a \(\lambda\)-term to its head normal form (h.n.f.) (if any). Given S a finite set of natural numbers, a closed term M is said to be S-strict if whenever \(k\geq \max (S)\) and terms \(N_ 1,...,N_ k\) are such that if \(i\in S\), \(N_ i\) has no h.n.f. then \(MN_ 1...N_ k\) has no h.n.f. If p is a natural number, a closed term M is p-eagerly evaluable if whenever given \(k>p\) and terms \(N_ 1,...,N_ k\) such that \(MN_ 1...N_ k\) has h.n.f. then \(N_ p\) also has h.n.f. and \({\mathcal E}[MN_ 1N_ 2...N_ k]\) reduces internally to \({\mathcal E}[MN_ 1N_ 2...{\mathcal E}[N_ p]...[N_ k]].\) The following results are proved: A term is \(\{\) \(k\}\)-strict iff it is k-eagerly evaluable. If M is a closed term and \(M=\lambda z_ 1...z_ p...z_ kQ_ 1Q_ 2...Q_ n\), then M is \(\{\) \(j\}\)-strict iff \(j=k\).