# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision | |||

sav08:theorems_as_abstract_data_types [2008/05/28 05:32] vkuncak |
sav08:theorems_as_abstract_data_types [2008/05/28 06:03] (current) vkuncak |
||
---|---|---|---|

Line 16: | Line 16: | ||

Soundness of the approach: if a value of type 'theorem' is computed, we know there exists an expression formed from ADT operations. This means that there is a proof tree, so the value is a theorem. | Soundness of the approach: if a value of type 'theorem' is computed, we know there exists an expression formed from ADT operations. This means that there is a proof tree, so the value is a theorem. | ||

+ | |||

+ | ===== Example Operations of Theorem ADT ===== | ||

+ | |||

+ | Often proof manipulating or even ADT functions are partial. We can express this using algebraic data types with alterbatives (e.g. option types), or using exceptions. These features, as implemented in ML do not compromise type safety. We illustrate this using propositional logic. | ||

+ | |||

+ | abstype theorem | ||

+ | groundT : formula -> theorem option // returns a theorem if given formula is ground and evaluates to true | ||

+ | inspect : theorem -> formula // return formula for theorem so we can decide how to prove it | ||

+ | cases : theorem -> theorem -> formula -> variable -> theorem option | ||

+ | andI : theorem -> theorem -> theorem | ||

+ | andE1 : theorem -> theorem option | ||

+ | |||

+ | Here 'cases t1 t2 f x' will compute f[x:=true] and check that it is identical to t1, then compute f[x:=false] and check it is identical to t2. If both tests succeed, it will return f as a theorem. | ||

+ | |||

+ | The 'andI' (and introduction) function takes two theorems and computes their conjunction, which is also a theorem. | ||

+ | |||

+ | The 'andE1' (first and-elimination) takes a theorem, checks whether it has the form 't1 & t2'. If so, it returns t1. | ||

+ | |||

+ | Using such ADT we can build a prover that is guaranteed to either produce correct result or fail (it will never produce a formula that is a non-theorem). | ||

+ | |||

+ | let rec prove (f : form) : theorem option = | ||

+ | if (isGround f) then (groundT f) | ||

+ | else (let v = getOneFreeVar f in | ||

+ | match (prove (subst [(v,True)] f), prove (subst [(v,False)] f)) with | ||

+ | | (Some t1, Some t2) -> cases t1 t2 f v | ||

+ | | _ -> None) | ||

+ | |||

+ | It can be tedious to propagate possible errors. This is why exceptions are so useful. | ||

+ | |||

+ | |||

+ | ===== Tactic and Tacticals ===== | ||

+ | |||

+ | Tactics accept formulas and try to produce the theorem containing this formula. | ||

+ | |||

+ | Tatics can often be combined into bigger tatics using higher-order functions called tacticals (for example, alternative, sequencing, repetition). | ||