Representing Nonterminating Rewriting with ${\mathbf{F}}_2^{\hat{I}}¼$

Abstract

We specify a second-order type system ${\mathbf{F}}_2^{\hat{I}}¼$ that is tailored for representing nonterminations. The nonterminating trace of a term $t$ in a rewrite system $\mathcal{R}$ corresponds to a productive inhabitant $e$ such that $\hat{I}{“}_{\mathcal{R}}⊢e:t$ in ${\mathbf{F}}_2^{\hat{I}}¼$, where $\hat{I}{“}_{\mathcal{R}}$ is the environment representing the rewrite system. We prove that the productivity checking in ${\mathbf{F}}_2^{\hat{I}}¼$ is decidable via a mapping to the $\hat{I}»$-Y calculus. We develop a type checking algorithm for ${\mathbf{F}}_2^{\hat{I}}¼$ based on second-order matching. We implement the type checking algorithm in a proof-of-concept type checker.