A positive perspective on term representation: Extended paper

We use the focused proof system LJF as a framework for describing term structures and substitution.Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise.When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion.In this situation, cut elimination also yields the familiar notion of substitution.On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible.Such a representation of terms provides an explicit method for sharing term structures.In this setting, cut elimination yields a different notion of substitution.We illustrate these two approaches to term representation by applying them to the encoding of untyped -terms.We also exploit concurrency theory techniques-namely traces and simulation-to compare untyped -terms using such different structuring disciplines.