Proof theory for term representations

Encadrement

Dale Miller, Partout team, Inria Saclay and LIX/Ecole Polytechnique

Description du sujet

Basic to the construction of any symbolic system is the structure terms, which are used to represent expressions, programs, formulas, types, etc. One way to define the structure of terms is as small proofs of their types. Such a view of terms provides a direct way to model substitutions as well bindings within terms. For example, a common representations of λ-terms uses the head normal form of terms where every (normal) term has the structure

(λ x1 ... λ xi. h t1 ... tj),

where h (the head of the term) is a variable or constant, t1, ..., tj are head normal terms (the arguments), and x1, ..., xi are variables bound in the body of this term (the binder). This structure for terms corresponds to particular cut-free proofs---variously called uniform proofs or LJT proofs---of implicational formulas viewed as types. Given that "terms are proofs", the encoding and dynamics of substitution can be addressed by using cut and cut-elimination.

One drawback of the head-normal form structure of λ-terms is that they do not have direct support for either sharing or parallel structure in terms. Direct support for sharing makes it possible to have much more compact encodings of some structures than is provided by the head normal form, which requires copying and recopying the same substructure. However, sharing appears to have its own problems: Can sharing in terms be enforced? Can sharing persist during substitutions and normalizations? Can sharing help or hinder operations on terms structures such as equality checking and unification?

Recent advances in proof theory related to focused proofs systems should have immediate application to these issues of term representation. Some of these recent advances include:

The purpose of this internship is to address some of these issues in term representation by making use of the recent results in focusing proof systems.

Roadmap

This stage can be broken down into the following intermediate goals.

  1. Develop notion for λ-terms in which sharing is different from cut. This should be based on positive biasing in LJF [LM09].
  2. Generalize this notion to account for both sharing and non-sharing term structures. This should be based on the full LJF proof system for implications.
  3. Describe equality and unification for first-order terms using these term representations. Starting points for this are the Peterson/Wegman [PW78] and Martelli/Montanari [MM82] unification algoritms.
  4. Repeat the previous point for the higher-order (simply typed λ-calculus). Huet's unification procedure [Hu72] is the starting point here.
  5. Finally, describe how cut-elimination in LJF can be used to describe the interaction between substitution, sharing, and explicit substitutions. The paper [AD14] is a good starting point for this task.

Two other members of the Parsifal team, Kaustuv Chaudhuri and Beniamino Accattoli, will also be available for advising this internship.

Bibliography

The following bibliography is indicative of the kind of papers that will be part of this research effort.

[AD14]
Beta Reduction is Invariant, Indeed by B. Accattoli and U. Dal Lago. CSL-LICS 2014.
[CHM13]
A multi-focused proof system isomorphic to expansion proofs by Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. Accepted to the J. of Logic and Computation: pdf.
[DL06]
LJQ: A Strongly Focused Calculus for Intuitionistic Logic by Roy Dyckhoff and Stéphane Lengrand. CiE 2006: 173-185: pdf.
[Hu72]
A Unification Algorithm for Typed λ-Calculus by Gérard Huet. Theoretical Computer Science, Vol 1 (1975), 27--57.
[LM09]
Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Theoretical Computer Science, 410(46), pp. 4747-4768 (2009): pdf.
[MM82]
An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari. ACM Trans. Program. Lang. Syst. 4 (2): 258-282 (1982).
[PW78]
Linear unification by Michael Stewart Paterson and M.N. Wegman. J. Comput. Syst. Sci. 16 (2): 158-167 (1978).
[S07]
Completing Herbelin's Programme by José Espírito Santo. TLCA 2007: 118-132: pdf.

Dale Miller