Logics of definitions extend first order intuitionistic logic with fixed-point definitions which associate formulas to atomic predicates. These associated formulas must be constrained for consistency. In the original formulation, predicate symbols were required to be ordered and only predicates lower in the order were allowed to appear negatively in the defining formula. This constraint renders ineligible definitions such as those of logical relations in which the predicate being defined must be allowed to appear negatively, albeit with smaller arguments. Tiu has formalized a weaker constraint called ground stratification that permits such definitions and has shown that it suffices for consistency. Definitions can also be given a least fixed-point interpretation via a special induction rule. We address the question of whether Tiu’s relaxation carries over to such a treatment. We propose a new induction rule for ground stratified inductive definitions that takes into account the fact that the definition of the predicate in question must itself be considered to be stratified by the complexity of its arguments to obtain a least fixed-point interpretation. We establish the consistency of the resulting logic and we illustrate its new capabilities via an example that encodes a strong normalizability proof for the simply typed λ-calculus in which the reducibility predicate is inductively defined by recursion on its arguments.

This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In this context, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of modular metatheory , by which we mean that proofs of relevant properties should be constructible by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called Sterling and a proof assistant called Extensibella and have used them to validate the examples that motivate the theoretical discussions.

A logic is presented for formalizing properties of specifications in the Edinburgh Logical Framework or LF. In this logic, typing judgments in LF serve as atomic formulas and quantification is permitted over LF terms and contexts. Quantifiers of the first variety are qualified by simple types that describe the functional structure associated with the variables they bind. Quantifiers over contexts are typed by context schemas that constrain their instantiations to adhere to a regular structure. The semantics of the logic is based ultimately on an understanding of derivability in LF. As such, valid formulas in the logic represent meta-theoretic properties of object systems that are encoded via LF signatures. The logic is complemented by a proof system that is briefly discussed. There are two categories to the rules in this proof system. One collection of rules captures the meanings of logical connectives and quantifiers. Another collection provides a means for analyzing atomic formulas based on an understanding of derivability in LF; these rules build in the capability for a case-analysis style reasoning about LF judgements and for induction over the heights of LF derivations.

The genesis of this special issue was in a meeting that took place at Université Paris Diderot on December 15 and 16, 2016. Dale Miller, Professor at École polytechnique, had turned 60 a few days earlier. In a career spanning over three decades and in work conducted in collaboration with several students and colleagues, Dale had had a significant influence in an area that can be described as structural proof theory and its application to computation and reasoning. In recognition of this fact, several of his collaborators thought it appropriate to celebrate the occasion by organizing a symposium on topics broadly connected to his areas of interest and achievements. The meeting was a success in several senses: it was attended by over 35 people, there were 15 technical presentations describing new results, and, quite gratifyingly, we managed to spring the event as a complete surprise to Dale.

The Abella interactive theorem prover has turned out to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism with respect to the logic that Abella is based on as well as the executable specification logic that it embeds.

The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems that are commonly presented via syntax-directed rules that make use of contexts and side-conditions. The two-level logic approach, as implemented in the Abella theorem prover, embeds the HH specification logic within a rich reasoning logic that supports inductive and co-inductive definitions, an equality predicate, and generic quantification. Properties of the encoded systems can then be proved through the embedding, with special benefit being extracted from the transparent correspondence between HH derivations and those in the encoded formal systems. The versatility of HH relies on the free use of nested implications, leading to dynamically changing assumption sets in derivations. Realizing an induction principle in this situation is nontrivial and the original Abella system uses only a subset of HH for this reason. We develop a method here for supporting inductive reasoning over all of HH. Our approach relies on the ability to characterize dynamically changing contexts through finite inductive definitions, and on a modified encoding of backchaining for HH that allows these finite characterizations to be used in inductive arguments. We demonstrate the effectiveness of our approach through examples of formal reasoning on specifications with nested implications in an extended version of Abella.

Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. Specifically, we describe a natural deduction calculus that adds a form of "closed-world'' equality - a key ingredient to supporting fixed-point definitions - to deduction modulo, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. Our integration of closed-world equality into deduction modulo is based on an elimination principle for this form of equality that, for the first time, allows us to require finiteness of proofs without sacrificing stability under reduction.

Dependently typed λ-calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the Twelf system is based on such an interpretation of LF. We consider here whether a conventional logic programming language can provide the benefits of a Twelf-like system for encoding type and proof-and-formula dependencies. In particular, we present a simple mapping from LF specifications to a set of formulas in the higher-order hereditary Harrop (hohh) language, that relates derivations and proof-search between the two frameworks. We then show that this encoding can be improved by exploiting knowledge of the well-formedness of the original LF specifications to elide much redundant type-checking information. The resulting logic program has a structure that closely resembles the original specification, thereby allowing LF specifications to be viewed as hohh meta-programs. Using the Teyjus implementation of λ Prolog, we show that our translation provides an efficient means for executing LF specifications, complementing the ability that the Twelf system provides for reasoning about them.

Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that allow direct, logic-based reasoning about such descriptions: the treatment of atomic judgments as fixed points (recursive definitions) and an encoding of binding constructs via generic judgments. However, the logics encompassing these two features have thus far treated them orthogonally: that is, they do not provide the ability to define object-logic properties that themselves depend on an intrinsic treatment of binding. We propose a new and simple integration of these features within an intuitionistic logic enhanced with induction over natural numbers and we show that the resulting logic is consistent. The pivotal benefit of the integration is that it allows recursive definitions to not just encode simple, traditional forms of atomic judgments but also to capture generic properties pertaining to such judgments. The usefulness of this logic is illustrated by showing how it can provide elegant treatments of object-logic contexts that appear in proofs involving typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.

The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problems. One issue concerns the machine representation of lambda terms suitable to their intended use: an adequate encoding must facilitate comparison operations over terms in addition to supporting the usual reduction computation. Another aspect relates to the treatment of a unification operation that has a branching character and that sometimes calls for the delaying of the solution of unification problems. A final issue concerns the execution of goals whose structures become apparent only in the course of computation. These various problems are exposed in this paper and solutions to them are described. A satisfactory representation for lambda terms is developed by exploiting the nameless notation of de Bruijn as well as explicit encodings of substitutions. Special mechanisms are molded into the structure of traditional Prolog implementations to support branching in unification and carrying of unification problems over other computation steps; a premium is placed in this context on exploiting determinism and on emulating usual first-order behaviour. An extended compilation model is presented that treats higher-order unification and also handles dynamically emergent goals. The ideas described here have been employed in the Teyjus implementation of the $\lambda$ Prolog language, a fact that is used to obtain a preliminary assessment of their efficacy.

Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions are realized incrementally through the use of environments. However, environments are usually not accorded a first-class status within such systems in that they are not reflected into term structure. This approach does not allow the smaller substitution steps to be intermingled with other operations of interest on lambda terms. Various new notations for lambda terms remedy this situation by proposing an explicit treatment of substitutions. Unfortunately, a naive implementation of beta reduction based on such notations has the potential of being costly: each use of the substitution propagation rules causes the creation of a new structure on the heap that is often discarded in the immediately following step. There is, thus, a tradeoff between these two approaches. This paper discusses these tradeoffs and offers an amalgamated approach that utilizes recursion in rewrite rule application but also suspends substitution operations where profitable.

Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We investigate the relevance of this uniform proofnotion to structuring proof search in classical logic. A logical language in whose context provability is equivalent to uniform provability admits of a goal-directed proof procedure that interprets logical symbols as search directives whose meanings are given by the corresponding inference rules. While this uniform provability property does not hold directly of classical logic, we show that it holds of a fragment of it that only excludes essentially positive occurrences of universal quantifiers under a modest, sound, modification to the set of assumptions: the addition to them of the negation of the formula being proved. We further note that all uses of the added formula can be factored into certain derived rules. The resulting proof system and the uniform provability property that holds of it are used to outline a proof procedure for classical logic. An interesting aspect of this proof procedure is that it incorporates within it previously proposed mechanisms for dealing with disjunctive information in assumptions and for handling hypotheticals. Our analysis sheds light on the relationship between these mechanisms and the notion of uniform proofs.

One formulation of the concept of logic programming is the notion of an abstract logic programming language. Central to its definition is a uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the duality of readings, both declarative and procedural. We use this technology to investigate disjunctive logic programming (DLP), an extension of traditional logic programming that permits disjunctive program clauses. This extension has been considered by some to be inappropriately identified with logic programming because the indefinite reasoning introduced by disjunction violates the goal-oriented search directionality that is central to logic programming. We overcome this criticism by showing that the requirement of uniform provability can be realized in a logic which is more general than that of DLP under a modest, sound modification of programs. We use this observation to derive inference rules that capture the essential proof structure of InH-Prolog (Inheritance Near-Horn Prolog), a known proof procedure for DLP.

Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 (1991) 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed.

A generalization of Horn clauses to a higher-order logic is described and examined as a basis for logic programming. In qualitative terms, these higher-order Horn clauses are obtained from the first-order ones by replacing first-order terms with simply typed λ-terms and by permitting quantification over all occurrences of function symbols and some occurrences of predicate symbols. Several proof-theoretic results concerning these extended clauses are presented. One result shows that although the substitutions for predicate variables can be quite complex in general, the substitutions necessary in the context of higher-order Horn clauses are tightly constrained. This observation is used to show that these higher-order formulas can specify computations in a fashion similar to first-order Horn clauses. A complete theorem-proving procedure is also described for the extension. This procedure is obtained by interweaving higher-order unification with backchaining and goal reductions, and constitutes a higher-order generalization of SLD-resolution. These results have a practical realization in the higher-order logic programming language called λProlog.

Consideration of the question of meaning in the framework of linguistics often requires an allusion to sets and other higher-order notions. The traditional approach to representing and reasoning about meaning in a computational setting has been to use knowledge representation systems that are either based on first-order logic or that use mechanisms whose formal justifications are to be provided after the fact. In this paper we shall consider the use of a higher-order logic for this task. We first present a version of definite clauses (positive Horn clauses) that is based on this logic. Predicate and function variables may occur in such clauses and the terms in the language are the typed λ-terms. Such term structures have a richness that may be exploited in representing meanings. We also describe a higher-order logic programming language, called λProlog, which represents programs as higher-order definite clauses and interprets them using a depth-first interpreter. A virtue of this language is that it is possible to write programs in it that integrate syntactic and semantic analyses into one computational paradigm. This is to be contrasted with the more common practice of using two entirely different computation paradigms, such as DCGs or ATNs for parsing and frames or semantic nets for semantic processing. We illustrate such an integration in this language by considering a simple example, and we claim that its use makes the task of providing formal justifications for the computations specified much more direct.