TY - JOUR

T1 - Normal Proofs and Their Grammar

AU - Takahashi, Masako

AU - Akama, Yohji

AU - Hirokawa, Sachio

PY - 1996/3/15

Y1 - 1996/3/15

N2 - We present grammatical (or equational) descriptions of the set of normal inhabitants {M | Γ ⊢ M : A, M in β-normal form} of a given type A under a given basis Γ, both for the standard simple type system (in the partial discharge convention) and for the system in the total discharge convention (or the Prawitz-style natural deduction system). It is shown that in the latter system we can describe the set by a (finite) context-free grammar, but for the standard system this is not necessarily the case because we may need an infinite supply of fresh (bound) variables to describe the set. In both cases, however, our grammars reflect the structure of normal inhabitants in such a way that, when non-terminals are ignored, a derivation tree of the grammars yielding a λ-term M can be identified with Böhm tree of M. We give some applications of the grammatical descriptions. Among others, we give simple algorithms for the emptiness/finiteness problem of the set of normal inhabitants of a given type (both for the standard and non-standard systems).

AB - We present grammatical (or equational) descriptions of the set of normal inhabitants {M | Γ ⊢ M : A, M in β-normal form} of a given type A under a given basis Γ, both for the standard simple type system (in the partial discharge convention) and for the system in the total discharge convention (or the Prawitz-style natural deduction system). It is shown that in the latter system we can describe the set by a (finite) context-free grammar, but for the standard system this is not necessarily the case because we may need an infinite supply of fresh (bound) variables to describe the set. In both cases, however, our grammars reflect the structure of normal inhabitants in such a way that, when non-terminals are ignored, a derivation tree of the grammars yielding a λ-term M can be identified with Böhm tree of M. We give some applications of the grammatical descriptions. Among others, we give simple algorithms for the emptiness/finiteness problem of the set of normal inhabitants of a given type (both for the standard and non-standard systems).

UR - http://www.scopus.com/inward/record.url?scp=0346089929&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0346089929&partnerID=8YFLogxK

U2 - 10.1006/inco.1996.0027

DO - 10.1006/inco.1996.0027

M3 - Article

AN - SCOPUS:0346089929

SN - 0890-5401

VL - 125

SP - 144

EP - 153

JO - Information and Computation

JF - Information and Computation

IS - 2

ER -