Title :
The omega rule is Π20-hard in the λβ-calculus
Author :
Intrigila, Benedetto ; Statman, Richard
Author_Institution :
Univ. degli Studi di L´´Aquila, Italy
Abstract :
We give a many-one reduction of the set of true Π20 sentences to the set of consequences of the lambda calculus with the omega rule. This solves in the affirmative a well known problem of H. Barendregt. The technique of proof has interest in itself and can be extended to prove that the theory which identifies all unsolvable terms together with the omega rule is H11-complete which solves another long-standing conjecture of H. Barendregt.
Keywords :
computational complexity; lambda calculus; pi calculus; Π20 sentences; Π20-hard; λβ-calculus; H11-complete; many-one set reduction; omega rule; proof technique; unsolvable terms; Automation; Calculus; Character generation; Computer science; Logic; Terminology;
Conference_Titel :
Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on
Print_ISBN :
0-7695-2192-4
DOI :
10.1109/LICS.2004.1319614
