Practical Reflection for
Formal Mathematics

Martin Giese

RICAM, Austrian Acad. of Sciences, Linz
Theorema Group

Workshop on Formal Groebner Bases Theory, Linz, 2006

Mathematical Theory Exploration

Mathematical Theory Exploration consists of:

But also:

And even:

Idea

Found a new reasoning technique?

Normally:

Idea:

Credits

Proving by First and Intermediate Principles
Invited talk at TYPES Workshop, Nov 1-2, 2004
University of Nijmegen,The Netherlands

Workflow

"ordinary" reasoning:

"meta" reasoning:

"ordinary" reasoning:

Reflection

Formulation of Reasoners means writing programs that manipulate terms and formulae

Therefore, the logic for the "meta" reasoning must contain representations of the syntactic entities of the logic used for the "ordinary" reasoning.

We want to use the same logic for "meta" and "ordinary" reasoning, so our logic will contain representations of its own syntax.

The term "Reflection" refers to a language that contains a representation of its own syntax.

Term Representation: Symbols

Many term representations are possible.

We decided to have a 'quoted' symbol in the logic as representation for every symbol.

In this talk, we represent quoted symbols for the term representation.  So

({{the symbol ... , represents the symbol ... }, {\(\(\ \)\(a\+_\)\(\ \)\), a}, {\(\(\ \)\(0\+_\)\(\ \)\), 0}, {\(\(\ \)\(\(a\+_\)\+_\)\(\ \)\), \(\(\ \)\(a\+_\)\(\ \)\)}, {…, …}})

Alternatives:

Enumerate symbols:

({{sym[zero] represents the symbol a}, {sym[succ[0]] represents the symbol b}})

Or use character codes:

({{sym[⟨97⟩] represents the symbol a}, {sym[⟨97, 98, 99⟩] represents the symbol abc}})

Term Representation: Variables

Assume that variables are different from other (constant) symbols.

Also represent variables by underined symbols:

({{the symbol ... , represents the variable ... }, {\(\(\ \)\(x\+_\)\(\ \)\), x}, {\(\(\ \)\(y\+_\)\(\ \)\), y}, {…, …}})

Note that a quoted variable is a constant symbol and not a variable.

Term Representation: Compound Terms

We also decided to reuse …[…] for construction of compound terms.

({{the term ... , represents the term ... }, {\(\(\ \)\(a\+_\)\(\ \)\), a}, {\(f\+_[b\+_]\), f[b]}, {({{\(f\+_[t]\)}, {where t represents a term}}), ({{f[s]}, {where s is the term represented by t}})}, { ({{\(t[a\+_]\)}, {where t represents a term}}), ({{s[a]}, {where s is the term represented by t}})}, {\(\((f\+_\( + \+_\)g\+_)\)[x\+_]\), (f + g)[x]}})

If f and t are term representations, f[t] is a compound term.
Otherwise, f[t] is the result of a function application.

Alternatives:

\(f\+_\([\+_\)b\+_\(]\+_\)\)

\(MkTerm[f\+_, b\+_]\)

An Example Exploration: Arithmetic of Natural Numbers

Axioms["nat constructors",any[n],
({{0 ∈ ℕ}, {\(n ∈ ℕ \[Implies] \(n\^+\) ∈ ℕ\)}})]

Axioms["nat sum",any[m ∈ ℕ, 
          n ∈ ℕ],
({{m + 0 := m}, {\(m + \(n\^+\) := \(\((m + n)\)\^+\)\)}})]

Proposition["0 left unit", 
      any[n ∈ ℕ], 
0 + n = 
        n]

Prove[Proposition["0 left unit"], using -> …, 
      by -> …]

and eventually...

Proposition["+ associative", 
      any[l ∈ ℕ, 
        m ∈ ℕ, 
        n ∈ ℕ], 
(l + 
              m) + n = l + (m + n)]

Prove[Proposition["+ associative"], using -> …, 
      by -> …]

Exploration continues: Multiplication

Define multiplication of natural numbers:

Axioms["nat product",any[m ∈ ℕ, 
          n ∈ ℕ],
({{m·0 := 0}, {\(m·\(n\^+\) := m + \((m·n)\)\)}})]

Now go on to show things about multiplication, using knowledge about addition:

\(Proposition["· associative", 
      any[l ∈ ℕ, 
        m ∈ ℕ, 
        n ∈ ℕ], 
\((l·m)\)·n = l·\((m·n)\)]\)

\(Prove[Proposition["· associative"], 
      using -> {…Proposition["+ associative"] …}, by -> …]\)

Probably the knowledge about +, like associativity is used quite heavily.

An Idea for a Reasoner

After doing some proofs involving addition, you might find out that
it's always possible, and often a good idea to write sums in right-associative form:  For instance, to take

((a + b) + (c + d)) + e

and rewrite it to

a + (b + (c + (d + e)))

You now would like to write a reasoner that can do this for you.

Reasoner just takes a term and simplifies it, so we call it a simplifier.

An implementation

Here is a formulation of the algorithm in the Theorema language with quoting:

Algorithm["shift parens right",any[t, t1, t2, l, acc],
({{simplify[t] := 
                sumList[collect[t, {}]]

              }, {\(collect[t1\( + \+_\)t2, acc] := 
                collect[t1, collect[t2, acc]]\)}, {collect[t, acc] := t⌣acc

              }, {\(sumList[{}] := 0\+_\)}, {sumList[{t}] := t}, {\(sumList[t⌣l] := t\( + \+_\)sumList[l]\)}})]

Formulating Soundness

When is such a simplifier sound?

First: it sends terms to terms:

\(Proposition["simplify is term function", 
      any[t], 
t ∈ 𝕋 \[Implies] simplify[t\ ] ∈ 𝕋]\)

Second: the result still means the same.

Two possibilities:

⊢(Underscript[∀ , t ∈ 𝕋])rewritable[t, simplify[t], KB]

KB⊢(Underscript[∀, ({{t ∈ 𝕋}, {β ∈ 𝔸}})])eval[t, β]=eval[simplify[t], β]

Reflection of Syntax/Semantics

Problems with Reflection of Syntax:

Reflection of Semantics avoids this, but:

Axioms for symbols and terms

Axiom Schemata for symbols. Let's use 𝕊 for the set of (quoted) symbols in the T'ma language, 𝕍 for the variable symbols and 𝕋 for the terms.

({{⊢\(a\+_\)∈𝕊    for all symbols  a}, {⊢\(x\+_\)∈𝕍    for all variables x
⊢𝕊 ⋂ 𝕍 = ∅}, {⊢0∉𝕊⋃𝕍   etc.}, {⊢t ∈ 𝕋 ∧ 
                  a ∈ 𝕋 \[Implies] 
                t[a] ∉ 𝕊 ⋃ 𝕍}, {⊢𝕊 ⋃ 𝕍 ⊆ 𝕋}, {⊢0 ∉ 𝕋}, {⊢t ∈ 𝕋 ∧ 
                  a ∈ 𝕋 \[Implies] 
                t[a] ∈ 𝕋}})

To prove inequalities between terms:

({{⊢\(a\+_\)≠\(b\+_\)     for all symbols/variables  a≠b}, {⊢t ∈ 𝕋 ∧ 
                  a ∈ 𝕋 ∧ 
                  s ∈ 𝕊 ⋃ 𝕍 \[Implies] t[a] ≠ s}, {⊢(Subscript[t, 1]) ∈ 𝕋 ∧ (Subscript[a, 1]) ∈ 𝕋 ∧ 
                  (Subscript[t, 2]) ∈ 𝕋 ∧ 
                  (Subscript[a, 2]) ∈ 𝕋 ∧ 
                  (Subscript[t, 1])[(Subscript[a, 1])] = (Subscript[t, 2])[(Subscript[a, 2])] \[Implies] 
                  (Subscript[t, 1]) = (Subscript[t, 2]) ∧ (Subscript[a, 1]) = (Subscript[a, 2])}})

Term Induction

No fixed type system or signatures => don't know arity of functions in advance.

Higher order terms => might not know head symbol of a term.

Therefore terms are inductive in 2 "dimensions"

Dimension 1: the nesting of terms

\(a\+_, \ f\+_[a\+_], \ f\+_[f\+_[a\+_]], \ …\)

Dimension 2: argument lists

\(\(\(f\+_[], \ f\+_[a\+_], \ f\+_[a\+_, a\+_], \ 
    f\+_[a\+_, a\+_, a\+_]\)\(
\)
    \)\)

({{(Underscript[∀ , s ∈ 𝕊])P[s]}, {(Underscript[∀ , v ∈ 𝕍])P[v]}, {(Underscript[∀ , head ∈ 𝕋])P[
                head] \[Implies] P[head[]]}, {(UnderBar[(Underscript[∀, ({{head ∈ 𝕋}, {t ∈ 𝕋}, {\(tail\&_ ∈ 𝕋–tuple\)}})])\((P[t] ∧ P[head[tail\&_]])\)\[Implies]\(P[head[t, tail\&_]]\)])}, {(Underscript[∀ , t ∈ 𝕋])P[t]}})

Axioms for evaluation function

eval function mimics evaluation function of model semantics.

Axioms like:

⊢v ∈ 𝕍 \[Implies] 
          eval[v, β] = β[v]

\(\(⊢\)\(eval[a\+_, β]\)\)=a     for all symbols  a

⊢t ∈ 𝕋 ∧ 
          a ∈ 𝕋 \[Implies] (eval[
              t[a], β] = eval[t, β][
              eval[a, β]])

which implies

({{\(eval[
              t\_1\( + \+_\)t\_2, β] = \(eval[\(+\+_\(\(,\)\(β\)\)\)]\)[eval[t\_1, β], 
              eval[t\_2, β]]\)}, {=eval[(Subscript[t, 1]), β] + eval[(Subscript[t, 2]), β]}})

Eval Caveat

Danger:

\(\(\(⊢\)\(eval[eval\+_, β]\)\) = eval\)

so:

⊢(Subscript[t, 1]) ∈ 𝕋 ∧ 
        (Subscript[t, 2]) ∈ 𝕋
\(	\(\(\[Implies]\)\(eval[eval\+_[t\_1, t\_2], β]\)\) = 
      eval[eval\+_[t\_1, β], eval\+_[t\_2, β]]\)

is no good as definition and leads to inconsistency

⟹ avoid defining \(eval[eval\+_]\) at all for the time being.

Later maybe have layers of eval: \(TraditionalForm\`eval\_1\ can\ evaluate\ \(eval\_0\)\+_\), \(TraditionalForm\`eval\_2\ can\ evaluate\ \(eval\_1\)\+_\),…

Proving Soundness

Let's prove:

(Underscript[∀ , t ∈ 𝕋])eval[simplify[t]] = 
      eval[t]

Strenghten induction: for all terms t and list of terms acc:

\(eval[sumList[collect[t, acc]]] = 
      eval[t\( + \+_\)sumList[acc]]\)

The Proof

Induction step: Statement holds for (Subscript[t, 1]) and (Subscript[t, 2]), show it for \(t\_1\( + \+_\)t\_2\).

\(eval[sumList[collect[t\_1\( + \+_\)t\_2, acc]]]\)
= eval[
        sumList[collect[(Subscript[t, 1]), collect[(Subscript[t, 2]), acc]]]]
\(\(\( = \&\(I . H . \)\)\(\ \)\(eval[
        t\_1\( + \+_\)sumList[collect[t\_2, acc]]]\)\)\)
= eval[(Subscript[t, 1])] + 
        eval[sumList[collect[(Subscript[t, 2]), acc]]]
\(\(\( = \&\(I . H . \)\)\(\ \)\(eval[t\_1] + 
        eval[t\_2\( + \+_\)sumList[acc]]\)\)\)
=eval[
          (Subscript[t, 1])] + (eval[(Subscript[t, 2])] + 
            eval[sumList[acc]])
=(eval[(Subscript[t, 1])] + eval[(Subscript[t, 2])]) + 
        eval[sumList[acc]]
\(\(\(=\)\(eval[t\_1\( + \+_\)t\_2] + 
        eval[sumList[acc]]\)\)\)
\(\(\(=\)\(eval[\((t\_1\( + \+_\)t\_2)\)\( + \+_\)sumList[
            acc]]\)\)\)

Putting the simplifier to work:

Now we can use the simplifier:

\(Compute[
      simplify[\((\((a\+_\( + \+_\)b\+_)\)\( + \+_\)\((c\+_\( + \+_\)d\+_)\))\)\( + \+_\)e\+_], 
      using -> Algorithm["shift parens right"]]\)

To use it like other reasoners, make it known to the system:

DeclareSimplifier[ShiftParens, simplify, 
      using -> Algorithm["shift parens right"]]

Now use it like other simplifiers

Compute[((a + b) + (c + d))+e,by -> ShiftParens]

Note: no mention of using->Proposition["+ associative"].

Related Work

Most closely related:

Meta-reasoning in NqThm and ACL2 (Boyer, Moore):

Can extend ACL2 theorem prover with simplifiers,
prove their soundness by Reflection of Semantics

Novelties in Theorema:

Conclusion

Next steps: