Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\) (Q1322474): Difference between revisions

System \(F_ \leq\) is an extension of second order lambda calculus with a relation of subtyping (whose maximum element is the type Top) and a corresponding notion of (second order) bounded quantification. The typing judgements of \(F_ \leq\) have been studied by the authors in an earlier paper [Math. Struct. Comput. Sci. 2, No. 1, 55-91 (1992; Zbl 0765.03008)]. In the present paper they address the equality judgements of \(F_ \leq\). Since a term may have many types, equality between two terms is formulated relative to a type. An equality judgement has thus the form \(\Gamma\lvdash a= b: A\). Equality is defined as the standard \(\beta\eta\) conversion between terms, enriched with a collapsing rule as type Top: if \(\Gamma\lvdash a: A\), then \(\Gamma\lvdash a=\text{top}: \text{Top}\), where top is the canonical element of Top. Main goal (and result) of the paper is to show the decidability of this equality relation, or, more precisely, that, given \(\Gamma\), \(a\), \(b\), and \(A\) such that \(\Gamma\lvdash a: A\) and \(\Gamma\lvdash b: A\), the relation \(\Gamma\lvdash a= b: A\) is decidable. The problem is complex since \(F_ \leq\) combines several problematic features, like the terminal type Top, multiple derivations of the same typing judgement, and, especially, the undecidability of the typing relation [\textit{B. C. Pierce}, Inf. Comput. 112, No. 1, 131-165 (1994; Zbl 0794.03023)]. Even defining a correct notion of reduction in a typed context and with multiple types for a single term is a delicate subject, which the paper discusses in Section 1.3. The authors attack the problem exploiting the system with explicit coercions (\({\mathbf c}{\mathbf R}\)) defined in their earlier paper. By using this tool, they are able to define a confluent and weakly normalizing typed reduction system whose equational theory is equivalent to \(\beta\eta\text{ top}\). Decidability, however, does not follow yet, since the reduction is not effective -- a peculiar situation, indeed, of a decidable conversion whose corresponding reduction is not effective. Confluence and decidability are proved by the application of a ``transfer'' technique which the authors introduced in Lect. Notes Comput. Sci. 488, 215-225 (1991). First they observe that a certain reduction system \({\mathbf R}_ 1\) (defined on \(F_ 1\), the second order lambda calculus with a terminal type) is confluent. Then they define a translation from \({\mathbf c}{\mathbf R}\) to \({\mathbf R}_ 1\). Under suitable hypotheses (e.g., weak normalization of \({\mathbf c}{\mathbf R}\), proved in Section 2, and several properties of the translation, proved in Sections 3 and 4), one can now transfer the confluence of the original system \({\mathbf R}_ 1\) back to \({\mathbf c}{\mathbf R}\) and, finally, to the \(\beta\eta\text{ top}\) reduction (main proof in Section 5). Decidability is proved with an additional, and at this point not difficult, transfer argument. The authors succeed to clearly present the structure of the complex proof, discussing both the conceptual and the technical problems they had to cope with.