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
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:
Focusing in intuitionistic logic allows two polarities to be given to atomic propositions. If such propositions are assigned a negative polarity, then cut-free focused proofs correspond to head-normal form terms. If positive polarity is used instead, then focused proofs encode terms with sharing.
Focus proofs can easily allow for "multi-focusing" and there is strong evidence in recent papers that multi-focusing provides a good encoding of parallelism in proofs and terms.
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.
This stage can be broken down into the following intermediate goals.
Two other members of the Parsifal team, Kaustuv Chaudhuri and Beniamino Accattoli, will also be available for advising this internship.
The following bibliography is indicative of the kind of papers that will be part of this research effort.