Proving the map function on finite lists using induction

In summary: Dick:Assuming that :: is a Haskellism for type-of, what would mean for the term "xs" is that it is a list of a's in the category of sets. The "map" is Haskell-lingo for a functor's action on arrows, and the "(\x -> x)" is Haskell-lingo for a lambda term. My hope is that this notation will help you to articulate what you're trying to prove.
  • #1
l46kok
297
0

Homework Statement



Prove by finite list induction

∀xs:: [a]. map (\x -> x) xs = xs

Homework Equations



map f [ ] = [ ]
map f (x : xs) = (f x) : map f xs


The Attempt at a Solution



The list induction principle to prove a finite lists of type a is

[P([ ])^
∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs)
=> ∀ys :: [a].P(ys)

So, to show ∀ys :: [a]. P(ys) we need to show two things
i.) P([ ])
ii.) ∀x :: a. ∀xs :: [a]. P(xs) => P(x : xs)


the i) part is really easy, it's just a base case but I am totally stomped on how to even go about proving the ii) part. I would like a guidance on this. Do I assume an arbitrary k of a newly list (that is previously constructed) and try to do an inductive proof? I don't know, I'm really lost.
 
Physics news on Phys.org
  • #2
Bump :(
 
  • #3
Did I finally break the experts here with an unsolvable question?

Bump
 
  • #4
l46kok said:
Did I finally break the experts here with an unsolvable question?

Bump

Probably not unsolvable, but I can't make heads or tails of your notation. I was hoping somebody would come along who could. So you probably have succeeded in writing something nobody understands. Is this some kind of formal logic course?? Or abstract computer science?
 
  • #5
The class is known as Advanced Discrete Structures, crosslisted with Mathematics and Computer Science. Apparently we cover topics of both formal logic and abstract computer science.

This is the notes we got from the professor. Maybe this would be of help?

http://www.mediafire.com/?jasbcwfxycy5hmk [Broken]
 
Last edited by a moderator:
  • #6
You might consider taking a look at the Haskell community or other language theoretic sites like lambda the ultimate as this is really more of a computer science/type theory question.

The following might help, you already have some of these steps but just to be explicit:
1) Write out exactly what your predicate is (P = ?).
2) Show "P []" holds.
3) Assume "[itex]\forall[/itex] xs . P xs" and show "[itex]\forall[/itex] x . P (x :: xs)".
Does this help at all?

@Dick:
My category theory is not great by any measure but List is an endofunctor over the category of sets. To my knowledge :: is a Haskellism for type-of (presumably because they used up : for the list construction function) but I imagine it could have roots that go further back.
Again I'm no expert but I think for notation "∀xs:: [a]" is universal quantification over the set produced from the functor List applied to the object "a" in the category of sets. The "map" is Haskell-lingo for a functor's action on arrows. The "(\x -> x)" is Haskell-lingo for a lambda term.
 
Last edited:
  • #7
lpjhjdh said:
Y
@Dick:
My category theory is not great by any measure but List is an endofunctor over the category of sets. To my knowledge :: is a Haskellism for type-of (presumably because they used up : for the list construction function) but I imagine it could have roots that go further back.
Again I'm no expert but I think for notation "∀xs:: [a]" is universal quantification over the set produced from the functor List applied to the object "a" in the category of sets. The "map" is Haskell-lingo for a functor's action on arrows. The "(\x -> x)" is Haskell-lingo for a lambda term.

I am more than willing to take your word for it. This is definitely not my field.
 
  • #8
Looking over what I've said I'm not sure I really addressed your question very well so I'll be a bit more specific.

All you know about the term "xs" is that it's a list of a's. We could perform case analysis and then have the two cases x:[] and x:x':xs', however we're stuck in the same situation with xs' as we were with xs. This is the intuition behind our use of induction to solve the problem. Our induction hypothesis tells us something about xs, can you state what that is?

It will also be helpful to write out what you're trying to prove in its full form. What is P (x:xs)?
 
Last edited:

What is induction proof on list?

Induction proof on list is a method used in mathematics to prove the validity of a statement for all elements in a list or sequence.

How does induction proof on list work?

Induction proof on list involves breaking down the statement into smaller cases and proving that it holds true for the first case, then assuming it holds true for the next case and proving it for the next case, and so on until the statement is proven for all elements in the list.

What is the basis step in induction proof on list?

The basis step in induction proof on list is the first element or case in the list, for which the statement is directly proven to be true without any assumptions.

What is the inductive step in induction proof on list?

The inductive step in induction proof on list is when we assume that the statement holds true for the n-th case, and then use this assumption to prove that it also holds true for the (n+1)-th case.

Why is induction proof on list important?

Induction proof on list is important because it allows us to prove the validity of a statement for an infinite list or sequence of elements, without having to prove it individually for each element. This makes it a powerful tool in mathematical reasoning and problem solving.

Similar threads

  • Calculus and Beyond Homework Help
Replies
1
Views
458
  • Calculus and Beyond Homework Help
Replies
6
Views
871
  • Calculus and Beyond Homework Help
Replies
1
Views
1K
  • Calculus and Beyond Homework Help
Replies
6
Views
983
  • Calculus and Beyond Homework Help
Replies
1
Views
902
  • Calculus and Beyond Homework Help
Replies
3
Views
1K
  • Calculus and Beyond Homework Help
Replies
1
Views
1K
  • Calculus and Beyond Homework Help
Replies
9
Views
1K
  • Calculus and Beyond Homework Help
Replies
2
Views
1K
  • Calculus and Beyond Homework Help
Replies
5
Views
2K
Back
Top