Bar induction is compatible with constructive type theory

Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable

Research output: Contribution to journalArticlepeer-review

Abstract

Powerful yet effective induction principles play an important role in computing, being a paramount component of programming languages, automated reasoning, and program verification systems. The Bar Induction (BI) principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of transfinite induction. In this work, we investigate the compatibility of several variants of BI with Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We first show that CTT is compatible with a BI principle for sequences of numbers. Then, we establish the compatibility of CTT with a more general BI principle for sequences of name-free closed terms. The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding BI, such as the non-truncated version of BI on monotone bars being intuitionistically false. These enhancements are carried out formally using the Nuprl proof assistant that implements CTT and the formalization of CTT within the Coq proof assistant presented in previous works.
Original languageEnglish
Article numbera13
Pages (from-to)13:1-13:35
JournalJournal of the ACM
Volume66
Issue number2
DOIs
Publication statusPublished - 26 Apr 2019

Keywords

  • Bar induction
  • Constructive mathematics
  • Coq
  • Nuprl
  • Theory of computation
  • Type theory
  • W types
  • choice sequences
  • computational type theory
  • intuitionistic logic
  • semantics

Fingerprint

Dive into the research topics of 'Bar induction is compatible with constructive type theory'. Together they form a unique fingerprint.

Cite this