Encoding Monomorphic and Polymorphic Types

TL;DR

This paper systematically analyzes and improves encoding schemes for translating typed logics into untyped first-order logic, extending to polymorphism, and implements these in Isabelle/HOL with significant performance gains.

Contribution

It introduces novel, efficient encoding schemes for monomorphic and polymorphic types using monotonicity and the concept of 'cover', with formal proofs and practical implementation.

Findings

New encodings outperform previous schemes in efficiency

Formal proofs of soundness and correctness provided

Implementations in Isabelle/HOL demonstrate practical benefits

Abstract

Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.