Coq中高效精确实数算术的类型类

草稿：使用序数赋值形式化验证皮亚诺算术一致性的构造性证明

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments

本文通过序数赋值形式化验证皮亚诺算术一致性的构造性证明，并使用Coq定理证明器验证所有结果。

Tactics for Reasoning modulo AC in Coq

We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC; second, an OCaml plug-in for pattern matching modulo AC. We handle associative only operations, neutral elements, uninterpreted function symbols, and user-defined equivalence relations. By relying on type-classes for the reification phase, we can infer these properties automatically, so that end-users do not need to specify which operation is A or AC, or which …

Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic

Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point …

Church's thesis and related axioms in Coq's type theory

"Church's thesis" ($\mathsf{CT}$) as an axiom in constructive logic states that every total function of type $\mathbb{N} \to \mathbb{N}$ is computable, i.e. definable in a model of computation. $\mathsf{CT}$ is inconsistent in both classical mathematics and in Brouwer's intuitionism since it contradicts Weak König's Lemma and the fan theorem, respectively. Recently, $\mathsf{CT}$ was proved consistent for (univalent) constructive type theory. Since neither Weak König's Lemma nor the fan theorem are a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, i…

Computer-Assisted Verification of Four Interval Arithmetic Operators

Interval arithmetic libraries provide the four elementary arithmetic operators for operand intervals bounded by floating-point numbers. Actual implementations need to make a large case analysis that considers, e.g., magnitude relations between all pairs of argument bounds, positional relations between the arguments and zero, and handling of the special values, infinities and NaN. Their correctness is not obvious as they are implemented by human hands, which comes to be critical for the reliability. This work provides a mechanically-verified interval arithmetic library. For this purpose, we uti…

PAC Learning, VC Dimension, and the Arithmetic Hierarchy

We compute that the index set of PAC-learnable concept classes is $m$-complete $Σ^0_3$ within the set of indices for all concept classes of a reasonable form. All concept classes considered are computable enumerations of computable $Π^0_1$ classes, in a sense made precise here. This family of concept classes is sufficient to cover all standard examples, and also has the property that PAC learnability is equivalent to finite VC dimension.

Descriptive Complexity of $\#\textrm{AC}^0$ Functions

We introduce a new framework for a descriptive complexity approach to arithmetic computations. We define a hierarchy of classes based on the idea of counting assignments to free function variables in first-order formulae. We completely determine the inclusion structure and show that #P and #AC^0 appear as classes of this hierarchy. In this way, we unconditionally place #AC^0 properly in a strict hierarchy of arithmetic classes within #P. We compare our classes with a hierarchy within #P defined in a model-theoretic way by Saluja et al. We argue that our approach is better suited to study arith…

Type Classes for Mathematics in Type Theory

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to make practical a particularly flexible approach formerly thought infeasible. Thus, we address both traditional proof engineering challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which abstraction penalties inhibiting efficient computation are reduced t…

A Unified Formal Description of Arithmetic and Set Theoretical Data Types

We provide a "shared axiomatization" of natural numbers and hereditarily finite sets built around a polymorphic abstraction of bijective base-2 arithmetics. The "axiomatization" is described as a progressive refinement of Haskell type classes with examples of instances converging to an efficient implementation in terms of arbitrary length integers and bit operations. As an instance, we derive algorithms to perform arithmetic operations efficiently directly with hereditarily finite sets. The self-contained source code of the paper is available at http://logic.cse.unt.edu/tarau/research/2010/uni…

构造性类型论中Tennenbaum定理的分析

An Analysis of Tennenbaum's Theorem in Constructive Type Theory

本文在构造性类型论框架下重新分析并推广Tennenbaum定理，通过Church论题内部化可计算性论证，构造化多个经典证明并给出内在构造性表述，揭示经典视角下不可见的假设与结论差异，并完成Coq机械化。