Avvio di una sessione

Una sessione è avviata da uno script F#. Innanzitutto è necessario referenziare la dll e importare i relativi moduli:

#r "nuget: nholz2"
open HOL

impostare il pretty printing delle espressioni:

fsi.AddPrinter print_type
fsi.AddPrinter print_qtype
fsi.AddPrinter print_term
fsi.AddPrinter print_qterm
fsi.AddPrinter print_thm

e caricare quindi i moduli con i seguenti comandi:

CoreThry.load
Equal.load
Bool.load
BoolAlg.load
BoolClass.load
Pair.load
Ind.load
Nat.load
NatNumrl.load
NatArith.load
NatRel.load
NatEval.load

I primi pochi secondi di avvio richiedono il build del sistema da zero. Alcune centinaia di righe di output scorrono velocemente sullo schermo.

// ...
// [HZ] Storing theorem "sub_floor_thm".
// [HZ] Setting term fixity for name ">".
// [HZ] Declaring constant ">".
// [HZ] Adding definition for constant ">".
// [HZ] Setting term fixity for name ">=".
// [HZ] Declaring constant ">=".
// [HZ] Adding definition for constant ">=".
// val it : (string * thm) list =
//   [("eta_ax", |- !(f:'a->'b). (\x. f x) = f);
//    ("imp_antisym_ax", |- !p1 p2. (p1 ==> p2) ==> (p2 ==> p1) ==> (p1 <=> p2));
//    ("infinity_ax", |- ?(f:ind->ind). ONE_ONE f /\ ~ ONTO f);
//    ("select_ax", |- !(P:'a->bool) x. P x ==> P ($@ P))]
// 
// >

il sistema è quindi pronto per ricevere i comandi dall'utente. Questi comandi sono di fatto espressioni F#.

Panoramica d'uso

Questa sezione fornisce una breve introduzione a semplici operazioni, incluso come immettere espressioni HOL e come eseguire una semplice dimostrazione.

Termini e tipi

Le espressioni nel linguaggio HOL sono chiamati termini HOL. I termini sono scritti utilizzando una stringa di caratteri ASCII a cui va applicata la funzione parse_term. Nel momento in cui si immette un termine in una sessione questo viene controllato e ristampato a video.

La sintassi dei termini è semplice e intuitiva Per esempio, il seguente termine significa ''per tutti i numeri naturali x, y e z, se x è minore di y e y è minore di z allora x è minore di z'':

@"!x y z. x < y /\ y < z ==> x < z" |> parse_term

val it: term = `!x y z. x < y /\ y < z ==> x < z`

Se si immette un termine mal formato si riceverà un messaggio di errore.

"x =" |> parse_term

// > 
// HOL.Exn+HolErr: [HZ] SYNTAX ERROR: Unexpected end of quotation instead of RHS for infix "="
// ...

Si noti che i messaggi specifici del sistema, diversamente da quelli che derivano dall'interprete F#, in generale, hanno il prefisso `[HZ]'. Questo vale per tutti i messaggi riportati da NHOLZ, inclusi messaggi di errore, warnings e feedback generici all'utente.

HOL è un linguaggio tipizzato, così ogni termine e sottotermine ha un tipo, e i termini devono essere costruiti in modo da avere un tipo corretto. Questo impedisce la costruzione di enunciati privi di significato come ''3 è uguale a vero''.

"3 = true" |> parse_term
// > 
// HOL.Exn+HolErr: [HZ] TYPE ERROR: Function subterm domain type incompatible with argument subterm type

I sottotermini possono essere annotati per indicare il loro tipo, facendo seguire al sottotermine il simbolo di due punti : e poi il suo tipo, il tutto chiuso tra parentesi. Il meccanismo di inferenza del tipo è usato per risolvere i tipi nei termini. Ad ogni termine inserito senza annotazioni di tipo sufficienti sono assegnate delle variabili di tipo numerate per tutti i tipi non determinabili. Di default i termini sono ristampati indietro con solamente le annotazioni di tipo sufficienti per evitare qualsiasi ambiguità circa i tipi di ogni sottotermine.

"!(w:nat) (x:nat) y z. w = x /\ y = z" |> parse_term

val it: term = `!(w:nat) x (y:'1) z. w = x /\ y = z`

I tipi HOL possono essere scritti fuori dal contesto di un termine usando la funzone parse_type.

"nat#nat->bool" |> parse_type

val it: hol_type = `:nat#nat->bool`

Teoremi, Dimostrazioni ed Asserzioni

I teoremi HOL consistono di un insieme di termini di assunzione con valore booleano e di un termine conclusione con valore booleano, e sono riservati ad enunciati di cui si è stabilito che valgono (per dimostrazione o asserzione - si veda sotto). Il significato di tali enunciati è che la conclusione vale assumendo che valgano tutte le assunzioni. I teoremi sono mostrati usando un turnstile (|-) per separare tutte le assunzioni dalla conclusione. Il sistema di base contiene già oltre 100 teoremi pre-dimostrati, ognuno dei quali non ha assunzione.

excluded_middle_thm

val it: thm = |- !p. p \/ ~ p

Le regole di inferenza della logica HOL sono qui implementate come funzioni F# che prendono teoremi e/o termini e restituiscono teoremi. Un passo di dimostrazione è eseguito semplicemente valutando l'applicazione di una tale funzione.

"x + y < 5" |> parse_term |> assume_rule
// val it : thm = x + y < 5 |- x + y < 5

spec_rule ("a = 0" |> parse_term) excluded_middle_thm
// val it : thm = |- a = 0 \/ ~ (a = 0)

Le dimostrazioni sono semplicemente espressioni F# composte con applicazioni di regole di inferenza ad ogni livello.

deduct_antisym_rule
    (contr_rule ("~ true" |> parse_term) (assume_rule ("false" |> parse_term)))
    (eq_mp_rule (eqf_intro_rule (assume_rule ("~ true" |> parse_term))) truth_thm)
// val it : thm = |- ~ true <=> false

il sistema supporta le seguenti teorie matematiche di base: logica predicativa, lambda calcolo, coppie ordinate e aritmetica dei numeri naturali.

Le teorie del sistema possono essere estese usando i comandi di teoria per dichiarare nuove costanti e costanti di tipo e per enunciare proposizioni a loro riguardo. Per esempio, il comando di definizione di costante introduce una nuova costante e restituisce un nuovo teorema, che afferma che il valore della costante è uguale a un'espressione data. Prende un termine di uguaglianza con la nuova costante come lato sinistro del'eguaglianza e il valore della costante come lato destro.

"max_height = 7" |> parse_term |> new_const_definition
// [HZ] Declaring constant "max_height".
// [HZ] Adding definition for constant "max_height".
// val it : thm = |- max_height = 7
namespace HOL
val print_type: ty: hol_type -> string
val print_qtype: ty: hol_type -> string
val print_term: tm: term -> string
val print_qterm: tm: term -> string
val print_thm: th: thm -> string
module CoreThry from HOL
<summary> This module completes the logical core for HOL by defining the core theory. This involves giving declarations, definitions and axioms for all the HOL theory objects anticipated by the language and inference kernels. </summary>
val load: (string * thm) list
module Equal from HOL
<summary> This module adds more constants and inference rules for basic reasoning using equality. </summary>
val load: (string * thm) list
<summary> Force module evaluation </summary>
module Bool from HOL
<summary> This module extends the boolean-related theory by giving definitions for classic predicate logic theory objects not introduced in 'CoreThry', and adds various derived syntax functions, theorems and inference rules. Note that derivations relying on the Axiom of Choice are separated out into the 'BoolClass' module. </summary>
module BoolAlg from HOL
<summary> This module proves various algebraic property theorems for the predicate logic operators. </summary>
module BoolClass from HOL
<summary> This module derives further predicate logic theorems and inference rules. Unlike all preceding derivations, these all use the Axiom of Choice (i.e. 'select_ax'), and thus could be considered as classical logic. However, note that some of these (such as 'exists_rule') are actually derivable in intuitionistic logic if an alternative definition of existential quantification is used (as in HOL Light). </summary>
module Pair from HOL
<summary> This module extends the HOL logic with the theory of ordered pairs. This involves giving theory object definitions for the product type operator, the pairing function and the constants "FST" and "SND", and proving a few basic properties. Syntax functions and equality congruence rules are also provided. </summary>
module Ind from HOL
<summary> This module extends the HOL logic with an infinite-cardinality base type, together with a zero and a successor function for this type. These get used in the 'Nat' module as the basis for defining the natural numbers. </summary>
module Nat from HOL
<summary> This module extends the HOL logic with the theory of natural numbers. This involves giving theory object definitions for the naturals base type and the "ZERO" and "SUC" constants, based on the theory of individuals, and proving a few important properties. </summary>
module NatNumrl from HOL
<summary> This module defines the representation of natural number numerals. This is based on the HOL functions "BIT0" and "BIT1". </summary>
module NatArith from HOL
<summary> This module defines some classic natural number arithmetic operators, using recursive function definition and the "SUC" and "ZERO" constants, and proves various basic properties about each operator. </summary>
module NatRel from HOL
<summary> This module defines the classic natural number arithmetic relations and derives various basic properties about them. </summary>
module NatEval from HOL
<summary> This module defines conversions for evaluating arithmetic operations on natual number numerals. Because large proofs may involve heavy numeric computation, special consideration is given to the efficieny of these functions. </summary>
val parse_term: x: string -> term
<summary> This takes a string and parses it into an internal term. The type analysis stage first detypes the preterm before inferring types (in 'resolve_preterm'), since the syntax analysis stage gives all variables and constants the null pretype. Note that type inference is capable of handling overloaded variables. </summary>
val parse_type: x: string -> hol_type
val excluded_middle_thm: thm
<summary> |- !p. p \/ ~p </summary>
val assume_rule: tm: term -> thm
<summary> This is the assumption rule. It takes a boolean term, and returns a theorem stating that the term holds under the single assumption of the term itself. `p` -------- {p} |- p </summary>
val spec_rule: tm: term -> th: thm -> thm
<summary> This is the universal elimination rule. It strips off the outermost universal quantifier from the supplied theorem, and replaces in the body each occurrence of the stripped binding variable with the supplied term. The type of the supplied term must equal the type of the stripped binding variable. `t` A |- !x. p ---------------- A |- p[t/x] </summary>
val deduct_antisym_rule: th01: thm -> th02: thm -> thm
<summary> This is the antisymmetry rule for deduction. It takes two theorem arguments. It returns a theorem stating that the supplied conclusions are equivalent, under the unioned assumptions but with each theorem's conclusion removed from the other's assumptions. A1 |- p A2 |- q -------------------------- A1\{q} u A2\{p} |- p &lt;=&gt; q See also: imp_antisym_rule, undisch_rule. </summary>
val contr_rule: tm: term -> th: thm -> thm
<summary> This is the intuitionistic contradiction rule. It takes a boolean term and a theorem with falsity as its conclusion. It returns a theorem with the supplied term as its conclusion, under the same assumptions as the supplied theorem. `p` A |- false ---------------- A |- p See also: ccontr_rule, deduct_contrapos_rule. </summary>
val eq_mp_rule: th1: thm -> th2: thm -> thm
<summary> This is the equality modus ponens rule. It takes an equality theorem and a second theorem, where the equality theorem's LHS is alpha-equivalent to the conclusion of the second theorem. It returns a theorem stating that the equality theorem's RHS holds, under the unioned assumptions of the supplied theorems. A1 |- p &lt;=&gt; q A2 |- p ------------------------ A1 u A2 |- q See also: mp_rule, eq_imp_rule1, eq_imp_rule2, imp_antisym_rule. </summary>
val eqf_intro_rule: th: thm -> thm
<summary> This is the falsity equivalence introduction rule. It takes a theorem with logical negation at its top level, and returns a theorem stating that the body of the negation is equivalent to falsity, under the same assumptions. A |- ~ p ---------------- A |- p &lt;=&gt; false See also: eqf_elim_rule, not_elim_rule, not_intro_rule, mk_not_rule, eqt_intro_rule. </summary>
val truth_thm: thm
<summary> |- true </summary>
val new_const_definition: tm: term -> thm