Difference between revisions of "Curry-Howard-Lambek correspondence"

From PKC
Jump to navigation Jump to search
 
(4 intermediate revisions by the same user not shown)
Line 6: Line 6:
Think about the following diagram and related it to Curry-Howard-Lambek correspondence.
Think about the following diagram and related it to Curry-Howard-Lambek correspondence.
{{:Hermeneutic Circle}}
{{: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>


[[Category:Category Theory]]
 
[[Category:Meta Mathematics]]
{{#ask: [[Authored by::Joachim Lambek]]
[[Category:Logic]]
|format=table
[[Category:Arithmetic]]
|mainLabel=Content Link
[[Category:Compiler]]
}}
[[Category:Testing]]
 
[[Category:Hermeneutics]]
<noinclude>
[[Category:Hermeneutic Circle]]
 
{{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]:

  1. Configuration
  2. Refiguration
  3. Prefiguration
HermeneuticalCircle.png


An Anectodal Reference

Bob Coecke talking about his encounter with Lambeck[2]. He later developed a python library for NLP called:lambeq[3]


Content Link


References

  1. 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
  2. Coecke, Bob (Feb 24, 2022). Bob Coecke: Compositional Intelligence. local page: Topos Institute. 
  3. Coecke, Bob (Oct 8, 2021). lambeq: An Efficient High-Level Python Library for Quantum NLP. local page: arXiv. 

Related Pages