Towards Weak Stratification for Logics of Definitions

TL;DR

This paper explores relaxing the stratification condition in logics of definitions, enabling broader definitions such as those used in logical relations, and aims to extend the Abella proof assistant accordingly.

Contribution

It demonstrates that weakened stratification is compatible with generic quantification and induction, broadening the applicability of the logic of definitions.

Findings

Weakened stratification condition supports more expressive definitions.

Compatibility with generic (nabla) quantification is established.

Extension of Abella proof assistant is justified for these definitions.

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.