| Abc-Active Terms in Transfinite Lambda Calculus (1996) | |||||||||||||
Abstract | |||||||||||||
| . This document contains proofs of some claims made in our paper "Meaningless terms in rewriting" [KvOdV96]. It depends on a knowledge of that paper. Theorem 1. In transfinite lambda calculus, Axiom 2 holds for all measures except 030 (i.e. 000 and 010). Axiom 3 is false for 330, and true for 331. Axiom 5 is false for 330 and 011, and true for 001, 101, and 111. Proof. Axiom 2 is false for 030 (i.e. 000 and 010). A counterexample is the term (x:x\Omega )(KI).x:x\Omega is 030-active, but the whole term reduces to the normal form I. It is true for 133, since x:s cannot be 133-active. The remaining depth measures are 031. For these we argue thus: if (x:s)t is reducible to a 031-stable term, then so is s[x := t]. By Axiom 3 (proved below), this implies that s is also. Axiom 3 is false for 330. A counterexample isx\Omega . This is 330-active, but its instance KI\Omega is not. The axiom is true for 331. Let s be 331-active, and consider any reduction d of s[x := t] to a term r. We must pr... | |||||||||||||
Details der Publikation | |||||||||||||
| |||||||||||||