Related papers: Statman's Hierarchy Theorem
We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contribution is placed in the context of the search for a natural,…
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.
From the analogue of Boehm's Theorem proved for the typed lambda calculus, without product types and with them, it is inferred that every cartesian closed category that satisfies an equality between arrows not satisfied in free cartesian…
The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $\beta\eta$-normal forms.…
A longstanding open problem is whether there exists a non-syntactical model of untyped lambda-calculus whose theory is exactly the least equational lambda-theory (=Lb). In this paper we make use of the Visser topology for investigating the…
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type rule. In this work, we argue that…
A longstanding open problem is whether there exists a non syntactical model of the untyped lambda-calculus whose theory is exactly the least lambda-theory (l-beta). In this paper we investigate the more general question of whether the…
The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between B\"ohm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal…
One takes advantage of some basic properties of every homotopic $\lambda$-model (e.g.\ extensional Kan complex) to explore the higher $\beta\eta$-conversions, which would correspond to proofs of equality between terms of a theory of…
We present a full formalization in Martin-L\"of's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple…
In this paper we consider a type system with a universal type $\omega$ where any term (whether open or closed, $\beta$-normalising or not) has type $\omega$. We provide this type system with a realisability semantics where an atomic type is…
We consider the following decision problem: given two simply typed $\lambda$-terms, are they $\beta$-convertible? Equivalently, do they have the same normal form? It is famously non-elementary, but the precise complexity - namely…
This paper expands on existing learned models of human behavior via a measured step in structured irrationality. Specifically, by replacing the suboptimality constant $\beta$ in a Boltzmann rationality model with a function over states…
It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant…
Many first-order equational theories, such as the theory of groups or boolean algebras, can be presented by a smaller set of axioms than the original one. Recent studies showed that a homological approach to equational theories gives us…
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not simultaneously satisfied in any partially ordered model…
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry…
In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidding a type from quantifying over all types. Instead, the…
A system $\boldsymbol\lambda_{\theta}$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory…
Generalized Higman's Theorem is the direct counterpart of Higman's Theorem that asserts the closure of the class of \emph{better} quasi-orders, instead of the class of \emph{well} quasi-orders, under the construction $P\mapsto P^{<\omega}$…