The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed [lgr]-calculus, i.e. to solve the equation a = b where a and b are simply typed [lgr]-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occuring in the problem are at most third order.

Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of (...) modal or intuitionistic logics, Kripke lambda models are likely to seem adequately ‘semantic’. However, when viewed as cartesian closed categories, they do not have the property variously referred to as concreteness, well- pointedness or having enough points. While the traditional lambda calculus proof system is not complete for Henkin models that may have empty types, we prove strong completeness for Kripke models. In fact, every set of equations that is closed under implication is the theory of a single Kripke model. We also develop some properties of logical relations over Kripke structures, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model. We discuss cartesian closed categories but present the main definitions and results without the use of category theory. (shrink)

In the Böhm theorem workshop on Crete, Zoran Petric called Statman’s “Typical Ambiguity theorem” the typed Böhm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Böhm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit the weak typed Böhm theorem holds. The system IMLL (...) exactly corresponds to the linear lambda calculus with multiplicative pairing. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner. (shrink)

Some sufficient conditions on a Symmetric Monoidal Closed category K are obtained such that a diagram in a free SMC category generated by the set A of atoms commutes if and only if all its interpretations in K are commutative. In particular, the category of vector spaces on any field satisfies these conditions . Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered . Two derivations of the same sequent are equivalent if and only if (...) all their interpretations in K are equal. In fact, the assignment of values to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R. Voreadou's proof of the “abstract coherence theorem” found by the author, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of S. Mac Lane conjecture also proves the correctness of the modified description. (shrink)

The λY calculus is the simply typed λ calculus augmented with the fixed point operators. We show three results about λY: the word problem is undecidable, weak normalisability is decidable, and higher type fixed point operators are not definable from fixed point operators at smaller types.

We define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A: → Preor equipped with certain natural transformations corresponding to application and abstraction . We (...) make use of an explicit construction of the exponential of functors in the Cartesian-closed category Preor, and we also define a kind of exponential ΠΦs ε T to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery . We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities. (shrink)