[Haskell-beginners] structural induction, two lists, simultaneous
Pascal Knodel
pascal.knodel at mail.com
Thu Dec 18 06:58:48 UTC 2014
> (∀ ys • (∀ f,zs • map f (ys ++ zs) = map f ys ++ map f zs))
>
> And now you can see that you want a proof of a one-variable theorem
Thank you, Rustom Mody, that's it, reordering of universal quantifiers.
By the way, I'm searching for a 'good' book about predicate logic for
quite some time now.
One with a strong link to mathematics and the quantification style
that is used there would be nice. By chance, is there a reference
(script/paper/book )
you would recommend?
I have rewritten my first proof a little. It mentions the other
variables now explicitly.
This way it should be cleaner:
-- 1. Induction Hypothesis (1. I.H.):
-- ----------------------------------
--
-- For an arbitrary but fixed list "ys", for all lists "zs" and for
all functions f the statement ...
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
-- ... holds.
When proving the proposition the first time I've used a different approach
(the chapter heavily promoted generalization and because I tried to get
around
the dilemma that I wasn't sure if I understood 'simultaneous induction'
correctly):
-- ---------------
-- 1. Proposition:
-- ---------------
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
--
--
-- Proof By Generalization:
-- ------------------------
--
--
-- ------------------------------
-- 1. Specialization Proposition:
-- ------------------------------
--
-- map f (ys ++ zs) = map f ys ++ map f zs
--
--
-- ------------------------------
-- 1. Generalization Proposition:
-- ------------------------------
--
-- map f (foldr (++) [] ls) = foldr ( (++) . (f `map`) ) [] ls
--
--
-- Proof By Structural Induction:
-- ------------------------------
--
--
-- 1. Induction Beginning (1. I.B.):
-- ---------------------------------
--
--
-- (Base case 1.) :<=> ls := []
--
-- => (left) := map f (foldr (++) [] ls)
-- | (Base case 1.)
-- = map f (foldr (++) [] [])
-- | foldr
-- = map f []
-- | map
-- = []
--
--
-- (right) := foldr ( (++) . (f `map`) ) [] ls
-- | (Base case 1.)
-- = foldr ( (++) . (f `map`) ) [] []
-- | foldr
-- = []
--
--
-- => (left) = (right)
--
-- ✔
--
--
-- 1. Induction Hypothesis (1. I.H.):
-- ----------------------------------
--
-- For an arbitrary but fixed (list-of-)lists "ls" and ∀ functions f,
the statement ...
--
-- map f ( foldr (++) [] ls ) = foldr ( (++) . (f `map`) ) [] ls
--
-- ... holds.
--
--
-- 1. Induction Step (1. I.S.):
-- ----------------------------
--
--
-- (left) := map f ( foldr (++) [] (l : ls) )
-- | foldr
-- = map f ( l ++ foldr (++) [] ls )
-- | (Specialized 1. I.H.)
-- = map f l ++ map f ( foldr (++) [] ls )
-- | (1. I.H.)
-- = map f l ++ ( foldr ( (++) . (f `map`) ) [] ls )
--
--
-- (right) := foldr ( (++) . (f `map`) ) [] (l : ls)
-- | foldr
-- = ( (++) . (f `map`) ) l foldr ( (++) . (f `map`) ) [] ls
-- | General rule of function application (left associativity)
-- = ( ( (++) . (f `map`) ) l ) foldr ( (++) . (f `map`)
) [] ls
-- | (.)
-- = ( (++) ( (f `map`) l ) ) foldr ( (++) . (f `map`) )
[] ls
-- | (f `map`)
-- = ( (++) (map f l) ) foldr ( (++) . (f `map`) ) [] ls
-- | General rule of function application (left associativity)
-- = (++) (map f l) ( foldr ( (++) . (f `map`) ) [] ls )
-- | ++
-- = map f l ++ ( foldr ( (++) . (f `map`) ) [] ls )
--
--
-- => (left) = (right)
--
--
-- ?■? (1. Generalization Proof)
--
--
-- (Generalization)
--
-- :<=> map f ( foldr (++) [] ls ) = foldr ( (++) . (f `map`) ) [] ls
-- | ls := [ys , zs]
-- |=> map f ( foldr (++) [] [ys , zs] ) = foldr ( (++) . (f
`map`) ) [] [ys , zs]
--
-- <=> map f (ys ++ zs) = map f ys ++ map f zs
--
-- <=>: (Specialization)
--
--
-- ■ (1. Specialization Proof)
Is this also possible? Is it allowed to use a specialized induction
hypothesis like that ( see '| (Specialized 1. I.H.)' above )?
Pascal
>
>
> On Mon, Dec 15, 2014 at 7:12 AM, Pascal Knodel <pascal.knodel at mail.com
> <mailto:pascal.knodel at mail.com>> wrote:
>
> Hi list,
>
>
> Proposition:
>
> map f (ys ++ zs) = map f ys ++ map f zs
>
> (Haskell, the craft of functional programming, exercise 11.31)
>
>
> Almost every time I'm asked to do (structural) induction over multiple
> 'things', in this example lists, I don't know how to do it.
> (I encountered similar difficulties when I worked through chapter
> 9, see
> https://github.com/pascal-knodel/haskell-craft/tree/master/Chapter%209
> ,
> ex. 9.5 ,
> https://github.com/pascal-knodel/haskell-craft/blob/master/Chapter%209/E%279%27%275.hs).
> I think my proof in this case isn't formally correct. It feels
> like it isn't.
>
> I would like to do the example with your help, so that I feel a
> little bit safer.
>
> Let's start with the base case. If I have two lists, do I select
> one, say ys := [] . Only one or one after another? Or both
> 'parallel'?
> I could state ys ++ zs := [] too, does it help?
>
> I could imagine that the proposition could be expanded to
> something like
>
> map f (l1 ++ l2 ++ ... ++ lN) = map f ys ++ map f zs
> = map f l1 ++ map f l2 ++ ... ++ map f lN
>
> And I could imagine that it is possible to do induction over more
> than two lists too.
>
> What is the reason why we can do it over two 'objects' at the same
> time?
> How do I start? Can you explain this to me?
>
>
>
> This is a right question
>
> It is somewhat a proof-version of currying
>
> What you want to prove is
>
> (∀ f,ys,zs • map f (ys ++ zs) = map f ys ++ map f zs)
>
> = "reorder the variables"
>
> (∀ ys,f,zs • map f (ys ++ zs) = map f ys ++ map f zs)
>
> = "(∀ x,y • ...) = (∀x • (∀ y • ...))"
>
> (∀ ys • (∀ f,zs • map f (ys ++ zs) = map f ys ++ map f zs))
>
> And now you can see that you want a proof of a one-variable theorem
>
> Of course at this stage you might ask "Why did you choose to pull ys
> out and not zs (or f for that matter)?"
>
> One possible answer: Experience!
>
> Another: Recursion in definitions and induction in proofs go hand in hand.
> Clearly the recursion is happening on the first list. So we may expect
> the induction to focus there
>
>
>
> Attempt:
>
> -- ---------------
> -- 1. Proposition:
> -- ---------------
> --
> -- map f (ys ++ zs) = map f ys ++ map f zs
> --
> --
> -- Proof By Structural Induction:
> -- ------------------------------
> --
> --
> -- 1. Induction Beginning (1. I.B.):
> -- ---------------------------------
> --
> --
> -- (Base case 1.) :<=> ys := []
> --
> -- => (left) := map f (ys ++ zs)
> -- | (Base case 1.)
> -- = map f ([] ++ zs)
> -- | ++
> -- = map f zs
> --
> --
> -- (right) := map f ys ++ map f zs
> -- | (Base case 1.)
> -- = map f [] ++ map f zs
> -- | map
> -- = map f zs
> --
> --
> -- => (left) = (right)
> --
> -- ✔
> --
> --
> -- 1. Induction Hypothesis (1. I.H.):
> -- ----------------------------------
> --
> -- For an arbitrary, but fixed list "ys", the statement ...
> --
> -- map f (ys ++ zs) = map f ys ++ map f zs
> --
> -- ... holds.
> --
> --
> -- 1. Induction Step (1. I.S.):
> -- ----------------------------
> --
> --
> -- (left) := map f ( (y : ys) ++ zs )
> -- | ++
> -- = map f ( y : ( ys ++ zs ) )
> -- | map
> -- = f y : map f ( ys ++ zs )
> -- | (1. I.H.)
> -- = f y : map f ys ++ map f zs
> -- | map
> -- = map f (y : ys) ++ map f zs
> --
> --
> -- (right) := map f (y : ys) ++ map f zs
> --
> --
> -- => (left) = (right)
> --
> --
> -- ?■? (1. Proof)
>
>
> But in this 'proof attempt' only "ys" was considered (1. I.H.).
> What do I miss?
>
> Pascal
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org <mailto:Beginners at haskell.org>
> http://www.haskell.org/mailman/listinfo/beginners
>
>
>
> --
> http://www.the-magus.in
> http://blog.languager.org
>
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20141218/7f5d3572/attachment-0001.html>
More information about the Beginners
mailing list