When locally-named becomes nominal

Gyesik Lee, Hugo Herbelin, and SunYoung Kim

(Submitted to a special issue of JFP on dependently typed programming)

Introduction

This paper introduces a representation style of variable binding using dependent types. Our representation is a variation of the Coquand-McKinna-Pollack's locally-named representation. The main characteristic of our representation is the use of dependent families in defining expressions such as terms and formulas. We also showed some hidden utility of simultaneous substitution and simultaneous renaming. Consequently, we can deal with definitions and proofs in a more compact way, among which well-formedness, provability, soundness, and completeness. In order to confirm the feasibility of our idea we made several experiments using the proof assistant Coq which supports all the functionalities we need: intentional type theory, dependent types, inductive families, and simultaneous substitution. Moreover, we could reveal a new aspect of locally-named representation style that it can be regarded as a nominal approach under the condition that proofs-as-programs is not a part of the domain of the discourse.

Motivations

This work started with the observation that, in Frege's work such as Begriffsschrift and Basic Laws of Arithmetic, parameters(also called free variables) play essentially no role. And this drove us to check whether we could show the same meta-theoretic results even when we do not involve parameters to the language.
Another motivation was the observation that locally-named representation and locally nameless representation are both too permissive in defining raw terms. Some terms could not have meaning because they contain free occurrences of some local variables which are subject to be bound. It is a distinctive feature of (McKinna & Pollack 1999) that they introduced a way of avoiding appeal to such well-formedness considerations except in a very small number of places such as the definition of typing rules.
In order to remove the necessity of using extra syntax for well-formed terms at all, we use traces to control the information of local variables occurring in the construction of terms. Our idea is very close to that used in the typechecker example by (McBride & McKinna, 2004, Section 7) and the use in Agda of families indexed by Nat to represent well-scoped terms.
Finally, we were interested in the utility of simultaneous substitution. Although some people have already showed the importance of simultaneous substitution in formal reasoning about languages with binding, we believed that there were still some hidden properties about it. For example, there are cases where simultaneous substitution is not a choice, but a must. Moreover, simultaneous substitution can be used in saving infrastructure for a formal reasoning.

Papers

  1. When locally-named becomes nominal. Gyesik Lee, Hugo Herbelin and SunYoung Kim.
    Submitted to JFP special issue on dependently typed programming.
  2. Technical report. Gyesik Lee, Hugo Herbelin, and SunYoung Kim.
    A supplementary report on technical issues.

Library codes

  1. Trace-Based Locally-Named Representation
    1. LJT and Kripke Semantics Without Parameters:
    2. LJT and Kripke Semantics With Parameters:

  2. Coquand-McKinna-Pollak Style Locally-Named Representation
    1. LJT and Kripke Semantics Without Parameters:
    2. LJT and Kripke Semantics With Parameters:

  3. Locally Nameless Representation
    1. Soundness of Simply-typed Lambda Calculus:

Trace-based
Locally-Named Representation		 LJT and Kripke Semantics Without Parameters Source
LJT and Kripke Semantics With Parameters Source
Coquand-McKinna-Pollack's
Locally-named Representation		 LJT and Kripke Semantics Without Parameters Source
LJT and Kripke Semantics With Parameters Source
Locally Nameless
Representation		 Soundness of Simply-typed Lambda Calculus Source

The proof scripts can be compiled on Coq8.4.pl6. It should also work with previous versions such as 8.4 and 8.3.

Main References

  1. Coquand, Catarina. A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic Computation 15(1):57-90, 2002.
  2. Herbelin, Hugo and Lee, Gyesik. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Logic, Language, Information and Computation, 16th International Workshop, Wollic 2009, LNAI 5514:209-217, 2009.
  3. Leroy, Xavier. A locally nameless solution to the POPLmark challenge. Tecnical report, 6908 (INRIA), 2007.
  4. McBride, Conor and McKinna, James. The view from the left. Journal of functional programming, 14(1):69-111, 2004.
  5. McKinna, James and Pollack, Randy. Some lambda calculus and type theory formalized. Journal of Automated Reasoning 23(3-4):373-409, 1999.
  6. Stoughton, Allen. Substitution Revisited. Theoretical computer science, 59:317-325, 1988.

People