{"id":59,"date":"2008-01-01T12:35:04","date_gmt":"2008-01-01T19:35:04","guid":{"rendered":"http:\/\/www.elbeno.com\/haskell_soe_blog\/?p=59"},"modified":"2008-01-08T10:09:50","modified_gmt":"2008-01-08T18:09:50","slug":"exercise-111","status":"publish","type":"post","link":"https:\/\/www.elbeno.com\/haskell_soe_blog\/?p=59","title":{"rendered":"Exercise 11.1"},"content":{"rendered":"<p>1) Prove that <tt>(\u00e2\u02c6\u20accs | cs is finite) putCharList cs = map putChar cs<\/tt><\/p>\n<p>where<\/p>\n<pre lang=\"haskell\">putCharList [] = []\r\nputCharList (c:cs) = putChar c : putCharList cs\r\n\r\nmap f [] = []\r\nmap f (x:xs) = f x : map f xs<\/pre>\n<p>Base case:<\/p>\n<pre lang=\"haskell\">putCharList []\r\n  => []\r\n  => map putChar []<\/pre>\n<p>Inductive Step:<\/p>\n<p>assume that <tt>purCharList cs = map putChar cs<\/tt><\/p>\n<p>then<\/p>\n<pre lang=\"haskell\">putCharList (c:cs)\r\n  => putChar c : putCharList cs\r\n  => putChar c : map putChar cs\r\n  => map putChar (c:cs)<\/pre>\n<p>QED.<\/p>\n<p>2) Prove that <tt>(\u00e2\u02c6\u20acxs | xs is finite) listProd xs = fold (*) 1 xs<\/tt><\/p>\n<p>where<\/p>\n<pre lang=\"haskell\">listProd [] = 1\r\nlistProd (x:xs) = x * listProd xs\r\n\r\nfold op init [] = init\r\nfold op init (x:xs) = x `op` fold op init xs<\/pre>\n<p>Base case:<\/p>\n<pre lang=\"haskell\">listProd []\r\n  => 1\r\n  => fold (*) 1 []<\/pre>\n<p>Inductive Step:<\/p>\n<p>assume that <tt>listProd xs = fold (*) 1 xs<\/tt><\/p>\n<p>then<\/p>\n<pre lang=\"haskell\">listProd (x:xs)\r\n  => x * listProd xs\r\n  => x * fold (*) 1 xs\r\n  => fold (*) 1 (x:xs)<\/pre>\n<p>QED.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>1) Prove that (\u00e2\u02c6\u20accs | cs is finite) putCharList cs = map putChar cs where putCharList [] = [] putCharList (c:cs) = putChar c : putCharList cs map f [] = [] map f (x:xs) = f x : map f xs Base case: putCharList [] => [] => map putChar [] Inductive Step: assume [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/59"}],"collection":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=59"}],"version-history":[{"count":0,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/59\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=59"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=59"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=59"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}