Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Weak Stratification for Logics of Definitions

Nathan Guermond

TL;DR

This paper extends the logic of definitions by introducing LD^{μ∇}, which combines weak stratification, nabla quantification, and inductive definitions. It establishes a ground version LD^{μ∇}_∞ and proves cut-elimination for this ground logic via a reducibility framework, thereby deriving the consistency of LD^{μ∇} through an interpretation into the ground system. The work shows that weak stratification can accommodate logical relations and nabla quantification without sacrificing consistency, while also identifying counterexamples that justify strict stratification for inductive definitions. Overall, it lays a foundation for extending the Abella proof assistant to support a broader class of definitions and inductive constructs. The results have implications for proof search and formalization of definitions in logics underlying programming language semantics.

Abstract

The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend on the predicate being defined. This leads to an apparent circularity which can be resolved by interpreting definitions as monotone fixed-point operators on terms, and which is enforced by imposing a stratification condition on definitions. In many instances, it is useful to consider definitions in which the predicate being defined appears negatively in the body of its definition. In the logic $\mathcal G$, underlying the Abella proof assistant, this is not allowed due to the stratification condition. One such application violating this condition is that of defining logical relations, which is a technique commonly used to prove properties about programming languages. Tiu has shown how to relax this stratification condition to allow for a broader body of definitions including that needed for logical relations. However, he only showed how to extend a core fragment of $\mathcal G$ with the weakened stratification condition, resulting in a logic he called $\mathrm{LD}$. In this work we show that the weakened stratification condition is also compatible with generic (nabla) quantification and general induction. The eventual aim of this work is to justify an extension of the Abella proof assistant allowing for such definitions.

Towards Weak Stratification for Logics of Definitions

TL;DR

This paper extends the logic of definitions by introducing LD^{μ∇}, which combines weak stratification, nabla quantification, and inductive definitions. It establishes a ground version LD^{μ∇}_∞ and proves cut-elimination for this ground logic via a reducibility framework, thereby deriving the consistency of LD^{μ∇} through an interpretation into the ground system. The work shows that weak stratification can accommodate logical relations and nabla quantification without sacrificing consistency, while also identifying counterexamples that justify strict stratification for inductive definitions. Overall, it lays a foundation for extending the Abella proof assistant to support a broader class of definitions and inductive constructs. The results have implications for proof search and formalization of definitions in logics underlying programming language semantics.

Abstract

The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend on the predicate being defined. This leads to an apparent circularity which can be resolved by interpreting definitions as monotone fixed-point operators on terms, and which is enforced by imposing a stratification condition on definitions. In many instances, it is useful to consider definitions in which the predicate being defined appears negatively in the body of its definition. In the logic , underlying the Abella proof assistant, this is not allowed due to the stratification condition. One such application violating this condition is that of defining logical relations, which is a technique commonly used to prove properties about programming languages. Tiu has shown how to relax this stratification condition to allow for a broader body of definitions including that needed for logical relations. However, he only showed how to extend a core fragment of with the weakened stratification condition, resulting in a logic he called . In this work we show that the weakened stratification condition is also compatible with generic (nabla) quantification and general induction. The eventual aim of this work is to justify an extension of the Abella proof assistant allowing for such definitions.
Paper Structure (51 sections, 21 theorems, 147 equations, 10 figures)

This paper contains 51 sections, 21 theorems, 147 equations, 10 figures.

Table of Contents

  1. Introduction
  2. The logic $\text{LD}^{\mu\nabla}$
  3. Syntax
  4. Logical rules
  5. Structural, axiom, and multicut rules
  6. Definitions and stratification
  7. The fixed-point and clausal form of definitions
  8. Inductive definitions
  9. The logic $\text{LD}^{\mu\nabla}$
  10. Examples
  11. Even numbers
  12. Logical equivalence
  13. Weak stratification is insufficient for inductive definitions
  14. The ground logic $\text{LD}^{\mu\nabla}_\infty$
  15. Interpreting $\text{LD}^{\mu\nabla}$ in $\text{LD}^{\mu\nabla}_\infty$
  16. ...and 36 more sections

Key Result

Lemma 1

For any permutation $\pi\in\mathrm{supp}(B)$, the following Init rule is derivable without cut:

Figures (10)

  • Figure 1: Definitions for $list$ and $append$
  • Figure 2: Logical equivalence in the simply typed lambda calculus
  • Figure 3: Core inference rules for $\text{LD}^{\mu\nabla}$
  • Figure 4: Structural, axiom, and multicut rules for $\text{LD}^{\mu\nabla}$
  • Figure 5: Definition rules for a predicate $p$, provided $A = p\ \vec{t}$
  • ...and 5 more figures

Theorems & Definitions (46)

  • Lemma 1
  • proof
  • Definition 1: The logic $\text{LD}^{\mu\nabla}$
  • Definition 2: The logic $\text{LD}^{\mu\nabla}_\infty$
  • Lemma 2: Grounding Lemma
  • proof
  • Lemma 3: Interpretation lemma
  • proof
  • Definition 3: normalizability
  • Definition 4: reducibility
  • ...and 36 more