Thread: Structural Induction problem

Hi, I am now struggling with structural induction, this cannot be proved so I needed to prove with stronger property but I am stuck... please help with proving..

so, this is based on Haskell property (tree structure)

so 'Haskell' definition of binary tree is

data Tree a = Nul
| Node a (Tree a) (Tree a)

so basically, if the tree has no node then it is Nul or otherwise tree a has node a and left to it another tree that has less number than a and another tree on the right with the number greater than Node a.

so the problem has this property.


mult Nul = 1 ------ (M1)
mult (Node a t1 t2) = a * mult t1 * mult t2 ------ (M2)

multa t = multb t 1 ------ (MA)

multb Nul acc = acc --------- (MB1)
multb (Node a t1 t2) acc = multb t1 (a * (multb t2 acc)) ---- (MB2)


and I need to prove

mult t = multa t

certain two cannot be equal hence must prove with stronger property...

it seems that multb is acc times multiplication all nodes but I don't know how to prove from this point..

help me thank you very much for your support always..

Originally Posted by gomdohri

mult (Node a u1 u2) = multa (Node a u1 u2)
= a* mult u1 * mult u2 ----- (M1)
= a * multa u1 * multa u2 ---(M2)
= a * (multb u1, 1) * (multb u2 1) ----- IH1, IH2
= multa (Node a u1 u2) (RH)
= multb (Node a u1 u2) 1 ---- (MA)
= multb u1 (a * (mult b u2 acc) ) ---- (MB2)

You are right; the explanations on the right do not make much sense. For example, M1 has to do with nult Nul, but there is no Nul here. The transition from the second to the third line is justified by IH1 and IH2, not M2, and so on.

Originally Posted by gomdohri

it seems that multb is acc times multiplication all nodes

Yes, and

acc * mult t = multb t acc

is exactly the stronger induction hypothesis you need.

Amazing! I must admit I didn't understand a freakin' word you said...
Sorry but I have to ask what part of math is this and if you could recommend some texts about it. Curiosity will get me killed, I know.

Haskell is a functional programming languages. Programs in Haskell are regular mathematical equations, so one can use them to replace equal expressions as in ubiquitous in mathematics. This is in contrast to imperative programming languages where expressions may have side effects like changing values of variables.

So basically we have a term algebra generated by a unary functional symbol Nul and a ternary functional symbol Node. Then there are equations that define functions mult, multa and multb by recursion. Even though this setting is studied in universal algebra and category theory, the closest math area is logic, in particular, proof theory and complexity theory, which study syntactic expressions.

Recently theories were developed that unite functional programming and proofs. They are based on Curry-Howard correspondence between proofs and programs. So, in a single theory one can write a functional program like mult and also construct a proof of its properties, like mult (Node a t1 t2) = mult (Node a t2 t1). This proof would also be a program that constructs evidence of the equality from given evidences like axioms and assumptions. One example of such theory is Calculus of Inductive Constructions. It is a descendant of Church's typed lambda calculus, and besides ideas from this calculus, it heavily uses induction principles for various term algebras.

Edit: I'll think about good sources on this topic.

Oh... my mistake. I put it in wrong place M1 should be M2 and M2 should be IH1 and IH2. Sorry about that.

Let me try the rest and if I am still struggling with this I will reply this message again. Thank you

Originally Posted by MathoMan

Amazing! I must admit I didn't understand a freakin' word you said...
Sorry but I have to ask what part of math is this and if you could recommend some texts about it. Curiosity will get me killed, I know.

Visit this page and learn haskell! Learn You a Haskell for Great Good!

HAHA... to think id actually find this just when i was stuck as well... gomdohri... your from ANU arent you.. in any case... im a little fuzzy about the whole tree thing... why is it that acc is acc*mult t ?? i understand the situation about proving with a stronger property but i just couldnt get the revised property as i was unsure how to place the acc..