Curry-Howard對應

出自維基百科,自由嘅百科全書

程式語言論證明論入面,Curry-Howard對應粵拼koe1 ri1 haau1 woet1 deoi3 jing3,亦稱Curry-Howard同構;英文:Curry-Howard correspondence;華文:柯里-霍華德對應)就係講緊電腦程式同埋數學證明之間嘅直接關連。

佢係generalize咗形式邏輯系統(formal logic)同公式計算(computational calculus)之間嘅關連,係由發現美國數學家Haskell Curry同埋邏輯師William Alvin Howard嘅。 邏輯同運算呢個𪐀褦先至係Curry同Howard嘅貢獻,其他嘅同直觀主義邏輯(institutional logic)有關嘅operational interpretation(睇Brouwer-Heyting-Kolmogorov演繹同埋可實現性)。呢個𪐀褦亦都可以延伸去同包埋範疇論(category theory),噉就而形成Curry-Howard-Lambek對應嘞。