Can LCF be topped? Flat lattice models of typed λ-calculus

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for , the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension _A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to .) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.     

Term Collections in λ and ρ-calculi

The ρ-calculus generalises term rewriting and the λ-calculus by defining abstractions on arbitrary patterns and by using a pattern-matching algorithm which is a parameter of the calculus. In particular, equational theories that do not have unique principal solutions may be used. In the latter case, all the principal solutions of a matching problem are stored in a “structure” that can also be seen as a collection of terms.Motivated by the fact that there are various approaches to the definition of structures in the ρ-calculus, we study in this paper a version of the λ-calculus with term collections.The contributions of this work include a new syntax and operational semantics for a λ-calculus with term collections, which is related to the λ-calculi with strict parallel functions studied by Boudol and Dezani et al. and a proof of the confluence of the β-reduction relation defined for the calculus (which is a suitable extension of the standard rule of β-reduction in the λ-calculus).     

A Symmetric Lambda Calculus for Classical Program Extraction

We introduce aλ-calculus with symmetric reduction rules and “classical” types, i.e., types corresponding to formulas of classical propositional logic. The strong normalization property is proved to hold for such a calculus, as well as for its extension to a system equivalent to Peano arithmetic. A theorem on the shape of terms in normal form is also proved, making it possible to get recursive functions out of proofs ofΠ⁰₂formulas, i.e., those corresponding to program specifications.     

Automated proofs of Löb's theorem and Gödel's two incompletensess theorems

The modal logic calculus K4, which represents important properties of the provability relation of Peano's Arithmetic, is formalized within the automated reasoning system ITP. Very high level automated proofs are then obtained of Löb's theorem, and of Gödel's two incompleteness theorems.     

Prehistoric Graph in Modal Derivations and Self-Referentiality

By terms-allowed-in-formulas capacity, Artemov’s Logic of Proofs LP Artemov includes self-referential formulas of the form t:?(t) that play a crucial role in the realization of modal logic S4 in LP, and in the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic via LP. In an earlier work appeared in the Proceedings of CSR 2010 the author defined prehistoric loop in a sequent calculus of S4, and verified its necessity to self-referentiality in S4?LP realization. In this extended version we generalize results there to T and K4, two modal logics smaller than S4 that yet call for self-referentiality in their realizations into corresponding justification logics JT and J4.     

Subtyping in Logical Form

By using intersection types and filter models we formulate a theory of types for a λ-calculus with record subtyping via a finitary programming logic. Types are interpreted as spaces of filters over a subset of the language of properties (the intersection types) which describes the underlying type free realizability structure. We show that such an interpretation is a PER semantics, proving that the quotient space arising from “logical” PERs taken with the intrinsic ordering is isomorphic to the filter semantics of types.     

On the Jacopini Technique

The general concern of the Jacopini technique is the question: “Is it consistent to extend a given lambda calculus with certain equations?” The technique was introduced by Jacopini in 1975 in his proof that in the untyped lambda calculusΩis easy, i.e.,Ωcan be assumed equal to any other (closed) term without violating the consistency of the lambda calculus. The presentations of the Jacopini technique that are known from the literature are difficult to understand and hard to generalise. In this paper we generalise the Jacopini technique for arbitrary lambda calculi. We introduce the concept ofproof-replaceabilityby which the structure of the technique is simplified considerably. We illustrate the simplicity and generality of our formulation of the technique with some examples. We apply the Jacopini technique to theλμ-calculus, and we prove a general theorem concerning the consistency of extensions of theλμ-calculus of a certain form. Many well known examples (e.g., the easiness ofΩ) are immediate consequences of this general theorem.     

On goal-directed provability in classical logic

One of the key features of logic programming is the notion of goal-directed provability. In intuitionistic logic, the notion of uniform proof has been used as a proof-theoretic characterization of this property. Whilst the connections between intuitionistic logic and computation are well known, there is no reason per se why a similar notion cannot be given in classical logic. In this paper we show that there are two notions of goal-directed proof in classical logic, both of which are suitably weaker than that for intuitionistic logic. We show the completeness of this class of proofs for certain fragments, which thus form logic programming languages. As there are more possible variations on the notion of goal-directed provability in classical logic, there is a greater diversity of classical logic programming languages than intuitionistic ones. In particular, we show how logic programs may contain disjunctions in this setting. This provides a proof-theoretic basis for disjunctive logic programs, as well as characterising the “disjunctive” nature of answer substitutions for such programs in terms of the provability properties of the classical connectives Λ and Λ.     

Classical Natural Deduction for S4 Modal Logic

This paper proposes a natural deduction system CNDS4 for classical S4 modal logic with necessity and possibility modalities. This new system is an extension of Parigot’s Classical Natural Deduction with dualcontext to formulate S4 modal logic. The modal λμ-calculus is also introduced as a computational extraction of CNDS4. It is an extension of both the λμ-calculus and the modal λ-calculus. Subject reduction, confluency, and strong normalization of the modal λμ-calculus are shown. Finally, the computational interpretation of the modal λμ-calculus, especially the computational meaning of the modal possibility operator, is discussed.     

Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus

We present a call-by-need λ-calculus λ_ND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ_≈, since the naïve bisimulation definition is useless. The main result is that bisimulation in λ_≈ is a congruence and coincides with the contextual equivalence. The proof is a non-trivial extension of Howe's method. This might be a step towards defining useful bisimulation relations and proving them to be congruences in calculi that extend the λ_ND-calculus.     

Completeness of Continuation Models for λμ-Calculus

We show that a certain simple call-by-name continuation semantics of Parigot's λ_μ-calculus is complete. More precisely, for every λ_μ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λ_μ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λ_μ-category in the sense of L. Ong (1996, in “Proceedings of LICS '96,” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation,” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λ_μ developed by C.-H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997,” Assoc. Comput. Mach. Press, New York).     

Descendants and Origins in Term Rewriting

In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first-order term rewriting and λ-calculus, their finitary as well as their infinitary variants. A recurrent theme is the parallel moves lemma. Next to the classical notion of descendant, we introduce an extended version, known as origin tracking. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the genericity lemma in λ-calculus, the theorem of Huet and Lévy on needed reductions in first-order term rewriting, and Berry's sequentiality theorem in (infinitary) λ-calculus.     

Interaction Nets vs. the ρ-calculus: Introducing Bigraphical Nets

The ρ-calculus generalises both term rewriting and the λ-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the λ-calculus, the prime example being the implementation of optimal β-reduction. It is thus natural to study interaction net encodings of the ρ-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the ρ-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets—a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.     

Developing (Meta)Theory of λ-calculus in the Theory of Contexts

We present a case study on the formal development of a non trivial (meta)theory in the Theory of Contexts using the Coq proof assistant. The methodology underlying the Theory of Contexts for reasoning on systems presented in HOAS is based on an axiomatic syntactic standpoint. We feel that one of the main advantages of this approach, is that it requires a very low logical overhead.The object system we focus on is the lazy, call-by-name λ-calculus (λ_cbn), both untyped and simply typed. We will see that the formal, fully detailed development of the theory of (λ_cbn) in the Theory of Contexts introduces a small, sustainable overhead with respect to the proofs “on the paper”. Moreover, this will allow for comparison with similar case studies developed in other approaches to the metatheoretical reasoning in higher-order abstract syntax.     

A Logic for Reasoning about Generic Judgments

This paper presents an extension of a proof system for encoding generic judgments, the logic FOλ^Δ of Miller and Tiu, with an induction principle. The logic FOλ^Δ is itself an extension of intuitionistic logic with fixed points and a “generic quantifier”, , which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλ^Δ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on , in particular by adding the axiom B≡x.B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.     

Perpetual Reductions inλ-Calculus

This paper surveys a part of the theory ofβ-reduction inλ-calculus which might aptly be calledperpetual reductions. The theory is concerned withperpetual reduction strategies, i.e., reduction strategies that compute infinite reduction paths fromλ-terms (when possible), and withperpetual redexes, i.e., redexes whose contraction inλ-terms preserves the possibility (when present) of infinite reduction paths. The survey not only recasts classical theorems in a unified setting, but also offers new results, proofs, and techniques, as well as a number of applications to problems inλ-calculus and type theory.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

Database Query Languages Embedded in the Typed Lambda Calculus

We investigate the expressive power of the typedλ-calculus when expressing computations over finite structures, i.e., databases. We show that the simply typedλ-calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs areλ-terms encoding databases, and a program expressing a query is aλ-term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME sequence of reduction steps. Under our database input-output conventions, all elementary queries are expressible in the typedλ-calculus and the PTIME queries are expressible in the order-5 (order-4) fragment of the typedλ-calculus (with equality).     

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification

We characterize provability in intuitionistic logic with equality in terms of a constraint calculus. This characterization uncovers close connections between provability in intuitionistic logic with equality and solutions to simultaneous rigid E-unification. We show that the problem of existence of a sequent proof with a given skeleton is polynomial-time equivalent to simultaneous rigid E-unifiability. This gives us a proof procedure for intuitionistic logic with equality modulo simultaneous rigid E-unification. We also show that simultaneous rigid E-unifiability is polynomial-time reducible to intuitionistic logic with equality. Thus, any proof procedure for intuitionistic logic with equality can be considered as a procedure for simultaneous rigid E-unifiability. In turn, any procedure for simultaneous rigid E-unifiability gives a procedure for establishing provability in intuitionistic logic with equality.