On the Role of Names in Reasoning about λ-tree Syntax Specifications

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).