LARA

Differences

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

Link to this comparison view

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