类型理论中"无终止实现"定位的含义和相关性

Question

在讨论哈斯克尔的背景下 https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, ，有人告诉我

多态类型没有终止实现 $(e o a) o a$

我们不能有一个类型的函数 $((e o a) o a) o e$ 或类型的函数 $(r o x) o x$, ，因为这些不会是"可实施的"。

这些类型在STLC中形成良好，因为我们可以使用类型形成规则来构建它们。而且我不明白为什么我们不能形成这种形状的lambda术语，例如 lambda\lambda c_{((a o t) o t)}。\,b_a$, ，或 lambda\lambda p_{e o a}。\,b_a$.

因此，问题是什么？具体来说，什么是STLC上下文中的"终止实现"？我相信这与以下事实有关： $(e o\bot) o\bot$ 不是建设性地等同于 $e$, ，但如果有人能为我阐明这一点，我将不胜感激。

Answer 1

你可以 永远如此 通过一个自由变量来定义一个类型:类型 $\头$ 由自由变量居住 $x_ au$.当人们谈论一种类型的"实现"时，他们的意思是 关闭期限, ，即一个没有自由变量。你给出的例子包含自由变量，即 ＜b_a＞.

在 纯 简单类型 $\lambda$-微积分所有术语都是"终止"，因为微积分是强烈归一化的，所以无论你采取什么减少，它们总是会导致（独特的）正常形式。

在 $\lambda$-微积分扩展与递归定义（如Haskell）我们可以居住在每一种类型 $\头$ 使用封闭项，例如在Haskell中，类型 t 居住在 a 定义为

a :: t
a = a

一旦我们有了递归定义，就很容易编写不终止（或没有正常形式）的封闭术语。