Thursday, June 18, 2015

A Small Derivation

I completely forgot what my prover does; I rushed it anyway. So, I worked out a rough example by hand below to get some grasp on it. In a bottom up fashion it collects a mess of constraints, say it gathered

int:*∧ (::Ord int) ⊢t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)

It then proves that (roughly) likes this

int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 ∧ 
k0 = ka =* ∧ t0: = int:*∧ k1 = kb=* ∧ t1:* = int:* 
-----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ int:* = t4:k4 
 k0 = ka =* ∧ t0:* = int:*∧ k1= kb = * ∧ t1:* = int:* 
⊢ (::Ord int)
----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ int:*= t3:k3 ∧ t1:k1 = t4:k4 
∧ k0 = ka =* ∧ t0:* = int:* 
⊢ t1:k1:* = int:kb ∧ (::Ord t1)
-----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 
⊢ t0:k0 = int:ka ∧ t1:k1 = int:kb ∧ (::Ord t1)
----------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4:* ∧ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 
⊢ t0:k0->t1:k1 = int:ka->int:kb ∧ (::Ord t1)
---------------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 ∧ t0:k0= t3:k3 
⊢ t1:k1 = t4:k4 ∧ t0:k0->t4:k4 = int:ka->int:kb ∧ (::Ord t1)
-----------------------------------------------------
int:*∧ (::Ord int) ∧ k2 = * ∧ t2:* = t3:k3->t4:k4 
⊢ t0:k0= t3:k3 ∧ t1:k1 = t4:k4 ∧ t3:k3->t4:k4 = int:ka->int:kb ∧ (::Ord t1)
----------------------------------------------------
int:*∧ (::Ord int) ⊢ t0:k0->t1:k1 = t2:k2 ∧ t2:k2 = int:ka->int:kb ∧ (::Ord t1)

So, okay. Guess that works. I made a reasonable estimate of how constraints should be solved, dump the mess in the prover, from the antecedent I read off how to attribute the tree with the solved constraints.

It doesn't seem to handle intermediaries well, though. Guess I need to check it with the algorithm. (Hmm. Intermediaries should remain on the left-hand side of the equation?)

No comments:

Post a Comment