partial functions & domain conditions

Freek Wiedijk & Jan Zwanenburg University of Nijmegen

TPHOLs 2003 Rome

2003 09 11, 09:30

the context

proof checking of mathematics

Metamath Agda Coq NuPRL

serious mathematical libraries →  \begin{matrix}Mizar \\ Isabelle \\ HOL \end{matrix} \}

no empty types no partial functions

PVS IMPS ACL2 Theorema Otter some partial operations in mathematics

x/y  y ≠ 0
\sqrt{x}  x ≥ 0
tan x  ∃n. nπ − \frac{π}{2} < x < nπ + \frac{π}{2}
lim_{x→a} f(x)  f is continuous in a
∫_{a}^{b} f(x) dx  f is integrable on [a, b]

function application in set theory (Mizar, Isabelle/ZF, Metamath, B method)

f(x)  f is a function ∧ ← set of pairs
x ∈ dom f

partial functions & proof assistants

approach I: making all functions total give each partial function a convenient value outside its domain approach used by ACL2 1/0 = 0 (car nil) = nil approach possible in all systems disadvantages: not faithful to actual mathematics the need to remember ‘special cases’ example

tan π = 0 = \frac{1}{1 − 0} − \frac{1}{1 + 0} = \frac{1}{1 − tan \frac{π}{2}} − \frac{1}{1 + tan \frac{π}{2}} tan \frac{π}{2} = 0 ≠ −\frac{1}{2} = 0 − \frac{1}{2} = \frac{1}{0} − \frac{1}{2} = \frac{1}{1 − tan \frac{π}{4}} − \frac{1}{1 + tan \frac{π}{4}}

approach II: undefined behavior outside domain

give each partial function some arbitrary value outside its domain ‘1/0 is some real number, but we can’t prove which one’

approach used by HOL, Isabelle, Mizar

disadvantages: not faithful to actual mathematics not possible to state that the meaning of an expression is ‘known’

example

tan 2θ = \frac{1}{1 − tan θ} − \frac{1}{1 + tan θ} : truth value is unknown for θ = \frac{π}{2} approach III: using the type system ← this talk

encode the domain of the partial function in its type make application outside that domain a type error

approach used by Coq, PVS

disadvantages: complicates logic doing type-related proofs is extra work

example Coq: division and tan both get an extra ‘proof’ argument

tan_{H_{1}} 2θ = 1/_{H_{4}}(1 − tan_{H_{2}} θ) − 1/_{H_{5}}(1 + tan_{H_{3}} θ)

PVS: proofs don’t occur explicitly in the terms (TCCs) approach IV: having a true logic of partial terms

approach used by LCF, IMPS

disadvantages: complicates logic how to deal with equality of undefined terms: 1/0 = 1/0 ?

different kinds of equality?

undefined truth values?

examples

tan θ ↓ ⇔ ∃n. nπ − \frac{π}{2} < θ < nπ + \frac{π}{2}

tan 2θ ⊒ \frac{1}{1 − tan θ} − \frac{1}{1 + tan θ}

the importance of first order logic two reasons to want a system based on total first order predicate logic

• best known easier for users of the system

• prover technology Otter, Spass, Gandalf, Vampire, Bliksem, Waldmeister,

E-SETHEO, DCTP, etc.

this talk: how to have approach III and total FOL at the same time

↑ |

‘applying a partial function outside its domain is a type error’

the goal the user gives for each partial function f a domain predicate D_{f}

D_{/}(x, y) ⇔ y ≠ 0
D_{tan}(θ) ⇔ ∃n. nπ − \frac{π}{2} < θ < nπ + \frac{π}{2}

the system calculates for each formula domain conditions DC(φ)

DC(tan 2θ = \frac{1}{1 − tan θ} − \frac{1}{1 + tan θ} ) =

\{ ⊢ ∃n. nπ − \frac{π}{2} < 2θ < nπ + \frac{π}{2} , ⊢ ∃n′. n′π − \frac{π}{2} < θ < n′π + \frac{π}{2} ,

⊢ tan θ ≠ 1 , ⊢ tan θ ≠ −1 }

the system uses total FOL to infer formulas and domain conditions (during steps in the proofs it may reason about 1/0)

three logical systems

system T: the operational logic

the well-known classical first order logic with Total functions 24 derivation rules in the paper

T ::= x_{i} | c_{i} | f_{i}(T , …, T ) | if F then T else T
F ::= ⊥ | P_{i}(T , …, T ) | T = T | F → F | ∀x_{i}. F

if-then-else construction

if x ≠ 0 then \frac{1}{x} else 0

needed to make the proofs manageable

constant symbols in the language our result doesn’t hold when constants are nullary functions system P: the intended logic logic with Partial functions in type theoretical style 24 derivation rules in the paper as close as possible to system T: untyped, classical, first order every function gets one extra argument:

f(x_{1}, …, x_{a}) ⇝ {α : D_{f}(x_{1}, …, x_{a}) \atop f(x_{1}, …, x_{a}, α)}
\frac{x}{y} ⇝ {α : y ≠ 0 \atop div(x, y, α)}

implications turn into a product and bind a proof variable:

∀x. x ≠ 0 → \frac{1}{x} ≠ 0 ⇝ ∀x. Π_{H:x≠0}. div(1, x, H) ≠ 0
if x ≠ 0 then \frac{1}{x} else 0 ⇝ if x ≠ 0 then _{H:x≠0} div(1, x, H) else _{H′:x=0} 0

erasure of proof terms | · | maps system P to system T

inductively defined following the structure of the argument

|f(t_{1}, ⋯, t_{a}, α)| = f(|t_{1}|, …, |t_{a}|)
|Π_{H:φ}. ψ| = |φ| → |ψ|
|if φ then _{H:φ} t else _{H′:¬φ} u| = if |φ| then |t| else |u|

domain conditions DC_{Γ}(·) maps a system T expression to a set of system T judgments

inductively defined following the structure of the argument

DC_{Γ}(f(t_{1}, …, t_{a})) = DC_{Γ}(t_{1}) ∪ … ∪ DC_{Γ}(t_{a}) ∪
{Γ ⊢ D_{f}(t_{1}, …, t_{a})}
DC_{Γ}(φ → ψ) = DC_{Γ}(φ) ∪ DC_{Γ, φ}(ψ)
DC_{Γ}(if φ then t else u) = DC_{Γ}(φ) ∪ DC_{Γ, φ}(t) ∪ DC_{Γ, ¬φ}(u)

main correspondence result statement together with domain conditions provable in system T

⟺ that statement provable in system P

more precisely: Γ ⊢^{P} wf

Γ ⊢^{P} φ ⇒ |Γ| ⊢^{T} |φ| & DC_{|Γ|}(|φ|)
|Γ| ⊢^{T} φ′ & DC_{|Γ|}(φ′) ⇒ ∃ φ . |φ| = φ′ & Γ ⊢^{P} φ

how the proof works system D: a third system term arguments have to stay inside the Domain ‘forbidden to reason about undefined objects’ system T formulas system P derivation rules

·^{∗} lifting from system T to system D f(t_{1}, …, t_{a})^{∗} = if D_{f}(t_{1}^{∗}, …, t_{a}^{∗}) then f(t_{1}^{∗}, …, t_{a}^{∗}) else c_{0}

facts:

Γ ⊢^{T} φ ⇒ Γ^{∗} ⊢^{D} φ^{∗}
Γ ⊢^{T} φ & DC(Γ) & DC_{Γ}(φ) ⇒ Γ ⊢^{D} φ

conclusions

domain conditions don’t respect logical equivalence!

DC(x ≠ 0 ∧ \frac{1}{x} > 1) ≠ DC(\frac{1}{x} > 1 ∧ x ≠ 0)

‘left-to-right evaluation’ φ ∧ ψ ≡ ¬(φ → ¬ψ) DC_{Γ}(φ ∧ ψ) = DC_{Γ}(φ) ∪ DC_{Γ, φ}(ψ)

strange in logic, but common in programming:

                 if (x != 0 && 1/x > 1) {

…

                 }

is it worth it? proving domain conditions is extra work

popularity of PVS is encouraging it can’t be worse than a total system

theoretical questions • same theory without if-then-else?

• equivalent theory for higher order logic? implementation?

‘partial Mizar’