Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transport via Partial Galois Connections and Equivalences

Kevin Kappelmann

TL;DR

Transport via Partial Galois Connections and Equivalences presents a framework to transport programs across related representations in simple type theory by using partial Galois connections and dependent function relators. It generalises prior approaches based on type equivalences and partial quotient types, addressing inter-argument dependencies and transports to more general target types, including possibly infinite ones. The authors establish closure properties under (dependent) function relators, (co)datatypes, and composition, and formalise the theory in Isabelle/HOL with a prototype transport tool. By grounding transport in Galois-theoretic concepts and providing a mechanised, extensible foundation, the work enables automatic, sound reuse of libraries across representation boundaries, facilitating representation independence in formal verification. It also lays groundwork for future extensions to constructive logics and more sophisticated white-box transports, aiming to supersede existing lifting-based tools.

Abstract

Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype. This is the extended version of "Transport via Partial Galois Connections and Equivalences", 21st Asian Symposium on Programming Languages and Systems, 2023.

Transport via Partial Galois Connections and Equivalences

TL;DR

Transport via Partial Galois Connections and Equivalences presents a framework to transport programs across related representations in simple type theory by using partial Galois connections and dependent function relators. It generalises prior approaches based on type equivalences and partial quotient types, addressing inter-argument dependencies and transports to more general target types, including possibly infinite ones. The authors establish closure properties under (dependent) function relators, (co)datatypes, and composition, and formalise the theory in Isabelle/HOL with a prototype transport tool. By grounding transport in Galois-theoretic concepts and providing a mechanised, extensible foundation, the work enables automatic, sound reuse of libraries across representation boundaries, facilitating representation independence in formal verification. It also lays groundwork for future extensions to constructive logics and more sophisticated white-box transports, aiming to supersede existing lifting-based tools.

Abstract

Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype. This is the extended version of "Transport via Partial Galois Connections and Equivalences", 21st Asian Symposium on Programming Languages and Systems, 2023.
Paper Structure (27 sections, 8 theorems, 27 equations, 2 figures)

This paper contains 27 sections, 8 theorems, 27 equations, 2 figures.

Table of Contents

  1. Introduction
  2. A Simple Example
  3. State of the Art
  4. Limitations of the Lifting Package
  5. Contributions and Outline
  6. The Essence of Transport
  7. Type Equivalences
  8. Partial Quotient Types
  9. The Essence
  10. Other Motivations
  11. Partial Galois Connections, Equivalences, and Relators
  12. (Order) Basics
  13. Function Relators and Monotonicity
  14. Galois Relator
  15. Partial Galois Connections and Equivalences
  16. ...and 12 more sections

Key Result

lemma thmcounterlemma

For every partial quotient type $(T,l,r)$ with induced left relation $\inflerel{L}$, we have $T = \mathsf{Galois}\, \inflerel{L}\, (=)\, r$.

Figures (2)

  • Figure 1: Examples of equivalences used in prior work. Types are drawn solid, black. Transport functions are drawn dashed. Each equivalence gives rise to a number of equivalence classes on the left and right-hand side of the equivalence, which are drawn dotted. Arrows inside equivalence classes are omitted.
  • Figure 2: Examples of partial equivalences as defined in \ref{['eq:def_gal_conn']},\ref{['eq:def_gal_equiv']}. Types are drawn solid, black, transport functions dashed, and left and right relations dotted.

Theorems & Definitions (10)

  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • remark thmcounterremark
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • theorem thmcountertheorem