Difference between revisions of "Curry-Howard-Lambek correspondence"
Jump to navigation
Jump to search
| Line 3: | Line 3: | ||
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. | 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}} | |||
[[Category:Category Theory]] | [[Category:Category Theory]] | ||
Revision as of 15:40, 24 February 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
- ↑ 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