Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ground Stratification for a Logic of Definitions with Induction

Nathan Guermond, Gopalan Nadathur

TL;DR

The results are a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.

Abstract

The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the logic includes a strict stratification condition on definitions that is too restrictive for some applications such as those that use a logical relations based approach to semantic equivalence. Tiu has shown how this restriction can be eased by utilizing a weaker notion referred to as ground stratification. Tiu's results were limited to a version of the logic that does not treat inductive definitions. We show here that they can be extended to cover such definitions. While our results are obtained by using techniques that have been previously deployed in related ways in this context, their use is sensitive to the particular way in which we generalize the logic. In particular, although ground stratification may be used with arbitrary fixed-point definitions, we show that weakening stratification to this form for inductive definitions leads to inconsistency. The particular generalization we describe accords well with the way logical relations are used in practice. Our results are also a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.

Ground Stratification for a Logic of Definitions with Induction

TL;DR

The results are a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.

Abstract

The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the logic includes a strict stratification condition on definitions that is too restrictive for some applications such as those that use a logical relations based approach to semantic equivalence. Tiu has shown how this restriction can be eased by utilizing a weaker notion referred to as ground stratification. Tiu's results were limited to a version of the logic that does not treat inductive definitions. We show here that they can be extended to cover such definitions. While our results are obtained by using techniques that have been previously deployed in related ways in this context, their use is sensitive to the particular way in which we generalize the logic. In particular, although ground stratification may be used with arbitrary fixed-point definitions, we show that weakening stratification to this form for inductive definitions leads to inconsistency. The particular generalization we describe accords well with the way logical relations are used in practice. Our results are also a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.
Paper Structure (15 sections, 10 theorems, 22 equations, 7 figures)

This paper contains 15 sections, 10 theorems, 22 equations, 7 figures.

Table of Contents

  1. Introduction
  2. A Logic with Definitions and Induction
  3. Syntax
  4. Logical Rules
  5. Treating Predicate Constants as Defined Symbols
  6. Inductive Definitions and Fixed-Point Operators
  7. Stratification and Consistency
  8. Applications for the More Permissive Form for Definitions
  9. Proving Consistency for the Logic
  10. The Ground Logic
  11. Consistency of the Ground Logic
  12. Cut reductions
  13. Cut Elimination
  14. Consistency of the Full Logic
  15. Conclusion

Key Result

Lemma 1

Suppose $p\ \vec{x}\stackrel{\mathclap{\hbox{$\mu$}}}{=} B\ p\ \vec{x}$ is the fixed-point form of an inductive definition, then for any derivation $\Psi$ of $\Delta\vdash D\ p$ where $p$ does not occur in $D$ and occurs only positively in $D\ p$ ( i.e., does not occur to the left of an implication)

Figures (7)

  • Figure 1: Logical rules for quantifiers
  • Figure 2: The multicut and axiom rules
  • Figure 3: Definition rules for a predicate $p$, provided $A = p\ \vec{t}$
  • Figure 4: Rules for introducing $p\ \vec{t}$ after converting the clauses for $p$ into the form $p\ \vec{x} \stackrel{\mathclap{\hbox{$\mu$}}}{=}_{\vec{x}} B\ p\ \vec{x}$
  • Figure 5: $\forall\mathcal{R}$ and $\exists\mathcal{L}$ rules in $\text{LD}^{\mu}_\infty$
  • ...and 2 more figures

Theorems & Definitions (16)

  • Lemma 1: Unfolding lemma
  • Definition 1: normalizability
  • Definition 2: reducibility
  • Lemma 2: Normalization Lemma
  • Lemma 3: Reducibility Lemma
  • Corollary 1
  • proof
  • Lemma 4: Normal form lemma
  • Theorem 1: Cut admissibility for $\text{LD}^{\mu}_\infty$
  • Corollary 2: Consistency of $\text{LD}^{\mu}_\infty$
  • ...and 6 more