Why the usual candidates of reducibility do not work for the symmetric $\lambda\mu$-calculus

TL;DR

This paper investigates the limitations of traditional reducibility candidates in the symmetric $mbda ext{ extmu}$-calculus and establishes a standardization theorem for it.

Contribution

It demonstrates why standard reducibility techniques fail for the symmetric $mbda ext{ extmu}$-calculus and provides a standardization result for this calculus.

Findings

Usual reducibility candidates are ineffective for the symmetric $mbda ext{ extmu}$-calculus.

A standardization theorem is proven for the symmetric $mbda ext{ extmu}$-calculus.

Examples illustrate the failure of existing reducibility techniques.

Abstract

The symmetric $\lambda mu$-calculus is the $\lambda\mu$-calculus introduced by Parigot in which the reduction rule $\mu'$, which is the symmetric of $\mu$, is added. We give examples explaining why the technique using the usual candidates of reducibility does not work. We also prove a standardization theorem for this calculus.