Difference between revisions of "Curry-Howard-Lambek correspondence"
| (8 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{WikiEntry|key=Curry-Howard-Lambek correspondence|qCode=110810925}} | {{WikiEntry|key=Curry-Howard-Lambek correspondence|qCode=110810925}} is an extension of [[Curry-Howard correspondence]]. | ||
By thinking about the correspondence between Proof, Programs, and Categories, we can see a circular triangle of data types that mutually serves and the Test Assertions, Proposed Programs, and Data Content in [[ordered relation]]s, as a self-sufficient environment for software verification and validation cycle. | |||
[[ | =Analogies in other fields= | ||
[ | Think about the following diagram and related it to Curry-Howard-Lambek correspondence. | ||
[[ | {{:Hermeneutic Circle}} | ||
[[ | =An Anectodal Reference= | ||
[[ | [[Bob Coecke]] talking about [https://youtu.be/03ZPDyj8TtM?t=822 his encounter with Lambeck]<ref>{{:Video/Compositional Intelligence}}</ref>. He later developed a python library for [[NLP]] called:[[lambeq]]<ref>{{:Paper/lambeq: An Efficient High-Level Python Library for Quantum NLP}}</ref> | ||
{{#ask: [[Authored by::Joachim Lambek]] | |||
|format=table | |||
|mainLabel=Content Link | |||
}} | |||
<noinclude> | |||
{{PagePostfix | |||
|category_csd=Correspondence,Category Theory,Logic,Grammer,Meta Mathematics,Arithmetic,Compiler,Testing,Hermeneutics | |||
}} | |||
</noinclude> | |||
Latest revision as of 04:04, 4 August 2022
Curry-Howard-Lambek correspondence(Q110810925) is an extension of Curry-Howard correspondence.
By thinking about the correspondence between Proof, Programs, and Categories, we can see a circular triangle of data types that mutually serves and the Test Assertions, Proposed Programs, and Data Content in ordered relations, as a self-sufficient environment for software verification and validation cycle.
Analogies in other fields
Think about the following diagram and related it to Curry-Howard-Lambek correspondence.
Hermeneutic circle(Q1570095) is the recursive structure that represent the iterative nature of interpretation.
Note the three stages in the following diagram[1]:
- Configuration
- Refiguration
- Prefiguration
An Anectodal Reference
Bob Coecke talking about his encounter with Lambeck[2]. He later developed a python library for NLP called:lambeq[3]
References
- ↑ Sangster, Alan (2021). "The Life and Works of Luca Pacioli (1446/7–1517), Humanist Educator". Abacus: A Journal of Accounting, Finance and Business Studies. local page: University of Sydney. 57. , Figure 2
- ↑ Coecke, Bob (Feb 24, 2022). Bob Coecke: Compositional Intelligence. local page: Topos Institute.
- ↑ Coecke, Bob (Oct 8, 2021). lambeq: An Efficient High-Level Python Library for Quantum NLP. local page: arXiv.
Related Pages