Results 1 to 7 of 7

Math Help - Structural Induction problem

  1. #1
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    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..
    Last edited by gomdohri; August 13th 2012 at 04:59 PM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,559
    Thanks
    785

    Re: Structural Induction problem

    Quote Originally Posted by gomdohri View Post
    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.

    Quote Originally Posted by gomdohri View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Sep 2010
    Posts
    185
    Thanks
    13

    Re: Structural Induction problem

    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.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,559
    Thanks
    785

    Re: Structural Induction problem

    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.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Re: Structural Induction problem

    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
    Follow Math Help Forum on Facebook and Google+

  6. #6
    Newbie
    Joined
    Aug 2012
    From
    China
    Posts
    18

    Re: Structural Induction problem

    Quote Originally Posted by MathoMan View Post
    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!
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Aug 2012
    From
    Singapore
    Posts
    1

    Re: Structural Induction problem

    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..
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. help with structural induction
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: June 1st 2011, 05:09 PM
  2. Strong induction vs. structural induction?
    Posted in the Discrete Math Forum
    Replies: 13
    Last Post: April 21st 2011, 01:36 AM
  3. Determine if this a structural property
    Posted in the Advanced Algebra Forum
    Replies: 0
    Last Post: February 15th 2010, 09:20 AM
  4. Computer Science Logic, Structural Induction?
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: February 5th 2010, 10:13 AM
  5. structural induction
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: October 19th 2009, 02:20 PM

Search Tags


/mathhelpforum @mathhelpforum