• DocumentCode
    3260592
  • Title

    The omega rule is Π20-hard in the λβ-calculus

  • Author

    Intrigila, Benedetto ; Statman, Richard

  • Author_Institution
    Univ. degli Studi di L´´Aquila, Italy
  • fYear
    2004
  • fDate
    13-17 July 2004
  • Firstpage
    202
  • Lastpage
    210
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-2192-4
  • Type

    conf

  • DOI
    10.1109/LICS.2004.1319614
  • Filename
    1319614
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3260592