Generalized numberings are an extension of Ershov's notion of numbering, based on partial combinatory algebra (pca) instead of the natural numbers. We study various algebraic properties of generalized numberings, relating properties of the numbering to properties of the pca. As in the lambda calculus, extensionality is a key notion here.

In the Simply Typed $\lambda$-calculus Statman investigates the reducibility relation $\leq_{\beta\eta}$ between types: for $A,B \in \mathbb{T}^0$, types freely generated using $\rightarrow$ and a single ground type $0$, define $A \leq_{\beta\eta} B$ if there exists a $\lambda$-definable injection from the closed terms of type $A$ into those of type $B$. Unexpectedly, the induced partial order is the (linear) well-ordering (of order type) $\omega + 4$. In the proof a finer relation $\leq_{h}$ is used, where the above injection is required to be a B\"ohm transformation, and an (a posteriori) coarser relation $\leq_{h^+}$, requiring a finite family of B\"ohm transformations that is jointly injective. We present this result in a self-contained, syntactic, constructive and simplified manner. En route similar results for $\leq_h$ (order type $\omega + 5$) and $\leq_{h^+}$ (order type $8$) are obtained. Five of the equivalence classes of $\leq_{h^+}$ correspond to canonical term models of Statman, one to the trivial term model collapsing all elements of the same type, and one does not even form a model by the lack of closed terms of many types.

Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.

Abstract. Happiness and suffering are both the result of two factors combined: the situation in which one is placed and our consciousness of it. Happiness is not only of personal importance, it is also a necessary factor for ensuring peace in society. Therefore it is important to know the two possible ways for the pursuit of happiness: applied science, which focuses on how situations can be controlled, and spirituality, which focuses on developing the various types of consciousness one can have. The notion of purified consciousness is formulated in terms of psychology, neurophysiology, logic and meditative practice.

The following claims will be made.

It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λ N ) and the other to sequent calculus (λ L ). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a ‘cut-free’ fragment (λ L cf ). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms possess a normal form.

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 Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, [3], we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions.

A term rewriting system is called complete if it is confluent and terminating.We prove that completeness of TRSS is a "modular" property (meaning that it stays preserved under direct sums), provided the constituent TRSS are left-linear.Here, the direct sum RO S3R ~is the union of TRSS R., RI with disjoint signature.The proof hinges crucially upon the (non)deterministic collapsing behavior of terms from the sum TRS.

Abstract Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).

Abstract A closed λ-term E is called an enumerator if Here ⋀ 0 is the set of closed λ-terms,. is the set of natural numbers and the ⌜ n ⌝ are the Church's numerals λ fx . f n x . Such an E is called reducing if, moreover An ingenious recursion theoretic proof by Statman will be presented, showing that every enumerator is reducing. I do not know any direct proof.

Abstract Let ψ be a partial recursive function (of one argument) with λ-defining term F ∈Λ°. This means There are several proposals for what F ⌜ n ⌝ should be in case ψ( n ) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman). These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.

Abstract Programming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems have appeared, so there is some need of classification. Working towards a taxonomy, Barendregt (1991) gives a fine-structure of the theory of constructions (Coquand and Huet 1988) in the form of a canonical cube of eight type systems ordered by inclusion. Berardi (1988) and Terlouw (1988) have independently generalized the method of constructing systems in the λ-cube. Moreover, Berardi (1988, 1990) showed that the generalized type systems are flexible enough to describe many logical systems. In that way the well-known propositions-as-types interpretation obtains a nice canonical form.

Programming languages which are capable of interpreting themselves have been fascinating computer scientists. Indeed, if this is possible then a ‘strange loop’ (in the sense of Hofstadter, 1979) is involved. Nevertheless, the phenomenon is a direct consequence of the existence of universal languages. Indeed, if all computable functions can be captured by a language, then so can the particular job of interpreting the code of a program of that language. Self-interpretation will be shown here to be possible in lambda calculus. The set of λ-terms , notation Λ, is defined by the following abstract syntax where is the set {v, v′, v″, v′″,…} of variables . Arbitrary variables are usually denoted by x, y,z,… and λ -terms by M,N,L,…. A redex is a λ -term of the form that is, the result of substituting N for (the free occurrences of) x in M. Stylistically, it can be said that λ -terms represent functional programs including their input. A reduction machine executes such terms by trying to reduce them to normal form; that is, redexes are continuously replaced by their contracta until hopefully no more redexes are present. If such a normal form can be reached, then this is the output of the functional program; otherwise, the program diverges.

In [6, p. 317] Curry described a formal system assigning types to terms of the type-free λ -calculus. In [11] Scott gave a natural semantics for this type assignment and asked whether a completeness result holds. Inspired by [4] and [5] we extend the syntax and semantics of the Curry types in such a way that filters in the resulting type structure form a domain in the sense of Scott [12]. We will show that it is possible to turn the domain of types into a λ -model, among other reasons because all λ -terms possess a type. This model gives the completeness result for the extended system. By a conservativity result the completeness for Curry's system follows. Independently Hindley [8], [9] has proved both completeness results using term models. His method of proof is in some sense dual to ours. For λ -calculus notation see [1].

Summary A λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Gödel numbers of its elements. is the λ-theory axiomatized by the set {M = N∣ M, N unsolvable}. A λ-theory is sensible iff T ⊃ ; for a motivation see [6] and [4]. In §1 it is proved that the theory is Σ20-complete. We present Wadsworth's proof that its unique maximal consistent extension * (= Th(D∞)) is Π20-complete. In §2 it is proved that η (= λη-calculus + ) is not closed under the ω-rule (see [1]). In §3 arguments are given to conjecture that is Π11-complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in ω. In §4 an infinite set of equations independent over η will be constructed. From this it follows that there are 2ℵ0 sensible theories T such that and 2ℵ0 sensible hard models of arbitrarily high degrees. In §5 some nonprovability results needed in §§1 and 2 are established. For this purpose one uses the theory η extended with a reduction relation for which the Church–Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct.

The theorem proved in this paper answers some transitivity questions (in the geometric sense) for the type free λ-calculus: Which objects can be mapped on all other objects? How much can an object do by applying it to other objects (see footnote 2)? The main result is that, for closed terms of the λI-calculus, the following conditions are equivalent: (a) M has a normal form. (b) FM = I for some λI-term F. (c) MN1 … Nn = I for some λI-terms N1 …, Nn. By the same method it follows that if M is a closed term of the λK-calculus having a normal form, then for some λI-terms (sic) N1, …, Nn, MN1… Nn = I is provable in the λK-calculus. The theorem of Böhm [2] states that if M1, M2 are terms of the λK-calculus having different βη-normal forms, then ∀A1, A2 ∃N1, …, NnMiN1 … Nn = Ai is provable in the λK-βη-calculus for i = 1, 2. As a consequence of this it was shown (implicitly) in [1, 3.2.20 1/2 (1)] that if M has a normal form, then for some λK-terms N1, …, Nn, MN1 … Nn =I is provable in the λK-calculus. It was not clear that this also could be proved for the λK-calculus since the proof of the theorem of Böhm essentially made use of λK-terms. We conjecture that, using the results of this paper, the full theorem of Böhm can be proved for the λI-calculus.