the Mizar type system

Freek Wiedijk Radboud University Nijmegen

TPHOLs 2007 University of Kaiserslautern

2007 09 12, 10:00 this talk

• Mizar

• Mizar types

• the paper – the Mizar type system in the form of typing rules – correctness with respect to first order predicate logic Mizar versus the HOLs

Mizar  HOL

Isabelle PVS Coq ⋮

batch checking  interactive
first order logic  higher order logic
readable proofs  tactic scripts
untyped set theory  typed foundations

very nice type system

Mizar types

features

• dependent types

• no types built from types no function types A → B for types A and B

   (‘Ordinal → Ordinal’?)

• subtyping

• ‘attributes’

• structure types (records) Alternative Aggregates in Mizar Gilbert Lee and Piotr Rudnicki

MKM 2007, LNAI 4573

attributes

             non empty  finite

                                 Subset of NAT

↑  ↑
adjectives  radix type
attributes  mode

overloading meaning of an attribute depends on the radix type:

  – connected Relation
  – connected Graph
  – connected TopSpace

example

definition let d be  non zero Element of NAT ;
 func cyclotomic_poly d ->  Polynomial of F_Complex  means
   ex s being  non empty finite Subset of F_Complex
    st s = { y where y is  Element of MultGroup F_Complex  : ord y = d } &
       it = poly_with_roots((s,1)-bag);
end;

UNIROOTS Primitive Roots of Unity and Cyclotomic Polynomials

Broderick Arneson and Piotr Rudnicki 3293 lines, 135K

full Mizar library 985 ‘articles’, 1.97 million lines, 68.9M

typings also are formulas

       for i being Integer holds i >= 0 iff i is Nat

∀ i : ℤ . i ≥ 0 ⇔ ( i : ℕ )

                                   i is Nat ≠ i in NAT

↑  ↑
type  term
‘has type’  ‘is element of’
the type system  the set theory

‘coerce’ a term to a more informative type by giving a proof

…

then n' - n >= 0 by XREAL_1:50;
then reconsider d = n' - n as Nat by INT_1:16;

…

subtyping

definition let C be Category;
  mode Subcategory of C -> Category means
:: CAT_2:def 4

…

end;
                            set

↑

                         Category

↑

                     Subcategory of C

supertype may depend on the types of the arguments of the type clusters

   for X being set holds X is empty implies X is finite

↓

                cluster empty -> finite set

any term with attribute empty automatically also gets attribute finite

typed or untyped logic?

what does it all mean?

foundations of Mizar:

Tarski-Grothendieck set theory = ZFC + ‘there are arbitrarily large inaccessible cardinals’

set of axioms on top of untyped first order predicate logic the axioms of Mizar

TARSKI:def 3  X ⊆ Y ⇔ (∀x. x ∈ X ⇒ x ∈ Y)
TARSKI:def 5  ⟨x, y⟩ = {{x, y}, {x}}
TARSKI:def 6  X ∼ Y ⇔ ∃Z. (∀x. x ∈ X. ⇒ ∃y. y ∈ Y ∧ ⟨x, y⟩ ∈ Z) ∧
(∀y. y ∈ Y. ⇒ ∃x. x ∈ X ∧ ⟨x, y⟩ ∈ Z) ∧
(∀x∀y∀z∀u. ⟨x, y⟩ ∈ Z ∧ ⟨z, u⟩ ∈ Z ⇒ (x = z ⇔ y = u))

TARSKI:def 1  x ∈ {y} ⇔ x = y

TARSKI:def 2  x ∈ {y, z} ⇔ x = y ∨ x = z
TARSKI:def 4  x ∈ ⋃ X ⇔ ∃Y. x ∈ Y ∧ Y ∈ X
TARSKI:2  (∀x. x ∈ X ⇔ x ∈ Y) ⇒ X = Y
TARSKI:7  x ∈ X ⇒ ∃Y. Y ∈ X ∧ ¬∃x. x ∈ X ∧ x ∈ Y
TARSKI:sch 1  (∀x ∀y ∀z. P [x, y] ∧ P [x, z] ⇒ y = z) ⇒
(∃X. ∀x. x ∈ X ⇔ ∃y. y ∈ A ∧ P [y, x])
TARSKI:9  ∃M. N ∈ M ∧ (∀X∀Y. X ∈ M ∧ Y ⊆ X ⇒ Y ∈ M) ∧
(∀X. X ∈ M ⇒ ∃Z. Z ∈ M ∧ ∀Y. Y ⊆ X ⇒ Y ∈ Z) ∧
(∀X. X ⊆ M ⇒ X ∼ M ∨ X ∈ M)

translation to untyped logic

      for i being Integer holds i >= 0 iff i is Nat

∀ i : Integer . i ≥ 0 ⇔ ( i : Nat )

↓
∀ i . Integer (i) ⇒ [ i ≥ 0 ⇔ Nat (i) ]

types are just predicates that the system manages automatically dependent types with n arguments are predicates with n + 1 arguments

the type system as typing rules

symbolic notation

x  term variables
f  function symbols
M  mode symbols
α  attribute symbols
t ::= x | f(t⃗)  terms
R ::= ⋆ | M(t⃗)  radix types
a ::= α | ᾱ  adjectives
T ::= a⃗ R  types
J ::= · | t : T | T ≤ T | ∃ T | α/T  judgment elements
D ::= x : T  declarations
Δ ::= D⃗
Γ ::= \overrightarrow{[Δ](J)}
Γ; Δ ⊢ J  judgments

rules twenty-two typing rules three examples:

\overline{; ⊢ ·}

mode definition:

\frac{Γ; x⃗ : T⃗ ⊢ ∃ T′}{Γ, [x⃗ : T⃗](M(x⃗) ≤ T′), [x⃗ : T⃗](∃ M(x⃗)); ⊢ ·} M ∉ Γ

conditional cluster:

\frac{Γ; Δ ⊢ a⃗ T′ ≤ T′ Γ; Δ ⊢ a′ T′ ≤ T′}{Γ, [Δ](a⃗ T′ ≤ a′ T′); ⊢ ·}

correctness

translating judgments

type judgment → first order sequent

int ≤ ⋆, ∃ int, pos/int, ∃ pos int ; x : pos int ⊢ x : ⋆

→

(∀x. int(x) ⇒ ⊤) , (∃x. int(x)) , ⊤, (∃x. pos(x) ∧ int(x)) , (pos(x) ∧ int(x)) ⊢ ⊤

main theorem ‘the type system is correct’

derivable judgment → provable sequent

outlook

system in the paper is an idealization

definition let n be Nat;
  redefine mode Element of n -> Element of n + 1;
end;

according to the rules from the paper we have

Element of n → Element of n + 1 → Element of n + 2 → . . .

in the actual Mizar system we just have

Element of n → Element of n + 1

why not have something like the Mizar type system yourself? • the Mizar proof language is well-known to be nice

• the Mizar type system is less known, but very nice too

• every system can have the Mizar type system as a layer on top