Commit 0e7d57fe authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

short description of HOL-Light

parent e47fb632
A Brief Description of HOL-Light
================================
Reference: [HOL Light: an overview. John Harrison](http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf)
## The logical framework
All starts with (polymorphic) simply-typed lambda-calculus.
#### The types
- Polymorphic type variable : `α, β, ...`
- Two primitive types : `bool` (for boolean, i.e. here all statements) and `ind` (individual, won't use it today).
- One type constructor : the functional arrow `→`.
#### The values
- Variables `x, y, z, ...`
- Functions `λx. t`
- Application `t(u)`
- Two predifined constants : `(=) : α → α → bool` and `ε : (α → bool) → α` (Hilbert choice operator).
Syntax : `t = u` is just `(((=) t) u)`.
And when `p` and `q` are of type `bool` (hence propositions), `p = q` is rather written `p ⇔ q`.
#### The deducibility predicate
Unlike in Coq or Agda, provability is **not** based on a typing relation. The type system is just here to ensure that propositions (and other
elements) are well-formed.
So for a proposition `p` (i.e. a well-typed lambda-term of type `bool`) and a context `Γ` (i.e. a set of well-typed lambda-terms of type `bool`), a separate predicate `Γ ⊢ p` will express that `p` is deducible from `Γ`.
This deducibility predicate is obtained through the following ten inference rules
## The logical rules
```
--------- (REFL)
⊢ t = t
Γ ⊢ s = t ∆ ⊢ t = u
-------------------------- (TRANS)
Γ ∪ ∆ ⊢ s = u
Γ ⊢ s = t ∆ ⊢ u = v
--------------------------- (MK_COMB)
Γ ∪ ∆ ⊢ s(u) = t(v)
Γ ⊢ s = t
------------------------- (ABS)
Γ ⊢ (λx. s) = (λx. t)
----------------- (BETA)
⊢ (λx. t)x = t
----------- (ASSUME)
{p} ⊢ p
Γ ⊢ p ⇔ q ∆ ⊢ p
--------------------- (EQ_MP)
Γ ∪ ∆ ⊢ q
Γ ⊢ p ∆ ⊢ q
------------------------------- (DEDUCT_ANTISYM_RULE)
(Γ − {q}) ∪ (∆ − {p}) ⊢ p ⇔ q
Γ[x1,...,xn] ⊢ p[x1,...,xn]
---------------------------- (INST)
Γ[t1,...,tn] ⊢ p[t1,...,tn]
Γ[α1,...,αn] ⊢ p[α1,...,αn]
---------------------------- (INST_TYPE)
Γ[γ1,...,γn] ⊢ p[γ1,...,γn]
```
## The other logical connectives
On top of predefined equality `=` (and hence equivalence `⇔` on propositions), the other logical connectives are "syntactic sugar" :
```
T := (λp. p) = (λp. p)
p ∧ q := (λf. f p q) = (λf. f T T)
p ⇒ q := (p ∧ q) ⇔ p
∀P := P = (λx. T)
∃P := ∀q. (∀x. P (x) ⇒ q) ⇒ q
p ∨ q := ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊥ := ∀p. p
¬ := p ⇒ ⊥
∃!P := ∃P ∧ (∀x. ∀y. P x ∧ P y ⇒ x = y)
```
And `∀x.P x` is a notation for `∀(λx.(P x))`, and similarly `∃x.P x` is `∃(λx.(P x))`.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment