Categorical Model of Functional Language with Natural Numbers and Boolean Values

摘要

Curry–Howard–Lambek isomorphism defines a correspondence between at first sight different theories: Church's computational calculi (which is the foundation of functional programming paradigm), intuitionistic logic, and category theory. In this paper, we focus on the correspondence between the last two theories. We define a simple functional language, and we model it by category theory. We describe a correspondence between language in a motivating example of an evaluation of a simple functional program.