Decomposing Typed Lambda Calculus into a Couple of Categorical Programming Languages
Decomposing Typed Lambda Calculus into a Couple of Categorical Programming Languages
复制标题
将类型化 Lambda 演算分解为几种分类编程语言
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Masahito Hasegawa
中科院分区：
文献类型：
--
作者：
Masahito Hasegawa
我们给出了两种具有可变箭头和相关抽象/归约机制的范畴编程语言，这扩展了范畴编程在实践中的可能性[Hag 87，CF 92]。这些语言是互补的-其中一个提供一阶编程风格，而另一个提供高阶编程风格-并且是简单类型lambda演算的“孩子”，因为我们可以将类型lambda演算分解为它们，相反，它们的组合等价于类型lambda演算。这种分解是对C语言的类型化lambda演算进行语义分析的结果。赫米达和B。Jacobs [HJ94].
We give two categorical programming languages with variable arrows and associated abstraction/reduction mechanisms, which extend the possibility of categorical programming [Hag87, CF92] in practice. These languages are complementary to each other — one of them provides a first-order programming style whereas the other does higher-order — and are “children” of the simply typed lambda calculus in the sense that we can decompose typed lambda calculus into them and, conversely, the combination of them is equivalent to typed lambda calculus. This decomposition is a consequence of a semantic analysis on typed lambda calculus due to C. Hermida and B. Jacobs [HJ94].