About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One

TL;DR

This paper critically examines a claimed solution to a complex reasoning challenge in type theory, revealing that the purported simplification was due to reformulating the problem rather than solving it as originally posed.

Contribution

The paper refutes a previous claim of a simplified proof for a subtyping problem, clarifying that the solution involved altering the problem's formulation.

Findings

The claimed proof does not fully solve the original challenge.

The reformulation changes the nature of the problem rather than providing a genuine solution.

The original problem remains unresolved as claimed.

Abstract

The POPLMARK Challenge comprises a set of problems intended to measure the strength of reasoning systems in the realm of mechanizing programming language meta-theory at the time the challenge was enunciated. Included in the collection is the exercise of demonstrating transitivity of subtyping for a specific algorithmic formulation of subtyping for an extension of System F. The challenge represented by this problem derives from the fact that, for the given formulation, subtyping must be proved simultaneously with another property called narrowing. In a paper published as a proof pearl, Brigitte Pientka claimed to have presented a solution to the problem in which "the full power of parametric and higher-order judgments" is exploited to "get the narrowing lemma for free." We show this claim to be inaccurate. In particular, we show that the simplification is in substantial part the result of changing the formulation of the subtyping relation in a way that modifies the challenge rather than the outcome of the manner in which the argument is mechanized.