• English only

# Differences

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

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).