Journal of Logic and Computation Advance Access published online on April 23, 2008
Journal of Logic and Computation, doi:10.1093/logcom/exn007
Original Papers |
The Expansion Problem in Lambda Calculi with Explicit Substitution
Department of Computer Science, University of Buenos Aires, Pabellón I - Ciudad Universitaria (1428) Buenos Aires, Argentina, E-mail: arbiser{at}dc.uba.ar
Received 30 January 2006.
| Abstract |
|---|
In this article, we address the problem of expansion with respect to rules of a calculus with explicit substitution. Mainly, we analyse the 
– and
s–calculi sets of terms having the property of expansion to pure terms, as minimal sets of terms for these calculi. We prove that, contrarily to what happens in the
x–calculus in which this set is trivial, for 
and
s they are proper and non-recursive, so a calculus based on a minimal set of terms has a syntax which is not context-free and hence cannot be presented in the usual way.
Keywords: Context-free; expansion; explicit substitution; lambda calculus; lambda s; lambda upsilon; recursiv set