Efficient proofs

Henk Barendregt Nijmegen University

The Netherlands —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Presenting Computer Mathematics: Citations

• Borwein: “Your obligations are high” (to developers of mathematical software) “The 4CT has a non-traditional standard of rigor”

• Greuel: “I only trust a machine that I built myself” “Be aware of selling our soul to the devil of algebra [computing]”

• Joswig: “ ... it is often hard to verify whether a computer proof is correct or not”

• Cohen: “All computational tasks (in number fields) are finished”

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Presenting Computer Mathematics: The Babylonian vs Greek tradition

Babylonian: computing Greek: proving

It took until the 19-th century until the two traditions fully came together

20-th century: a temporary separation

• Computer algebra: Babylonian

• Formalization of proofs: Greek

21-st century: synthesis is emerging

Computer Mathematics —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Presenting Computer Mathematics: mathematical activity

Mathematical activity: defining, computing, proving Mathematical assistant helps human user:

Representing arbitrary mathematical notions  (defining)
Manipulating these  (computing)
Proving results about them  (proving)

in an impeccable way Eventually to assist humans to learn and develop mathematics At present an interesting foundational problem —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Presenting Computer Mathematics: computable vs non-computable objects

• Representing “computable” objects \sqrt{2} becomes a symbol α α^{2} − 2 becomes 0 α + 1 cannot be simplified

• Representing “non-computable” objects Hilbert space H, again just a symbol P (H) := “H is locally compact” is not decidable But ⊢ p :^{1} P (H) is decidable (^{1}p is a proof of P (H))

But then we need formalized proofs —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Presenting Computer Mathematics: the axiomatic-deductive method

Aristotle

• The axiomatic method

objects  properties
primitive axioms
defined  derived
defining proving

computing

• The quest for logic try to chart reasoning

• Poof-checking vs theorem proving —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Ontology

Ontology (what objects do there exist?) Classical mathematics (before the 19-th century) only needed a few fixed spaces Modern mathematics needs a wealth of new spaces and ample energy is devoted to the construction of these Set theory gives the illusion that all these spaces exist beforehand but it has the virtue that it unifies all needed concepts in one framework Type theory based on

• inductively defined data types with their

• recursively defined functions and closed under

• dependent products is an interesting alternative —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Ontology: Inductive Types

Inductive types (freely generated data types)

Natural numbers nat

 nat := 0 | S(nat)
 nat := 0:nat | S:nat→nat

Primitive recursion over nat: we postulate an f : nat,nat^{k}→nat such that

\begin{aligned}f(0, x⃗) & = & g(x⃗) \\ f(S(n), x⃗) & = & h(f(n, x⃗), n, x⃗) \end{aligned}

for g : nat^{k}→nat, h : nat,nat,nat^{k}→nat.

For example

\begin{aligned}0 + x & = & x & 0 ∗ x & = & 0 & 0! & = & 1 \\ S(n) + x & = & S(n + x) & S(n) ∗ x & = & (n ∗ x) + x & (S(n))! & = & n! ∗ (n + 1) \end{aligned}

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Ontology: other Data Types

Other data type: (binary) trees.

   tree := leaf:nat→tree | p:tree,tree→tree

Primitive recursion over trees: given g, h we postulate F such that

\begin{aligned}F (leaf(n), x⃗) & = & g(n, x⃗) \\ F (p(t_{1}, t_{2}), x⃗) & = & h(F (t_{1}, x⃗), F (t_{2}, x⃗), t_{1}, t_{2}) \end{aligned}

For example

mirror(leaf(n)) = leaf(n)
mirror(p(t_{1}, t_{2})) = p(mirror(t_{2}), mirror(t_{1}))

No need to code such structures into numbers via the Chinese remainder theorem (Gödel)

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Ontology: Type Theory

Function space types If A, B are types, then A→B is the type of functions from objects of type A into objects of type B.

{a : A f : (A→B) \atop (f a) : B} {f : (A→B) g : (B→C) \atop (g ∘ f) : (A→C)}

Dependent products

{Γ, n:A ⊢ B(n) : type \atop ⊢ Π_{n:A}.B(n) : type}

Functional abstraction

λx.f(x)

stands for the function x ⟼ f(x). For example, g ∘ f = λx.g(f(x))

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Logic

First order: rules for →, & , ∨, ¬, ⇔ , ∀x∈U, ∃x∈U Continuity: ∀ϵ>0∀x∃δ∀y. …, uniform continuity: ∀ϵ>0∃δ∀x, y. …

Second-order: rules for ∀X⊆U, ∃X⊆U An element x in a group G has torsion iff ∃n∈ℕ.x^{n} = e This definition is not allowed in pure first order logic. In second-order logic:

∀X⊆G[x∈X & (∀y∈X.xy∈X) ⇒ e∈X]

Higher-order statements O is a topology on X There exists a topology on U such that F is continuous —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Logic: Intuitionism

Brouwer: Aristotelian logic is unreliable It may promise existence without being able to give a witness

⊢ ∃n∈ℕ.P (n), but ⊬ P (0), ⊬ P (1), …

Heyting: charted Brouwer’s logic Gentzen: gave it a nice form

Example of such a P

P (n) ⇔ (n = 0 & GRH) ∨ (n = 1 & ¬GRH)

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Logic: “Intuitionism has become technology” (Constable)

Theorem-classical [No effectiveness] For every ideal I = (p_{1}, …, p_{n}) in ℚ[x⃗] there is a Gröbner basis P of I.

Theorem-classical [This does not give the theorem] There is a Turing machine TM such that for every ideal I = (p_{1}, …, p_{n}) in ℚ[x⃗] the result TM(p_{1}, …, p_{n}) = P is a Gröbner basis of I.

Theorem-classical [We do not always want to be explicit] Let TM = ⟨⟨q_{0}, ..⟩, …⟩. Then TM is a Turing machine and for every ideal I = (p_{1}, …, p_{n}) in ℚ[x⃗] the result TM(p_{1}, …, p_{n}) = P is a Gröbner basis of I.

Theorem-constructively. [Effectiveness] For every ideal I = (p_{1}, …, p_{n}) in ℚ[x⃗] there is a Gröbner basis P of I.

Building an intuitionistic library provides certified tools —————————————————————————————————–

Logic: Natural Deduction

Γ ⊢ A means: in context Γ one can derive A.

\begin{aligned}& A∈Γ \\ Γ ⊢ A \end{aligned}

{Γ ⊢ A Γ ⊢ A→B \atop Γ ⊢ B} {Γ, A ⊢ B \atop Γ ⊢ A→B}

Γ ⊢ A ; x ∉ Γ ; Γ ⊢ ∀x.A Γ ⊢ ∀x.A ; t is free in A ; Γ ⊢ A[x := t]

HB  Mathematical Software  Beijing, August 19, 2002

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Logic: propositions-as-types, proofs as lambda terms

Γ ⊢ p : A means: in context Γ one can derive A with proof p

\begin{aligned}& x:A∈Γ \\ Γ ⊢ x : A \end{aligned}

{Γ ⊢ p : A Γ ⊢ q : A→B \atop Γ ⊢ (q p) : B}  {Γ, x:A ⊢ p : B \atop Γ ⊢ (λx:A.p) : A→B}

Γ ⊢ p : A ; x ∉ Γ ; Γ ⊢ (λx:D.p) : ∀x:D.A Γ ⊢ p : ∀x.A

t is free in A

Γ ⊢ (p t) : A[x := t]

A proof of A→B is an algorithm transforming proofs of A into those of B Γ ⊢_{L} p : A is decidable, A proof of ∀x:D.A(x) is an algorithm transforming a d:D into a proof of A(d) where L is first, second or higher-order logic.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Proof-assistants: formalized proofs are difficult to obtain.

Assistance

Reliability? The de Bruijn criterion: have a small checker.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Proof-assistants: romantic proofs vs. cool proofs

A romantic proof

Theorem. For all d > 0 and all n∈ℕ there exist q, r∈ℕ such that

d < n & n = d ∗ q + r.

Proof. Given 0 < d∈ℕ write

P_{d}(n) := ∃q, r∈ℕ[r < d & n = dq + r].

By applying course of value induction on n we show ∀n∈ℕ.P (n). So let n∈ℕ and assume

∀m < n P (m)  (ih)

in order to show P (n). If n < d, we can take q = 0, r = n. If n ≥ d, write n′ := n − ˙ d. Then n′ < n and hence by (ih)

P (n′).  (H1)

Hence for some q′, r′∈ℕ

n′ = d ∗ q′ + r′ & r′ < d.  (H2)

Now take q = q′ + 1 and r = r′. Then r < d and d ∗ q + r = d ∗ q′ + r + d = n′ + d = n, so we are done.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Proof-assistants: romantic proofs vs. cool proofs

A cool proof (proof-object)

Proposition. ∀d:ℕ[0 < d ⇒ ∃q, r:ℕ.(r < d) & n = d ∗ q + r] Proof.

Proof-object —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Using a proof assistant

Coq: Arithmetic0 Coq: Course of value induction Coq: Euclid —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: computations and intuition

How does one give formal proofs of

• Computations

\begin{aligned}(xy − x^{2} + y^{2})(x^{3} − y^{3} + z^{3}) & = & x^{4}y − xy^{4} + xyz^{3} − x^{5}+ \\ & & x^{2}y^{3} − x^{2}z^{3} + y^{2}x^{3} − y^{5} + y^{2}z^{3}. \end{aligned}

• Intuition

Let f : ℝ→ℝ be defined by

f(x) = \frac{e^{x} + e^{−x}}{2} + e^{sin^{2} x} + e^{cos^{2} x.}

Then f is continuous. It is important to formally prove computations, not just for computational statements, but also for statements involving intuition —————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: proving computational statements

[figure: log a; 2.; log b; a; e^{−}; square; b; e^{−}; a^{+}; f; b^{+}; a; F; b]

Some computations f come for free: f(a^{+}) = b^{+} is built into the system. This is the so-called Poincaré Principle:

If f(a) = b, via an external computation, then a = b axiomatically.

The class P of f’s for which this is postulated may vary, but usually contains the primitive recursive computations. Two extreme cases P = ∅ and P is the class of all Computer Algebra definable maps do uccur.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: Applying the Poincaré Principle

In our case the map + is not the logarithm but usually of a syntactic coding nature (reflection): ((x + y)^{2})^{+} = sq(plus var_{x} var_{y}) and f is something like a simplify function on these syntactic expressions. The role of the exp function is played by the semantic function [[ ]].

   [figure: times(minusxy)(plusxy); smpl.; minus(sqx)(sqy); (x − y)(x + y); [[ ]]; =_{provably}; (x^{2} − y^{2}); [[ ]]]

In order to apply this freely one has to show

∀e:L.[[e]] = [[smple]]

once and for all.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: dealing with intuition

Goal to prove

A(t)

Pattern generalization Strategy: write t = f(s) with s∈L and try to prove

∀x∈L.A(f(x))

giving A(f(s)), hence A(t).

This method is particularly powerful if combined with reflection. Again we need to prove a computational equality f(s) = t.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: application of reflection

Claim. Let g : ℝ→ℝ be defined by

g(x) = \frac{e^{x} + e^{−x}}{2} + e^{sin^{2} x} + e^{cos^{2} x}

Then g is continuous Proof. Use pattern generalization with

• A language L of expressions for continuous functions

• A valuation [[ ]] : L→(ℝ→ℝ)

• ∀t∈L.[[t]] is continuous

• [[ λx.\frac{e^{x}+e^{−x}}{2} + e^{sin^{2} x} + e^{cos^{2} x} ]](x) = \frac{e^{x}+e^{−x}}{2} + e^{sin^{2} x} + e^{cos^{2} x} A(g) := ‘g is continuous’, F (t) = [[t]], ∀t:L.A([[t]]) and F ( g ) = g.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Facing problems: partial reflection

Proofs of computational equalities between rational expressions like

∀x, y∈ℂ.x ≠ y & x ≠ −y ⇒ \frac{1}{x + y} + \frac{1}{x − y} = \frac{2x}{x^{2} − y^{2}}

are obtained by partial reflection and pattern generalization.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Case studies

Formalized in Coq (intuitionistic proofs)

Theorem 1. [Formalization: Geuvers, Wiedijk, Zwanenburg, Pollack, Niqui] Every non-constant polynomial p(x) over ℂ has a root x.

Theorem 2. Collaboration between Coq and GAP

[Formalization: Oostdijk, Caprotti, Elbers]

The number 9026258083384996860449366072142307801963 is a prime. (Based on little Fermat’s theorem and Pocklington.)

Theorem 3.

[Formalization: Capretta]

Correctness of the Fast Fourier Transform.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Theorem 4. [Formalization: Person, Théry] Correctness of an efficient Gröbner base algorithm.

Theorem 5. [Formalization: Danos, Gonthier, Werner] Main lemma for the four colour theorem.

For this, Coq needed an overdrive: compilation rather than interpretation

This compiler was proved correct in the simpler version of Coq

Cf.

• Human eye  Romantic proof
• Light microscope  Cool proof
• Electronic microscope Hyper cool proof

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Challenge: to formalize substantial parts of mathematics

Start with undergraduate mathematics. Needed • Libraries: theories, algorithms.

• Tools for proving computations, intuitive steps.

• Interface: views, proof by clicking, library management.

• Make formalization as easy as writing down a proof in LaTeX, by developing a mathematical proof language (like Mizar has).

• International collaboration: Bologna database HELM.

• There is an onto-logical shift ⊢_{PA} ∀x.P (x) ⊢_{λL} ∀x:nat.P (x) ⊢_{ZF} ∀x∈ω.P (x)

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Mathematical assistants

System  Underlying logic  Poincaré Principle
Mizar  ZF  ∅
HOL, Isabelle, Isar HOL  ∅
[Automath]  λP  β
NuPrl  extensional TT  βδι
Agda  λP  βδι
Coq, Lego, Plastic λP ω  βδι
ACL2, PVS  Prim. Rec. Arithmetic? “Cas”

See ⟨www.cs.kun./nl/~freek⟩ for a longer (commented) list. See Barendregt, Cohen, Issac 2000, Special Issue JSC, for references.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Moral

The computer algebra community has done and is doing impressive work. But the work will not be finished until the semantical content of mathematics is fully encorporated.

—————————————————————————————————–

HB  Mathematical Software  Beijing, August 19, 2002

Encore

There are modern functional programming languages with • Every object is a typed function (no side effectes)

• Implementation is efficient

• Only meaningful combinations can be made

• Interaction can be programmed nicely with higher order functions

• The language has mobile code (dynamic linking)*

This makes it possible to bring down development time, during the design, debugging and maintenance. The mobile code makes possible distributed and parallel computing over the internet. Clean (Nijmegen) *only in Clean Haskell (Glasgow)

Slides powered by advi