The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and (...) give a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system. (shrink)

The lambda-calculus lies at the very foundation of computer science. Besides its historical role in computability theory it has had significant influence on programming language design and implementation, denotational semantics and domain theory. The book emphasizes the proof theory for the type-free lambda-calculus. The first six chapters concern this calculus and cover the basic theory, reduction, models, computability, and the relationship between the lambda-calculus and combinatory logic. Chapter 7 presents a variety of typed calculi; first the (...) simply typed lambda-calculus, then Milner-style polymorphism and, finally the polymporphic lambda-calculus. Chapter 8 concerns three variants of the type-free lambda-calculus that have recently appeared in the research literature: the lazy lambda-calculus, the concurrent y-calculus and the lamdba omega-calculus. The final chapter contains references and a guide to further reading. There are exercises throughout. In contrast to earlier books on these topics, which were written by logicians, the book is written from a computer science perspective and emphasizes the practical relevance of many of the key theoretical ideas. The book is intended as a course text for final year undergraduates or first year graduate students in computer science. Research students should find it a useful introduction to more specialist literature. (shrink)

This paper gives the strong reduction of the combinatory calculus SCL, which was introduced as a combinatory calculus corresponding to the untyped Lambda-mu calculus. It proves the confluence of the strong reduction. By the confluence, it also proves the conservativity of the extensional equality of SCL over the combinatory calculus CL, and the consistency of SCL.

The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language Λ! and a categorical model for it.The terms of Λ! encode (...) a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of Λ! are built out of two disjoint sets of variables. Moreover, the λ-abstractions of Λ! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of Λ!, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language Λ! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction.The categorical model induces operational equivalences like, for example, a set of extensional equivalences.The paper presents also an untyped version of Λ! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from Λ! all the good computational properties and enjoys also the Principal-Type Property. (shrink)

This paper describes a novel pedagogical software program that can be seen as an online companion to one of the standard textbooks of formal natural language semantics, Heim and Kratzer (1998). The Penn Lambda Calculator is a multifunctional application designed for use in standard graduate and undergraduate introductions to formal semantics: Teachers can use the application to demonstrate complex semantic derivations in the classroom and modify them interactively, and students can use it to work on problem sets provided by (...) the teacher. The program supports demonstrations and exercises in two main areas: (1) performing beta reduction in the simply typed lambda calculus; (2) application of the bottom-up algorithm for computing the compositional semantics of natural language syntax trees. The program is able to represent the full range of phenomena covered in the Heim and Kratzer textbook by function application, predicate modification, and lambda abstraction. This includes phenomena such as intersective adjectives, relative clauses and quantifier raising. In the student use case, emphasis has been placed on providing “live” feedback for incorrect answers. Heuristics are used to detect the most frequent student errors and to return specific, interactive suggestions. (shrink)

Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, (...) we introduce an untyped term calculus, called Light Affine Lambda Calculus (λLA), which corresponds to ILAL. λLA is a bi-modal λ-calculus with certain constraints, endowed with very simple reduction rules. The main property of LALC is the polynomial time strong normalization: any reduction strategy normalizes a given λLA term in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs of ILAL are structurally representable by terms of λLA, we conclude that the same holds for ILAL. (shrink)

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 Godel numbers of its elements. H is the $\lamda$ -theory axiomatized by the set {M = N ∣ M, N unsolvable. A $\lamda$ -theory is sensible $\operatorname{iff} T \supset \mathscr{H}$ , for a motivation see [6] and [4]. In § it is proved that the theory H is ∑ 0 2 -complete. We present Wadsworth's proof (...) that its unique maximal consistent extention $\mathscr{H}^\ast (= \mathrm{T}(D_\infty))$ is Π 0 2 -complete. In $\S2$ it is proved that $\mathscr{H}_\eta(= \lambda_\eta-\text{Calculus} + \mathscr{H})$ is not closed under the ω-rule (see [1]). In $\S3$ arguments are given to conjecture that $\mathscr{H}\omega (= \lambda + \mathscr{H} + omega-rule)$ is Π 1 1 -complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in Hω. In $\S4$ an infinite set of equations independent over H η will be constructed. From this it follows that there are 2^{ℵ_0 sensible theories T such that $\mathscr{H} \subset T \subset \mathscr{H}^\ast$ and 2 ℵ 0 sensible hard models of arbitrarily high degrees. In $\S5$ some nonprovability results needed in $\S\S1$ and 2 are established. For this purpose one uses the theory H η 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. (shrink)

We consider reducts of the structure $\mathscr{R} = \langle\mathbb{R}, +, \cdot, <\rangle$ and other real closed fields. We compete the proof that there exists a unique reduct between $\langle\mathbb{R}, +, <, \lambda_a\rangle_{a\in\mathbb{R}}$ and R, and we demonstrate how to recover the definition of multiplication in more general contexts than the semialgebraic one. We then conclude a similar result for reducts between $\langle\mathbb{R}, \cdot, <\rangle$ and R and for general real closed fields.

This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s \-calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the \-calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional (...) Z theorem can be applied to prove confluence of the call-by-name and the call-by-value \-calculi with both simplification rules, the renaming and the \-rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants. (shrink)

We present an extension of the lambda calculus with the letrec construct. In contrast to current theories, which impose restrictions on where the rewriting can take place, our theory is very liberal, e.g., it allows rewriting under lambda abstractions and on cycles. As shown previously, the reduction theory is non-confluent. Thus, we searched for and found a new property that resembles confluence and that is equivalent to uniqueness of infinite normal forms: skew confluence. This notion is based (...) on the intuition that some terms are better than others and that terms reduce to better terms. It states that if a term reduces to two other terms, the second of those terms can always be reduced to a term that is better than the first. Using skew confluence we define the infinite normal form of a term and show that the infinite normal form defines a congruence on the set of terms. We relate the lambda calculus plus letrec to the plain lambda calculus and to one of the infinitary lambda calculi. We also present a variant of our calculus, which follows the tradition of the explicit substitution calculi. (shrink)

Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous (...) normal forms relate to derivations of strong normalizability in the typed λ-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel’s system , leading to a value table semantics for number-theoretic functions. (shrink)

In this paper, we present three methods to give the value of a classical integer in $\lambda\mu$ -calculus. The first method is an external method and gives the value and the false part of a normal classical integer. The second method uses a new reduction rule and gives as result the corresponding Church integer. The third method is the M. Parigot's method which uses the J.L. Krivine's storage operators.

Looking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to (...) analyse the role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory. (shrink)

We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard’s F (Proofs and types. Cambridge University Press, Cambridge, 1989). It is like the simple theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recursive (...) functionals of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by ${{\varepsilon}_0}$ -recursion which takes every typable term to a natural number which is an upper bound to the lengths of all βη-reduction sequences starting with that term. (shrink)

The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) (...) −→ (A −→ C)), respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S.. (shrink)

We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly (...) normalizing terms of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms. (shrink)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds (...) to term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free derivations—of a number (...) of well-known and central results concerning β- and βη-reduction. The latter include the Church–Rosser theorem for both reductions, the Standardization theorem for β- reduction, as well as the Normalization (Leftmost reduction) theorem and the Postponement of η-reduction theorem for βη-reduction. (shrink)

This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy (...) and van Oostrom, called the Z theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi. (shrink)

A reduction algebra is defined as a set with a collection of partial unary functions (called reduction operators). Motivated by the lambda calculus, the Church-Rosser property is defined for a reduction algebra and a characterization is given for those reduction algebras satisfying CRP and having a measure respecting the reductions. The characterization is used to give (with 20/20 hindsight) a more direct proof of the strong normalization theorem for the impredicative second order intuitionistic propositional calculus.

Translations from Lambda calculi into combinatory logics can be used to avoid some implementational problems of the former systems. However, this scheme can only be efficient if the translation produces short output with a small number of combinators, in order to reduce the time and transient storage space spent during reduction of combinatory terms. In this paper we present a combinatory system and an abstraction algorithm, based on the original bracket abstraction operator of Schonfinkel [9]. The algorithm introduces (...) at most one combinator for each abstraction in the initial Lambda term. This avoids explosive term growth during successive abstractions and makes the system suitable for practical applications. We prove the correctness of the algorithm and establish some relations between the combinatory system and the Lambda calculus. (shrink)

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 interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of (...) saturation (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity. As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that (...) the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said. (shrink)

Sections 1 through 4 define, in the usual inductive style, various classes of object including one which is called the “combinatory terms of polymorphic type”. Section 5 defines a reduction relation on these terms. Section 6 shows that the weak normalizability of the combinatory terms of polymorphic type entails the weak normalizability of the lambda terms of polymorphic type. The entailment is not vacuous, because the combinatory terms of polymorphic type are indeed weakly normalizable, as is proven in (...) Sect. 7 using Tait and Girard’s computability predicates. The remainder of the paper is devoted to arguing that interesting consequences would follow from the existence of an “ordinally informative” proof, i.e. one which uses transfinite induction over recursive ordinal numbers and otherwise finitary methods, of normalizability for as large a class of the terms as possible. (shrink)

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.

When the Canonical Ramsey’s Theorem by Erdős and Rado is applied to regressive functions, one obtains the Regressive Ramsey’s Theorem by Kanamori and McAloon. Taylor proved a “canonical” version of Hindman’s Theorem, analogous to the Canonical Ramsey’s Theorem. We introduce the restriction of Taylor’s Canonical Hindman’s Theorem to a subclass of the regressive functions, the $$\lambda $$ λ -regressive functions, relative to an adequate version of min-homogeneity and prove some results about the Reverse Mathematics of this Regressive Hindman’s Theorem (...) and of natural restrictions of it. In particular we prove that the first non-trivial restriction of the principle is equivalent to Arithmetical Comprehension. We furthermore prove that the well-ordering-preservation principle for base-$$\omega $$ ω exponentiation is reducible to this same principle by a uniform computable reduction. (shrink)

We prove the following algebraic characterization of elementary equivalence: $\equiv$ restricted to countable structures of finite type is minimal among the equivalence relations, other than isomorphism, which are preserved under reduct and renaming and which have the Robinson property; the latter is a faithful adaptation for equivalence relations of the familiar model theoretical notion. We apply this result to Friedman's fourth problem by proving that if L = L ωω (Q i ) i ∈ ω 1 is an (ω 1 (...) , ω)-compact logic satisfying both the Robinson consistency theorem on countable structures of finite type and the Löwenheim-Skolem theorem for some $\lambda for theories having ω 1 many sentences, then $\equiv_L = \equiv$ on such structures. (shrink)

Partial combinatory algebras (pcas) are algebraic structures that serve as generalized models of computation. In this article, we study embeddings of pcas. In particular, we systematize the embeddings between relativizations of Kleene’s models, of van Oosten’s sequential computation model, and of Scott’s graph model, showing that an embedding between two relativized models exists if and only if there exists a particular reduction between the oracles. We obtain a similar result for the lambda calculus, showing in particular that it (...) cannot be embedded in Kleene’s first model. (shrink)

In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general than the ones usually considered in literature, are inspired to the reductions of Felleisen's lambda calculus with continuations.

We tackle the problem of preservation of totality by composition in arena games. We first explain how this problem reduces to a finiteness theorem on what we call pointer structures, similar to the parity pointer functions of Harmer, Hyland and Mélliès and the interaction sequences of Coquand. We discuss how this theorem relates to normalization of linear head reduction in simply-typed lambda-calculus, leading us to a semantic realizability proof à la Kleene of our theorem. We then present another (...) proof of a more combinatorial nature. Finally, we discuss the exact class of strategies to which our theorems apply. (shrink)

Let $R$ be a convergent term rewriting system, and let $CR$-equality on combinatory logic terms be the equality induced by $\beta \eta R$-equality on terms of the lambda calculus under any of the standard translations between these two frameworks for higher-order reasoning. We generalize the classical notion of strong reduction to a reduction relation which generates $CR$-equality and whose irreducibles are exactly the translates of long $\beta R$-normal forms. The classical notion of strong normal form in combinatory (...) logic is also generalized, yielding yet another description of these translates. Their resulting tripartite characterization extends to the combined first-order algebraic and higher-order setting the classical combinatory logic descriptions of the translates of long $\beta$-normal forms in the lambda calculus. As a consequence, the translates of long $\beta R$-normal forms are easily seen to serve as canonical representatives for $CR$-equivalence classes of combinatory logic terms for non-empty, as well as for empty, $R$. (shrink)

Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after (...) generalizing maximally the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic. The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well. The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic. (shrink)

Girard and Reynolds independently invented System F to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates types with untyped lambda terms, raises the questions of typability and type checking. Typability asks for a term whether there exists some type it can be given. Type checking asks, for a particular term and type, whether the term can be given that type. The decidability of these problems has been settled for restrictions (...) and extensions of F and related systems and complexity lower-bounds have been determined for typability in F, but this report is the first to resolve whether these problems are decidable for System F. This report proves that type checking in F is undecidable, by a reduction from semi-unification, and that typability in F is undecidable, by a reduction from type checking. Because there is an easy reduction from typability to type checking, the two problems are equivalent. The reduction from type checking to typability uses a novel method of constructing lambda terms that simulate arbitrarily chosen type environments. All of the results also hold for the λI-calculus. (shrink)

We consider a deterministic rewrite system for combinatory logic over combinators , and . Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be "shared" rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda-expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are (...) considered equivalent if they represent the same lambda-expression (up to --equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the "fastest running" combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the "Hitting Set" problem. (shrink)

We present a new proof for the standardization theorem in $\lambda$-calculus, which is largely built upon a structural induction on $\lambda$-terms. We then extract some bounds for the number of $\beta$-reduction steps in the standard $\beta$-reduction sequence obtained from transforming a given $\beta$-reduction sequence, sharpening the standardization theorem. As an application, we establish a super exponential bound for the lengths of $\beta$-reduction sequences from any given simply typed $\lambda$-terms.

In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $lambda$-calculus, the 'call by value' in a context of a 'call by name'. J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of (...) this result to other types. (shrink)

In his influential paper ‘‘Essence and Modality’’, Kit Fine argues that no account of essence framed in terms of metaphysical necessity is possible, and that it is rather metaphysical necessity which is to be understood in terms of essence. On his account, the concept of essence is primitive, and for a proposition to be metaphysically necessary is for it to be true in virtue of the nature of all things. Fine also proposes a reduction of conceptual and logical necessity (...) in the same vein: a conceptual necessity is a proposition true in virtue of the nature of all concepts, and a logical necessity a proposition true in virtue of the nature of all logical concepts. I argue that the plausibility of Fine's view crucially requires that certain apparent explanatory links between essentialist facts be admitted and accounted for, and I make a suggestion about how this can be done. I then argue against the reductions of conceptual and logical necessity proposed by Fine and suggest alternative reductions, which remain nevertheless Finean in spirit. (shrink)

In this article we critically evaluate Robin Le Poidevin's recent attempt to set out an argument for the ontological reduction of chemistry independently of intertheoretic reduction. We argue, firstly, that the argument he envisages applies only to a small part of chemistry, and that there is no obvious way to extend it. We argue, secondly, that the argument cannot establish the reduction of chemistry, properly so called.

An effective theory in physics is one that is supposed to apply only at a given length scale; the framework of effective field theory describes a ‘tower’ of theories each applying at different length scales, where each ‘level’ up is a shorter-scale theory. Owing to subtlety regarding the use and necessity of EFTs, a conception of emergence defined in terms of reduction is irrelevant. I present a case for decoupling emergence and reduction in the philosophy of physics. This (...) paper develops a positive conception of emergence, based on the novelty and autonomy of the ‘levels’, by considering physical examples, involving critical phenomena, the renormalisation group, and symmetry breaking. This positive conception of emergence is related to underdetermination and universality, but, I argue, is preferable to other accounts of emergence in physics that rely on universality. (shrink)