PaperlayerView exact revision on arXiv

Source-linked AI summary

Logical Step-Indexed Logical Relations

Derek Dreyer, Amal Ahmed, Lars Birkedal

arXiv:1103.0510v2cs.PLcs.LO

TL;DR

Step-indexed logical relations can make proofs about program equivalence tedious and obscure through finite-index arithmetic. The paper introduces LSLR, a modal logic for recursively defined relations, and uses it to derive sound and complete reasoning principles for contextual approximation and equivalence without counting steps.

  • Problem

    Step-indexed logical-relation proofs can require tedious, error-prone finite-index reasoning that obscures their substance.

    Source: §1 · p. 2

  • Method

    The paper combines parametricity logic with a later modality to define recursive relations and encode a logical relation for call-by-value Fµ.

    Source: §1 · pp. 2–3

  • Results

    The resulting logical relation is sound and complete for contextual approximation, and derived rules support contextual-equivalence proofs without step-index arithmetic.

    Source: §1.1 · p. 3, §1 · p. 3

  • Takeaways & Limitations

    LSLR provides abstract equational and inequational reasoning principles for contextual approximation and equivalence without counting steps.

    Source: §1 · p. 3, §1.1 · p. 3

    Identity extension does not hold for the step-indexed model, although the paper demonstrates some free theorems despite this limitation.

    Source: §4.7 · p. 22

Abstract

from arXiv · show

Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal "later" operator from Appel, Melli\`es, Richards, and Vouillon's "very modal model" paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.

1. Introduction

Step-indexed relations support reasoning about recursive and other semantically interesting types, but proofs can become cluttered by finite-index arithmetic. LSLR combines parametricity logic with a later modality to derive sound and complete relational reasoning principles for contextual approximation without step-index arithmetic.

1. Introduction

  • Step-indexed proofs can require tedious, error-prone arithmetic that obscures their substance and may hinder wider acceptance.The difficulty arises because reasoning about infinite relatedness still requires reasoning at particular finite indices.Source: §1 · p. 2
  • LSLR synthesizes Plotkin and Abadi’s logic for parametricity with the very modal model’s later operator to support recursively defined relations.The later operator supports contractive recursive relations and is used with the Löb rule, which has an induction-on-worlds and coinductive flavor.Source: §1 · pp. 2–3
  • The paper encodes a logical relation for call-by-value Fµ that is sound and complete with respect to contextual approximation and supports both equational and inequational reasoning.Fµ has recursive and polymorphic types; the relation builds on Ahmed’s earlier step-indexed relation.Source: §1 · pp. 2–3

1.1. Overview.

  • Derived rules enable contextual-equivalence proofs using logical reasoning without step-index arithmetic, and the paper compares this approach with an Ahmed-style proof.The paper also reports improvements to, and a correction of a technical flaw in, its earlier LICS 2009 version.Source: §1.1 · p. 3

2. The Language Fµ

Fµ is a call-by-value language with impredicative polymorphism and iso-recursive types. The section gives its syntax and deterministic small-step semantics, then defines contextual approximation and equivalence through program contexts and termination.

2. The Language Fµ

  • Fµ is a call-by-value λ-calculus with impredicative polymorphism and iso-recursive types.Its syntax is presented in Figure 1.Source: §2 · p. 3, Figure 1 · p. 4
  • The dynamic semantics uses left-to-right call-by-value reduction and is deterministic.Figure 2 presents the small-step relation using evaluation contexts.Source: §2 · p. 4, Figure 2

2.1. Contextual Approximation and Equivalence.

  • Contextual approximation means every well-typed program context that terminates with one term also terminates with the other; equivalence is approximation in both directions.The context’s hole has the type of the compared terms.Source: §2.1 · p. 5

3. The Logic LSLR

LSLR is a second-order intuitionistic modal logic for term relations, including recursively defined relations. Its Kripke model and sound inference rules support reasoning about those relations without explicitly naming a step level in each judgment.

3.1. Syntax.

  • LSLR extends second-order intuitionistic logic with term relations and recursively defined relations, using the later operator to enforce contractiveness.A recursive relation is contractive when its recursive variable occurs only beneath later, so its interpretation depends on strictly future worlds.Source: §3 · p. 5, §3.1 · p. 6

3.2. A “Step-Indexed” Model of LSLR.

  • The Kripke model uses natural-number worlds, with smaller numbers as strictly future worlds, and interprets recursive relations by induction over worlds and relation size.The later modality at a world refers to strictly future worlds; contractiveness makes recursive expansion smaller for interpretation.Source: §3.2 · pp. 6–7
  • The logical judgment universally quantifies over worlds while interpreting hypotheses and conclusion in the same world, so proofs need not name a particular level.The model’s worlds are not themselves computational steps; their connection to computation is made later when defining the Fµ logical relation.Source: §3.2 · p. 8

3.3. Core Inference Rules.

  • The core rules include monotonicity and Löb induction over future worlds; the latter needs no base case because every proposition holds in world 0.The paper establishes sound rules for later, including distributivity over connectives under its monotonicity axiom.Source: §3.3 · pp. 8–9
  • LSLR is intended to formalize the relational reasoning portions of proofs, while first-order syntactic properties may be established separately in the meta-logic.The paper also notes that first-order propositions have a step-free interpretation in its model.Source: §3.3 · p. 9

4. A Syntactic Logical Relation for Fµ

This section develops a syntactic LSLR logical relation for Fµ and derives rules for reasoning about approximation and equivalence, including a symmetric relation for equational reasoning. It establishes connections with contextual and CIU approximation and presents results on recursive types and identity extension.

4.1. Roadmap and Preliminaries.

  • Contextual, ciu, and logical approximation coincide via the chain ⪯ctx ⊆ ⪯ciu ⊆ ⪯log ⊆ ⪯ctx.Ciu approximation uses evaluation contexts and explicit substitutions for closing open terms, and is easier to work with than contextual approximation.Source: §4.1 · p. 10

4.2. Atomic Relations.

  • The relation uses atomic propositions for typing, evaluation-context typing, reduction sequences, reductions with zero or one unroll-roll step, and ciu approximation.These propositions support syntactic value and term relations defined by induction on types under relational interpretations of free type variables.Source: §4.2 · p. 11, §4.3 · p. 12

4.3. Logical Relation.

  • Recursive types place the later modality only where needed, while term relatedness uses ciu approximation for completeness and a delayed unroll-roll case for compatibility.The logic imposes no admissibility requirement on candidate relations.Source: §4.3 · p. 13

4.4. Derivable Rules.

  • Derivable rules support reasoning about stuck terms with bind, compatibility with bind2, and clean function extensionality without mentioning later for functions.The weak-⊲ rule and Löb rule support inductive proofs that assume relatedness later and establish it now.Source: §4.4 · pp. 15–16

4.5. Proofs of Derivability.

  • The derivability proofs include a type-substitution result equating interpretations after substituting a type with interpretations under an extended relational assignment.The section states that it derives the rules shown in Figure 7.Source: §4.5 · p. 16
  • Derivability proofs establish value, weakening, reduction, and expansion rules, including a conditional expansion rule and a later-guarded expansion rule.The conditional rule requires an additional reduction premise.Source: §4.5 · pp. 16–17
  • The cited propositions report that both rule exp and rule ciu are derivable, supporting the main result that the expansion and CIU rules are derivable.Source: §4.5 · p. 17
  • The derivable compatibility rules include bind, bind2, application, unrolling, function extensionality, and fixpoint rules.Source: §4.5 · pp. 18–19

4.6. Soundness and Completeness of the Logical Relation.

  • The fundamental theorem gives logical reflexivity, and adequacy ensures that if the first term terminates, then the second does too.Source: §4.6 · p. 19
  • Logical approximation implies contextual approximation, CIU approximation implies logical approximation, and the three approximation relations are equivalent.Source: §4.6 · pp. 19–20

4.7. Symmetric Version of the Logical Relation.

  • Requiring asymmetric logical relatedness in both directions does not ensure the function behavior needed for a useful symmetric relation.Related functions must map value-related arguments to expression-related results, not merely equivalent arguments to equivalent results.Source: §4.7 · p. 20
  • The symmetric relation uses a Boolean whose unknown identity lets one proof establish logical approximation in both directions simultaneously.When the Boolean is true the relation uses the asymmetric relation in one direction; when false it uses the reverse direction.Source: §4.7 · p. 20
  • The recursive-type equivalence proof uses the Löb rule and splits on d: each case reduces to equivalent relation membership, by the basic axioms and inductive hypothesis.For d = true it uses V JτK with ρ; for d = false it uses V JτK with ρop and reversed arguments.Source: §4.7 · p. 21
  • Most derived rules, including compatibility properties, have symmetric counterparts using E≈ and V≈, with technical relations enabling symmetric premises for approximation directions.Several exceptions to the usual pattern are presented in Figure 9; the proofs rely on e1 ❀∗e2 implying e1 ≈ciu e2.Source: §4.7 · p. 21, Figure 9 · p. 22
  • Identity extension does not hold for the step-indexed model: contextual equivalence corresponds only to pairs related at every index, yet some free theorems remain provable.The paper demonstrates such free theorems in Section 5.3.Source: §4.7 · p. 22

5. Examples

The paper illustrates LSLR with three contextual-equivalence examples, presenting detailed proofs that do not mention step indices. The examples cover existentially typed flag objects, a recursive-type invariant, and a free theorem.

5. Examples

  • The proofs of three contextual-equivalence examples use LSLR’s derived rules without mentioning step indices.The examples are representation independence for existential recursive objects, a syntactic minimal invariant, and a Wadler-style free theorem.Source: §5 · pp. 22–23

5.1. Flag Objects.

  • Boolean- and integer-backed flag objects are proved equivalent by relating their hidden states so that true corresponds to 0 and subsequent flips preserve the relation.The objects expose a flag state and two methods; the proof uses a relation connecting Boolean values to integers of the corresponding parity.Source: §5.1 · p. 23

5.2. Syntactic Minimal Invariance.

  • For τ = µα. unit + (α →α), the identity function is shown equivalent to a recursive function, establishing the syntactic minimal invariant property.The proof uses Löb induction and the logical relation for the recursive type.Source: §5.2 · pp. 24–25

5.3. A “Free Theorem”.

  • For polymorphic h and f : τ →σ, h σ (f v) (f w) contextually approximates f (h τ v w) unconditionally; the reverse approximation holds when f is total.Totality is a sufficient, but not necessary, condition for the reverse direction.Source: §5.3 · p. 25

6. The Merits of Our Approach

The section contrasts Ahmed’s explicit step arithmetic with LSLR’s higher-level proof structure, then argues that selected LSLR principles can also improve direct step-indexed proofs.

6.1. Flag Objects Proof With Explicit Step Manipulation.

  • Ahmed’s flag-object proof tracks termination within n steps and adjusts relatedness indices, while LSLR lets the proof focus on substantive structure.The explicit proof follows evaluation and then relates resulting values at a reduced index; the LSLR proof avoids this step manipulation.Source: §6.1 · pp. 26–27, §6.2 · p. 27

6.2. What Have We Achieved?

  • Compatibility rules and sym-bind replace symbolic execution when the related terms share structure and differ in one place.Using these rules clarifies why the terms are equivalent.Source: §6.2 · pp. 27–28
  • A bind2 variant can improve direct step-indexed proofs, but it still explicitly quantifies over future worlds, unlike LSLR’s rule.The authors say it is less clear how to turn the symmetric rules into useful step-indexed rules.Source: §6.2 · p. 28

6. The Merits of Our Approach

  • The authors identify LSLR’s main contribution as step-free proof principles that better structure reasoning about step-indexed relations.At least some of those principles may also help structure direct proofs in the step-indexed model.Source: §6.2 · p. 28

7. Comparison With an Earlier Version of LSLR

The current LSLR version revises its logical apparatus, makes the logical relation complete for contextual approximation, and corrects unsound rules in the earlier version.

Atomic Typing and Value Predicates

  • The current logic treats typing and valuehood as ordinary atomic relations and makes relation types definable, a simpler and more general treatment.The earlier version built typing and valuehood into the logic and restricted relations to binary ones.Source: §7 · p. 28

Distinction Between Logic and Model

  • The current version conflates the logical judgment and its model interpretation, allowing later additions of inference rules when soundness is proved.The core rules are not complete; some arguments, such as adequacy, still require reasoning directly in the model.Source: §7 · pp. 28–29

Completeness of the Logical Relation

  • The current logical relation adds ciu-approximation to the case where the first term is already a value, enabling Ciu-Transitivity and completeness.The earlier relation, like Ahmed’s, was sound but not complete with respect to contextual approximation.Source: §7 · p. 29

Fixing a Technical Flaw

  • Three rules in the LICS version were unsound because their proofs mishandled the later operator’s world-1 case; none was critical.The sole rule used in the examples affected the syntactic minimal invariance proof, which now relies on canonical forms.Source: §7 · pp. 29–30
  • Rule ⊲∃1 fails for an uninhabited type because its premise can hold while its conclusion cannot; requiring an inhabited type restores soundness.The current version avoids this issue by not baking typing or value predicates into the variable context.Source: §7 · p. 29

8. Related Work and Conclusion

The authors position LSLR as an abstract way to reason about step-indexed relations, compare it with related logics and closure techniques, and identify limits and future directions.

Related Work and Conclusion

  • LSLR uses the later operator for binary contextual approximation and equivalence in a high-level language, unlike AMRV’s unary type-safety reasoning in a low-level language.The authors also emphasize language-specific inference rules and examples as part of their contribution.Source: §8 · p. 30
  • The IntSet equivalence does not seem provable directly in LSLR, though a transitive combination of equivalence proofs can establish it.Its recursive functions have structurally dissimilar calling patterns, and the proof needs inductive reasoning about computations on lists and trees.Source: §8 · pp. 30–31
  • Ciu-closure offers a simpler, more direct route to completeness in this setting, while ⊤⊤-closure applies more broadly but may rule out sym-bind.The authors say neither closure technique subsumes the other, and leave their tradeoffs for future study.Source: §8 · p. 31
  • LSLR aims to match the abstraction of non-step-indexed methods without claiming greater power, and uses Löb with sym-exp-⊲ for a stream-operations example.The authors note that step-indexed relations have been more adaptable to languages with effects, particularly state.Source: §8 · p. 32
  • The later operator’s use for binary reasoning distinguishes LSLR from AMRV; the authors describe LADR as a promising extension to general references.LADR enables abstract relational reasoning about a step-indexed model of Fµ with general references.Source: §8 · pp. 30, 32

Appendix A. Additional Details of Fµ

The appendix provides Fµ typing-context and program-context syntax, along with static-semantics material for expressions and contexts.

Appendix A. Additional Details of Fµ

  • Typing contexts are formed from the empty context by adding type variables or term variables annotated with types.Source: Appendix A · p. 34
  • Program contexts are defined by a grammar covering holes within expressions, conditionals, pairs, functions, type abstractions, packages, and recursive types.The grammar includes evaluation positions in constructs such as application, projection, case analysis, and unpacking.Source: Appendix A · p. 35
  • A context-typing judgment relates a context expecting Γ ⊢ τ to a result Γ′ ⊢ bool.Source: Appendix A · p. 35

Appendix B. Remaining Inference Rules for LSLR

The appendix lists remaining LSLR inference rules and well-formedness constraints for relations and substitutions.

Appendix B. Remaining Inference Rules for LSLR

  • The appendix presents LSLR judgments for relation and substitution well-formedness alongside additional standard inference rules.Prop is synonymous with Rel(0).Source: Appendix B · p. 36
  • A relation variable must match the relation’s arity, and a relation defined recursively in that variable must be contractive in it.Source: Appendix B · p. 36
  • Variable substitutions constrain their domain and require the free variables of substituted types and terms to lie in X.Source: Appendix B · p. 37
  • Relation substitutions require each substituted relation to have the variable’s arity and be well formed under X; R.Source: Appendix B · p. 37
Loading 1103.0510v2…