A Self-dependency Constraint in the Simply Typed Lambda Calculus

We consider terms of simply typed lambda calculus in which copy of a subterm may not be inserted to the argument of itself during the reduction. The terms form wide class which includes linear terms. We show that corresponding variant of the dual interpolation problem i.e. problem in which all expressions can be restricted to terms of this us the model for this kind of expressions can admit fully abstract semantics. Classification: semantics, logic in computer science.

• Type: Conference
• Year: 2005
• Where: FCT
• Authors: Aleksy Schubert
• Keywords: FCT 2005, Interpolation Problem I.e, Linear Terms, Simply Typed Lambda Calculus