{"id":10479,"date":"2015-01-13T11:59:15","date_gmt":"2015-01-13T16:59:15","guid":{"rendered":"http:\/\/mjtsai.com\/blog\/?p=10479"},"modified":"2015-01-24T11:47:34","modified_gmt":"2015-01-24T16:47:34","slug":"proof-in-functions","status":"publish","type":"post","link":"https:\/\/mjtsai.com\/blog\/2015\/01\/13\/proof-in-functions\/","title":{"rendered":"Proof in Functions"},"content":{"rendered":"<p><a href=\"http:\/\/www.fewbutripe.com\/swift\/math\/2015\/01\/06\/proof-in-functions.html\">Brandon Williams<\/a> (<a href=\"https:\/\/twitter.com\/mbrandonw\/status\/552493185982013441\">tweet<\/a>):<\/p>\n<blockquote cite=\"http:\/\/www.fewbutripe.com\/swift\/math\/2015\/01\/06\/proof-in-functions.html\">\n<p>Swift&rsquo;s generic functions allow us to explore a beautiful idea that straddles the line between mathematics and computer science. If you write down and implement a function using only generic data types, there is a corresponding mathematical theorem that you have proven true. There are a lot of pieces to that statement, but by the end of this short article you will understand what that means, and we will have constructed a computer proof of De Morgan&rsquo;s law.<\/p>\n<p>[&#8230;]<\/p>\n<p>The rigorous statement of the relationship we have been grasping at is known as the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Curry%E2%80%93Howard_correspondence\">Curry-Howard correspondence<\/a>, first observed by the mathematician Haskell Curry in 1934 and later finished by logician William Howard in 1969. It sets up a kind of dictionary mapping terms in the computer science world to terms in the mathematics world.<\/p>\n<\/blockquote>\n<p>Update (2015-01-24): <a href=\"http:\/\/www.fewbutripe.com\/swift\/math\/2015\/01\/13\/solutions-to-proof-in-functions.html\">[Solutions to Exercises] &ldquo;Proof in Functions&rdquo;<\/a>.<\/p>","protected":false},"excerpt":{"rendered":"<p>Brandon Williams (tweet): Swift&rsquo;s generic functions allow us to explore a beautiful idea that straddles the line between mathematics and computer science. If you write down and implement a function using only generic data types, there is a corresponding mathematical theorem that you have proven true. There are a lot of pieces to that statement, [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"apple_news_api_created_at":"","apple_news_api_id":"","apple_news_api_modified_at":"","apple_news_api_revision":"","apple_news_api_share_url":"","apple_news_coverimage":0,"apple_news_coverimage_caption":"","apple_news_is_hidden":false,"apple_news_is_paid":false,"apple_news_is_preview":false,"apple_news_is_sponsored":false,"apple_news_maturity_rating":"","apple_news_metadata":"\"\"","apple_news_pullquote":"","apple_news_pullquote_position":"","apple_news_slug":"","apple_news_sections":"\"\"","apple_news_suppress_video_url":false,"apple_news_use_image_component":false,"footnotes":""},"categories":[4],"tags":[263,46,259,71,901],"class_list":["post-10479","post","type-post","status-publish","format-standard","hentry","category-programming-category","tag-theory","tag-languagedesign","tag-math","tag-programming","tag-swift-programming-language"],"apple_news_notices":[],"_links":{"self":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/10479","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/comments?post=10479"}],"version-history":[{"count":2,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/10479\/revisions"}],"predecessor-version":[{"id":10576,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/posts\/10479\/revisions\/10576"}],"wp:attachment":[{"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/media?parent=10479"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/categories?post=10479"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mjtsai.com\/blog\/wp-json\/wp\/v2\/tags?post=10479"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}