We prove Church’s lambda calculus semigroup is sq-universal.

Solving the Entscheidungsproblem was a challenge first posed by David Hilbert in 1928, and solutions to decision problems are perhaps the most prized posessions in logic. Pawel Urzyczyn has a number of these, one of which I will discuss below. However, let me remind you of Michael Rabin describing his time with Dana Scott at IBM prior to their Turing award winning paper Finite automata and their decision problems “So we both went, in 1957 to IBM and the location was the so-called Lamb Estate [Robert S. Lamb estate], a wonderful place, while the Princeton Laboratory, designed by Sarason, the Watson Laboratory was in stages of construction. The Lamb Estate, very appropriately, used to be, before that, an Insane Asylum. All those buildings were building where kooks were housed...” [1]. This is what IBM thought of decision problems. In this note we give a new proof of the undecidability of the inhabitation problem for intersection types.

A natural question in the λ-calculus asks what is the possible number of fixed points of a combinator (closed term). A complete answer to this question is still missing (Problem 25 of TLCA Open Problems List) and we investigate the related question about the number of fixed points of a combinator in λ-theories. We show the existence of a recursively enumerable lambda theory where the number is always one or infinite. We also show that there are λ-theories such that some terms have only two fixed points. In a first example, this is obtained by means of a non-constructive (more precisely non-r.e.) λ-theory where the range property is violated. A second, more complex example of a non-r.e. λ-theory (with a higher unsolvability degree) shows that some terms can have only two fixed points while the range property holds for every term.

In Barendregt (1984), Corrado Böhm conjectured that every adequate (Barendregt 1984, 6.4.2 (ii)) numeral system of normal combinators has normal successor, predecessor and zero test. In this note, we give a counterexample to this conjecture. Our example is shown to have no normal zero test. Böhm has informed us that Intrigila (1994) has given an example with no normal successor. Our strategy, in terms of the ant-lion paradigm, is to pry open the trap so wide that it enters its active state before its jaws are shut.

We consider an operator definable in the intuitionistic theory of monadic predicates and we axiomatize some of its properties in a definitional extension of that monadic logic. The axiomatization lends itself to a natural deduction formulation to which the Curry-Howard isomorphism can be applied. The resulting Church style type system has the property that an untyped term is typable if and only if it is strongly normalizable.

The λ-theory ℋ is obtained from β-conversion by identifying all closed unsolvable terms (or, equivalently, terms without head normal form). The range problem for the theory ℋ asks whether a closed term has always (up to equality in ℋ) either an infinite range or a singleton range (that is, it is a constant function). Here we give a solution to a natural version of this problem, giving a positive answer for the theory ℋ restricted to Combinatory Logic. The method of proof applies also to the Lazy λ-Calculus.

Abstract We consider three problems concerning alpha conversion of closed terms (combinators). (1) Given a combinator M find the an alpha convert of M with a smallest number of distinct variables. (2) Given two alpha convertible combinators M and N find a shortest alpha conversion of M to N. (3) Given two alpha convertible combinators M and N find an alpha conversion of M to N which uses the smallest number of variables possible along the way. We obtain the following results. (1) There is a polynomial time algorithm for solving problem (1). It is reducible to vertex coloring of chordal graphs. (2) Problem (2) is co-NP complete (in recognition form). The general feedback vertex set problem for digraphs is reducible to problem (2). (3) At most one variable besides those occurring in both M and N is necessary. This appears to be the folklore but the proof is not familiar. A polynomial time algorithm for the alpha conversion of M to N using at most one extra variable is given. There is a tradeoff between solutions to problem (2) and problem (3) which we do not fully understand.

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 Π11-complete set. Here we prove that conjecture.

We give a many-one reduction of the set of true /spl Pi//sub 2//sup 0/ sentences to the set of consequences of the lambda calculus with the omega rule. This solves in the affirmative a well known problem of H. Barendregt. The technique of proof has interest in itself and can be extended to prove that the theory which identifies all unsolvable terms together with the omega rule is H/sub 1//sup 1/-complete which solves another long-standing conjecture of H. Barendregt.

In this paper we consider three problems concerning the lambda Y calculus obtained from the simply typed lambda calculus by the addition of fixed point combinators Y: (A/spl rarr/A)/spl rarr/A. The "paradoxical" combinator Y was first discussed in by Curry & Feys Vol 1 (1958). It appears first in a typed context by A. Scott (1969) and also by R. Platek's thesis (1963), and forms the basis for L. C. F. (1980) and its descendants. In this paper we shall consider (1) the question of whether higher type Y are "definable" from lower type Y. We shall show that it is not the case in this context, sharpening a result of ours from [8]. A similar result has been obtained by Warner Damm; (2) the question of the decidability of termination. More precisely, we shall show that it is decidable whether a given term has a normal form. This extends results of Plotkin and Bercovicci. [2]. By similar methods we show that we show that it is decidable whether a term has a head normal form, and whether a term has a finite Bohm tree; (3) the question of the decidability of the word problem. This question was first put to us by Albert Meyer 20 years ago. We shall show that it is in general undecidable whether two lambda Y terms convert. This is done by encoding the behavior of register machines. In addition we shall give a decision procedure for the special case of only Y's of type (0/spl rarr/0)/spl rarr/0.

This theoretical pearl is about the closed term model of pure untyped lambda-terms modulo β-convertibility. A consequence of one of the results is that for arbitrary distinct combinators (closed lambda terms) M , M ′, N , N ′ there is a combinator H such that formula here The general result, which comes from Statman (1998), is that uniformly r.e. partitions of the combinators, such that each ‘block’ is closed under β-conversion, are of the form { H −1 { M }} M ∈Λ Φ . This is proved by making use of the idea behind the so-called Plotkin-terms, originally devised to exhibit some global but non-uniform applicative behaviour. For expository reasons we present the proof below. The following consequences are derived: a characterization of morphisms and a counter-example to the perpendicular lines lemma for β-conversion.

Abstract Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show that an important subcase, namely unification modulo thelinear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming.

An axiomatization of the isomorphisms that hold in all Cartesian closed categories (CCCs), discovered independently by S.V. Soloviev (1983) and by K.B. Bruce and G. Longo (1985), leads to seven equalities. It is shown that the unification problem for this theory is undecidable, thus setting an open question. It is also shown that an important subcase, namely unification modulo the linear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by M. Rittri (1990, 1991). It also has potential applications to the problem of polymorphic higher-order unification, which in turn is relevant to theorem proving, logic programming, and type reconstruction in higher-order languages.>

Retractions existing in all models of simply typed lambda -calculus are studied and related to other relations among types, such as isomorphisms, surjections, and injections. A formal system to deduce the existence of such retractions is shown to be sound and complete with respect to retractions definable by linear lambda -terms. Results aiming at a system complete with respect to the provable retractions tout court are established.>

The Freyd hierarchy of monoids is introduced. The Freyd hierarchy is a fragment of type-free combinatory algebra lambda -calculus that has some remarkable properties, some of which are presented. One result characterizes the combinators in the hierarchy in terms of some simple ideas from the theory of rewrite rules. The computational/expressive power of the fragment is studied. This includes not only the functions computable by the combinators but also the varieties definable by combinator equations. Certain extraordinary connections between the lowest level of the hierarchy, combinatorics, and topology are also included.>

The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard β-ε axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. Without a little care about variable elimination, the standard rules are not even sound for empty types. We extend the standard system to obtain a complete proof system for models with empty types. The completeness proof is complicated by the fact that equational “term models” are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.

An Armstrong relation for a set of functional dependencies (FDs) is a relation that satisfies each FD implied by the set but no FD that is not implied by it.The structure and size (number of tuples) of Armstrong relatsons are investigated.Upper and lower bounds on the size of minimal-sized Armstrong relations are derived, and upper and lower bounds on the number of distinct entries that must appear m an Armstrong relation are given.It is shown that the time complexity of finding an Armstrong relation, gwen a set of functional dependencies, is precisely exponential in the number of attributes.Also shown ,s the falsity of a natural conjecture which says that almost all relations obeying a given set of FDs are Armstrong relations for that set of FDs.Finally, Armstrong relations are used to generahze a result, obtained by Demetrovics using quite complicated methods, about the possible sets of keys for a relauon.

In [4] Gordon Plotkin considers the problem of characterizing the λ-definable functionals in full type structures. A plausible, but, as we shall see, quite false, conjecture is that a functional is λ-definable ⇔ it is invariant in the sense of Fraenkel and Mostowski. A better guess might be that the set of λ-definable functionals of type σ has a uniform (in σ) definition in type theory over all full type structures (Plotkin explicitly considers a certain sort of definition by means of “logical relations”). More or less generally, one may ask if the following question is decidable. Given: a functional F in a full type structure over a finite ground domain. Question: is Fλ-definable? We call the statement that this question is decidable Plotkin's λ-definability conjecture. We do not know if Plotkin's conjecture is true. In this note we consider several questions which quickly arise from Plotkin's conjecture. In §1, we ask which type structures satisfy λ-definability = invariance. We construct for each consistent set of equations a model satisfying this equality. From consideration of these models we obtain a number of syntactic corollaries including a reduction of βη-conversion to βη-conversion at a single type (Theorem 3), an “ω-rule” for βη-conversion (Proposition 6) and consistency with βη-conversion (Proposition 8), definability and indefinability results for versions of Kronecker's δ (Propositions 10 and 11), and a decidability result for the problem of inter-definability among combinators.

Input resolution with paramodulation is a theorem proving procedure complete for sets of unit clauses with equality. This procedure recommends itself because it is easy to implement, and several implementations are in use in more general theorem proving programs. In this note we show that input resolution with paramodulation requires, in the worst case, proofs of exponential length even though the satisfiability problem for sets of unit clauses can be solved in polynomial time.

Historically, the principal interest in the typed λ-calculus is in connection with Godel's functional ("Dialectica") interpretation'of intuitionistic arithmetic. However, since the early sixties interest has shifted to a wide variety of applications in diverse branches of logic, algebra, and computer science. For example, in proof-theory, in constructive logic, in the theory of functionals, in cartesian closed categories, in automatic theorem proving, and in the semantics of natural languages. In almost all such applications there is a point at which one must ask, for closed terms t1and t2, whether t1β-converts to t2. We shall show that in general this question cannot be answered by a Turing machine in elementary time. We shall also investigate the computational complexity of related questions concerning the typed. λ-calculus (for example, the question of whether a given type contains a closed term).