On the role of names in reasoning about lambda-tree syntax specifications

Abstract

Lambda tree syntax (a variant of HOAS) and nominal techniques are two approaches to representing and reasoning about languages containing bindings. Although they are based on separate foundations, recent advances in the proof theory of generic judgments have shown that one may be able to incorporate some aspects of nominal techniques (i.e., the equivariant principle) to simplify reasoning about λ-tree syntax specifications, while still maintaining the crucial aspects of λ-tree syntax. In this paper, we present a logic, called LGnω, which incorporates a notion of generic judgments and equivariant reasoning. The logic LGnω is a simple extension of a logic called LGω by Tiu, and can be seen as a special case of the logic G by Gacek, Miller and Nadathur. A central idea of LGnω is the representation of a data type for names (represented by a predicate). Although the data type is inhabited by infinitely many elements, the judgments of the logic only ever use finitely many of them, and more importantly, validity of these judgments are preserved under arbitrary permutation of names, i.e., they are equivariant judgments. This finite support of judgments allows for tractable introduction rules of the name predicate. We illustrate with two examples how this simple extension can be used for reasoning about specifications involving bindings. In the first example, we show how one can represent the data type for λ-terms, and derive a structural induction principle for inductive reasoning over λ-terms. In the second example, we re-examine previous known encodings of open and late bisimulations for the π-calculus. We show that the difference between open and late bisimulation can be characterized by the choice of the encodings of names: the "untyped" version (for the former) versus the "typed" one (for the latter). Show more