arXiv subjects
Publications and source records attributed to Richard Statman.
We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $\lambda$-definability conjecture implies the higher-order matching conjecture.
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Veneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term $M$ admits a *uniqueness typing*, which is a pair $(\Gamma,A)$ such that 1) $\Gamma \vdash M : A$ 2) $\Gamma \vdash N : A \Longrightarrow M =_{\beta\eta} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.
We consider certain decision problems for the free model of the theory of Cartesian monoids. We introduce a model of computation based on the notion of a single stack one-way PDA due to Ginsburg, Greibach and Harrison. This model allows us to solve problems such as (1) Given a finite set B of elements and an element F, is F a product of members of B? (2) Is the submonoid generated by the finite set B infinite? for certain fragments of the free Cartesian monoid. These fragments include the submonoid of right invertible elements and so our results apply to the Thompson-Higman groups.
Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair $(\Gamma,A)$ such that 1) $\Gamma \vdash M : A$ 2) $\Gamma \vdash N : A \Longrightarrow M =_{\beta\eta} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules. Moreover, we show that the set of closed terms with a given type is uniformly separable, and, if infinite, forms an adequate numeral system. The proof of this fact uses an internal version of the B\"ohm-out technique, adapted to terms of a given intersection type.
In a functional calculus, the so called \Omega-rule states that if two terms P and Q applied to any closed term N return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the \lambda\beta-calculus the \Omega-rule does not hold, even when the \eta-rule (weak extensionality) is added to the calculus. A long-standing problem of H. Barendregt (1975) concerns the determination of the logical power of the \Omega-rule when added to the \lambda\beta-calculus. In this paper we solve the problem, by showing that the resulting theory is \Pi\_{1}^{1}-complete.
H is the theory extending β-conversion by identifying all closed unsolvables. H ω is the closure of this theory under the ω-rule (and β-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of H ω form Π 1 1 -complete set. Here we prove that conjecture.