| Combining Algebraic Rewriting with the Second-Order Extensional Polymorphic Lambda Calculus (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| . We prove that strong normalisation and confluence properties are conserved when a left-linear canonical first-order algebraic rewriting system is combined with the second-order polymorphic -calculus with a restricted version of j-expansions. This strengthens many results in [4, 5, 8, 11]. We achieve this through an approach which simulates j-expansions with fi-reductions in the second-order polymorphic -calculus. This immediately yields a modular proof showing that the second-order extensional polymorphic -calculus is strongly normalising. Our work supports the adoption of j-expansions as rewrite rules in typed settings. 1 Introduction j-conversion presents an approach to studying extensional equalities for -terms. Given an j-equality x:M (x) = j M , where x has no free occurrences in M ; one can either say x:M (x) j-contracts (\Gamma! j ) to M , or M j-expands (\Gamma! j ) to x:M (x); the former is usually adopted as a rewrite rule since every -term can then be j-contracted t... | |||||||||||||||||
Details der Publikation | |||||||||||||||||
| |||||||||||||||||