# Representing Nonterminating Rewriting with $\mathbf{F}_2^\mu$

## TL;DR

This paper introduces a second-order type system, $ extbf{F}_2^$, for representing and deciding nontermination in rewriting systems, with a focus on productivity and a practical type checker implementation.

## Contribution

The paper defines $ extbf{F}_2^$, proves decidability of productivity checking via a lambda-Y calculus mapping, and develops a type checker based on second-order matching.

## Key findings

- Productivity checking in $ extbf{F}_2^$ is decidable.
- A type checking algorithm for $ extbf{F}_2^$ is developed and implemented.
- The system effectively represents nonterminating rewrite traces.

## Abstract

We specify a second-order type system $\mathbf{F}_2^\mu$ 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 $\Gamma_{\mathcal{R}} \vdash e : t$ in $\mathbf{F}_2^\mu$, where $\Gamma_{\mathcal{R}}$ is the environment representing the rewrite system. We prove that the productivity checking in $\mathbf{F}_2^\mu$ is decidable via a mapping to the $\lambda$-Y calculus. We develop a type checking algorithm for $\mathbf{F}_2^\mu$ based on second-order matching. We implement the type checking algorithm in a proof-of-concept type checker.