We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

Abstract We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Σ1 level of the Mints hierarchy in first-order intuitionistic logic. It follows that Σ1 formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in Theory and Practice of Logic Programming

We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co- 2-N exptime . Our approach is to represent proof-search as computation of an alternating automaton. The memory of the automaton is structured in a way that strictly corresponds to scopes of the binders used in the constructed proof. This provides an application of automata-theoretic techniques in proof theory.

Beauty is truth, truth beauty -that is all Ye know on earth,

Is is shown that the inhabitation problem is decidable for intersection type assignment without the intersection elimination rule.

Abstract There is a simple technique, due to Dragalin. for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop's ι-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings; it is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus.

The purpose of this note is to give a methodologically simple proof of the undecidability of strong normalisation in the pure lambda calculus. For this we show how to represent an arbitrary partial recursive function by a term whose application to any Church numeral is either strongly normalizable or has no normal form. Intersection types are used for the strong normalization argument.

Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculus λ2 (System F) in several different ways, depending on the choice of the elimination operator. We compare several such definitions and we show that they fall into two equivalence classes with respect to mutual interpretability by means of beta-eta reductions. Elimination operators for fixpoint types are thus classified as either or recursors. This classification has an interpretation in terms of the Curry-Howard correspondence: types of iterators and recursors can be seen as images of induction axioms under different dependency-erasing maps. Systems with recursors are beta-eta equivalent to a calculus λ2U of recursive types with the operators Fold: σ[μα.σ/α]←μα.σ and Unfold: μα.σ←σ[μα.σ/α], where the composition Unfold or Fold reduces to identity.It is known that systems with iterators can be defined within λ2, by means of beta reductions. We conjecture that systems with recursors can not. In this paper we show that the system λ2U does not have such a property. For this we study the notion of polymorphic type embeddability (via (beta) left-invertible terms) and we show that if a type σ is embedded into another type τ then τ must be of depth at least equal to the depth of σ.

There are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-order λ -calculus F of Girard and Reynolds without affecting the typing power of the system. On the other hand we show that it is impossible to eliminate alpha-conversion on universally quantified variables in the higher-order λ -calculus F ω of Girard, by exhibiting a term which is typable in F ω with alpha-conversion but not typable in F ω without alpha-conversion.

Abstract We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of “strong conjunction” of Mints and Lopez-Escobar is also undecidable.

The main result of the paper is a proof of the following equivalence: two pure lambda terms are observationally equivalent in the lazy concurrent lambda calculus if they have the same Levy-Longo trees. It follows that contextual equivalence coincides with behavioural equivalence (bisimulation) as considered by Sangiorgi (1994). Another consequence is that the discriminating power of concurrent lambda contexts is the same as that of Boudol-Laneve's contexts with multiplicities (1996).

We investigate Girard's calculus Fω as a ‘Curry style’ type assignment system for pure lambda terms. First we show an example of a strongly normalizable term that is untypable in Fω. Then we prove that every partial recursive function is nonuniformly represented in Fω (even if quantification is restricted to constructor variables of level 1). It follows that the type reconstruction problem is undecidable and cannot be recursively separated from normalization.

We prove that the subtyping problem induced by Mitchell's containment relation (1988) for second-order polymorphic types is undecidable. It follows that type-checking is undecidable for the polymorphic lambda-calculus extended by an appropriate subsumption rule.

We consider several different definitions of type assignment with positive recursive types, from the point of view of their typing ability. We discuss the relationships between these systems. In particular, we show that the class of typable pure lamb

We prove that it is undecidable whether a given intersection type is non-empty, i.e., whether there exists a closed term of this type.>

We carry out an analysis of typability of terms in ML. Our main result is that this problem is DEXPTIME-hard, where by DEXPTIME we mean DTIME(2 n 0(1) ). This, together with the known exponential-time algorithm that solves the problem, yields the DEXPTIME-completeness result. This settles an open problem of P. Kanellakis and J. C. Mitchell. Part of our analysis is an algebraic characterization of ML typability in terms of a restricted form of semi-unification, which we identify as acyclic semi-unification . We prove that ML typability and acyclic semi-unification can be reduced to each other in polynomial time. We believe this result is of independent interest.

We study the problem of type-checking functional programs in three extensions of ML.One distinguishing feature of these extensions is that they allow recursive definitions to be polymorphically typed.Although the motivation for these extensions comes from pragmatic considera-

Finitely typed functional programs are naturally classified by their levels. This syntactic classification of functional programs corresponds to a semantical classification: the higher the level of functional programs, the more functions they can compute. We call FL the language of finitely typed functional programs. The halting problem on finite interpretations is elementary recursive for every FL program, i.e. for every FL program P there is an elementary recursive procedure to decide for every finite interpretation I whether P halts on I. The well-known programming language ML is essentially FL, augmented with the polymorphic let-in constructor. We show that ML computes the same class of functions as FL. As a consequence.

The Semi-Unification Problem (SUP) is a natural generalization of both first-order unification and matching.The problem arises in various branches of computer science and logic.Although several special cases of SUP are known to be decidable, the problem in general has been open for several years.We show that SUP in general is undecidable, by reducing what we call the "boundedness problem" of Turing machines to SUP.The undecidability of this boundedness problem is established by a technique developed in the mid-1960's to prove related results about Turing machines,

A generalization of first-order unification, called semiunification, is studied with two goals in mind: (1) type-checking functional programs relative to an improved polymorphic type discipline; and (2) deciding the typability of terms in a restricted form of the polymorphic lambda -calculus.>

ML/sup +/ is an extension of the functional language ML that allows the actual parameters of recursively called functions to have types that are generic instances of the (derived) types of corresponding formal parameters. It is shown that the polymorphism allowed by the original ML can be eliminated without loss of computational power, specifically, it is shown that its computational power (in all interpretations) is the same as that of finitely typed functional programs. It is proved that the polymorphism of ML/sup +/ cannot be eliminated, in that its computational power far exceeds that of finitely typed functional programs and therefore that of the original ML too.>

We extend the functional language ML by allowing the recursive calls to a function F on the right-hand side of its definition to be at different types, all generic instances of the (derived) type of F on the left-hand side of its definition. The original definition of ML does not allow this feature. This extension does not produce new types beyond the usual universal polymorphic types of ML and satisfies the properties already enjoyed by ML: the principal-type property and the effective type-assignment property.

The aim of this paper is to show that some open problems in Comparative Schematology and in Logics of Programs are equivalent to open problems in Complexity Theory. In particular we show that PSPACE = PTIME holds if and only if flow-diagrams with arrays are of the same computational power as recursive procedures. These statements are also equivalent to the following statement: Logics based on the above-mentioned classes of program schemes have equal expressive power. A similar characterization may be given for other complexity classes.