Open Collections

Chan, Jonathan H.W.

University of British Columbia

Many contemporary proof assistants based on dependent type theories such as Coq and Agda are founded on the types-as-propositions paradigm where type checking a program corresponds to verifying a proof of some proposition in a higher-order predicate logic. To ensure decidability of type checking and consistency of the logic, these proof assistants forbid nonterminating recursive functions using guard predicates that only allow structurally recursive functions recurring on syntactically smaller arguments. However, these guard predicates are sometimes too restrictive and reject simple terminating functions that aren't otherwise structurally recursive. An alternative is to use type-based termination checking such as sized types, where inductively-defined types are annotated with sizes. Successful type checking guarantees that functions recur only on arguments whose types have smaller sizes, rather than merely on syntactic subarguments. Some existing models of sized dependent type theories support features for more expressive sized types, namely higher-rank size quantification (which allows for passing around size-preserving functions) and bounded size quantification (which eliminates the need for complex semi-continuity checks), but unfortunately none support both simultaneously. Meanwhile, the only implementation of sized types in a major proof assistant, Agda, does support these features, but is unfortunately logically inconsistent. In this thesis, I design a sized dependent type theory with higher-rank and bounded sizes (STT), and show that it's suitable for theorem proving by proving its consistency with a syntactic model: by compiling STT into the Extensional Calculus of Inductive Constructions (CICᴇ), a variant of Coq's core type theory, and showing that this translation is type preserving, the consistency of STT follows from the consistency of CICᴇ. This approach refutes the existence of an infinite size strictly greater than all sizes, which is present in prior sized type systems to overcome the limitations of finitary size expressions, meaning that some infinitary constructs unfortunately aren't definable in STT. Even so, STT provides a valid foundation for sized types in a proof assistant, opening the way for future work on recovering expressivity lost from the lack of an infinite size and on restricting sized types in Agda to be consistent.

Text

2022-07-27

Attribution 4.0 International

http://hdl.handle.net/2429/82209

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by/4.0/