Difference between revisions of "Curry-Howard correspondence"
Jump to navigation
Jump to search
| Line 2: | Line 2: | ||
[[Category:Meta Mathematics]] | [[Category:Meta Mathematics]] | ||
[[Category:Logic]] | |||
[[Category:Arithmetic]] | |||
[[Category:Compiler]] | |||
[[Category:Testing]] | |||
Revision as of 08:00, 4 February 2022
Curry-Howard correspondence(Q975734) is the isomorphic mapping between arithmetic calculation and logical proofs. This means that any arithmetic calculation can be one-to-one uniquely mapped to a logical operation sequence. This has been extended to Category Theory, meaning that all logical structures and arithemtic numbering system can be mapped to topolgical structures represented in the language of arrows. This is also known as Curry-Howard-Lambek correspondence