Primitive recursion for higher-order abstract syntax. (English) Zbl 1063.03511
de Groote, Philippe (ed.) et al., Typed lambda calculi and applications. Third international conference on typed lambda calculi and applications, TLCA ’97, Nancy, France, April 2–4, 1997. Proceedings. Berlin: Springer (ISBN 3-540-62688-3/pbk). Lecture Notes in Computer Science 1210, 147-163 (1997).
Introduction: Higher-order abstract syntax is a central representation technique in many logical frameworks, that is, meta-languages designed for the formalization of deductive systems. The basic idea is to represent variables of the object language by variables in the meta-language. Consequently, object language constructs which bind variables must be represented by meta-language constructs which bind the corresponding variables.
This deceptively simple idea, which goes back to Church and Martin-Löf’s system of arities, has far-reaching consequences for the methodology of logical frameworks. On one hand, encodings of logical systems using this idea are often extremely concise and elegant, since common concepts and operations such as variable binding, variable renaming, capture-avoiding substitution, or parametric and hypothetical judgments are directiy supported by the framework and do not need to be encoded separately in each application. On the other hand, higher-order representations are no longer inductive in the usual sense, which means that standard techniques for reasoning by induction do not apply.
Various attempts have been made to preserve the advantages of higher-order abstract syntax in a setting with strong induction principles, but none of these is entirely satisfactory from a practical or theoretical point of view.
In this paper we take a first step towards reconciling higher-order abstract syntax with induction by proposing a system of primitive recursive functionals that permits iteration over subjects of functional type. In order to avoid the well-known paradoxes which arise in this setting, we decompose the primitive recursive function space \(A\Rightarrow B\) into a modal operator and a parametric function space \((\square A)\to B\). The inspiration comes from linear logic which arises from a similar decomposition of the intuitionistic function space \(A\supset B\) into a modal operator and a linear function space \((!A)-\!\!\circ\, B\).
The resulting system allows, for example, iteration over the structure of expressions from the untyped \(\lambda\)-calculus when represented using higher-order abstract syntax. It is general enough to permit iteration over objects of any simple type, constructed over any simply typed signature and thereby encompasses Gödel’s system \(T\). Moreover, it is conservative over the simply-typed \(\lambda\)-calculus which means that the compositional adequacy of encodings in higher-order abstract syntax is preserved. We view our calculus as an important first step towards a system which allows the methodology of logical frameworks such as LF to be incorporated into systems such as Coq or ALF.
The remainder of this paper is organized as follows: Section 2 reviews the idea of higher order abstract syntax and introduces the simply typed \(\lambda\)-calculus \((\lambda^\to)\) which we extend to a modal \(\lambda\)-calculus in Section 3. Section 4 then presents the concept of iteration. In Section 5 we sketch the proof of our central result, namely that our extension is conservative over \(\lambda^\to\). Finally, Section 6 assesses the results, compares some related work, and outlines future work.
See also the full paper in Theor. Comput. Sci. 266, 1–57 (2001; Zbl 0994.68028).
For the entire collection see [Zbl 1045.03501].
This deceptively simple idea, which goes back to Church and Martin-Löf’s system of arities, has far-reaching consequences for the methodology of logical frameworks. On one hand, encodings of logical systems using this idea are often extremely concise and elegant, since common concepts and operations such as variable binding, variable renaming, capture-avoiding substitution, or parametric and hypothetical judgments are directiy supported by the framework and do not need to be encoded separately in each application. On the other hand, higher-order representations are no longer inductive in the usual sense, which means that standard techniques for reasoning by induction do not apply.
Various attempts have been made to preserve the advantages of higher-order abstract syntax in a setting with strong induction principles, but none of these is entirely satisfactory from a practical or theoretical point of view.
In this paper we take a first step towards reconciling higher-order abstract syntax with induction by proposing a system of primitive recursive functionals that permits iteration over subjects of functional type. In order to avoid the well-known paradoxes which arise in this setting, we decompose the primitive recursive function space \(A\Rightarrow B\) into a modal operator and a parametric function space \((\square A)\to B\). The inspiration comes from linear logic which arises from a similar decomposition of the intuitionistic function space \(A\supset B\) into a modal operator and a linear function space \((!A)-\!\!\circ\, B\).
The resulting system allows, for example, iteration over the structure of expressions from the untyped \(\lambda\)-calculus when represented using higher-order abstract syntax. It is general enough to permit iteration over objects of any simple type, constructed over any simply typed signature and thereby encompasses Gödel’s system \(T\). Moreover, it is conservative over the simply-typed \(\lambda\)-calculus which means that the compositional adequacy of encodings in higher-order abstract syntax is preserved. We view our calculus as an important first step towards a system which allows the methodology of logical frameworks such as LF to be incorporated into systems such as Coq or ALF.
The remainder of this paper is organized as follows: Section 2 reviews the idea of higher order abstract syntax and introduces the simply typed \(\lambda\)-calculus \((\lambda^\to)\) which we extend to a modal \(\lambda\)-calculus in Section 3. Section 4 then presents the concept of iteration. In Section 5 we sketch the proof of our central result, namely that our extension is conservative over \(\lambda^\to\). Finally, Section 6 assesses the results, compares some related work, and outlines future work.
See also the full paper in Theor. Comput. Sci. 266, 1–57 (2001; Zbl 0994.68028).
For the entire collection see [Zbl 1045.03501].
MSC:
| 03B40 | Combinatory logic and lambda calculus |
| 68N18 | Functional programming and lambda calculus |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
