Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Experiments with Choice in Dependently-Typed Higher-Order Logic

Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk

TL;DR

This paper extends the DHOL term structure by Hilbert’s indefinite choice operator ε, defines a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and shows that the extension of the translation is complete and give an argument for soundness.

Abstract

Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator $ε$, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

Experiments with Choice in Dependently-Typed Higher-Order Logic

TL;DR

This paper extends the DHOL term structure by Hilbert’s indefinite choice operator ε, defines a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and shows that the extension of the translation is complete and give an argument for soundness.

Abstract

Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator , define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

Paper Structure

This paper contains 13 sections, 1 theorem, 9 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. DHOL
  4. Erasure
  5. Choice
  6. Completeness
  7. Proof of completeness for $\varepsilon_1$ and strong erasure
  8. Proof of completeness for $\varepsilon_2$ and weak erasure
  9. Soundness
  10. Experimental Problems and Results
  11. Results
  12. Conclusion
  13. Acknowledgements

Key Result

Theorem 1

For either variant --- DHOL$_{\varepsilon1}$ or DHOL$_{\varepsilon2}$ --- we retain that if $\Gamma \vdash^{\mathsf{d}} t:A$ then $\widetilde{\Gamma} \vdash^{\mathsf{s}} \widetilde{t}:\widetilde{A}$ and $\widetilde{\Gamma} \vdash^{\mathsf{s}} A^*~\widetilde{t}~\widetilde{t}$. Also, if $\Gamma \vdash

Figures (5)

  • Figure 1: HOL Syntax
  • Figure 2: DHOL Syntax (changes are highlighted)
  • Figure 3: Choice Rules for DHOL${_{\varepsilon1}}$
  • Figure 4: Choice Rules for DHOL${_{\varepsilon2}}$
  • Figure 5: Choice Rules for HOL$_\varepsilon$

Theorems & Definitions (1)

  • Theorem