haskell - 指称语义映射是可判定的吗？

Question

为我对这个问题的糟糕表达道歉，我不确定我是否有足够的词汇来恰本地提出这个问题。

我写了(最近)类似的东西

⟦let x = x in x⟧ = ⊥

但实际上我在这里无法理解一些棘手的事情。我可以断言这句话是真的 ⊥因为我知道这是一个非生产性的无限循环。此外，我可以断言类似

⟦let ones = 1:ones in ones⟧ = μ(λx.(1,x)) = (1, (1, (1, ... )))

但是省略号的内容是什么？大概它是无限数量的“1-and-tuples”，如果您对 AFA 没问题，这是一个完美定义的数学对象，但我怎么能让您相信它不是有限数量的“1-and-tuples”然后是非生产性 ⊥ ?

显然，这涉及回答停止问题，所以我一般不能。

那么在这种情况下，我们如何计算语义映射，就好像它们是一个全函数一样？图灵不完全语言的语义是否一定是非确定性的？我想这意味着语义永远只是对语言的一种近似的、非正式的描述，但是这个“洞”会更进一步吗？

Answer 1

没有图灵完备语言的集合理论模型。如果您的语言正在强烈规范化，则存在一个总功能来“解释”某些东西。您可能已经或可能没有在非图灵完整语言中设置理论语义。无论如何，图灵完备和非图灵完备的语言都可以具有非集合论语义和全语义映射函数。

我不认为这是这里的问题。

归纳和共归纳定义之间存在差异。我们可以从理论上探索这个集合:

整数列表的归纳定义如下:

the set [Z] is the smallest set S such that the empty list is in S , and such that for any ls in S and n in Z the pair (n,ls) in S.

这也可以以“步骤索引”的方式呈现为 [Z](0) = {[]}和 [Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)}它允许您定义 [Z] = \Union_{i \in N}([Z](n) (如果你相信自然数!)

另一方面，Haskell 中的“列表”与“互感流”更密切相关，后者是互感定义的

the set [Z] (coinductive) is the largest set S such that forall x in S, x = [] or x = (n,ls) with n in Z and ls in S.

也就是说，共归纳定义是倒退的。归纳定义定义了包含某些元素的最小集合，而协约定义定义了所有元素都采用某种形式的最大集合。

很容易证明所有归纳列表的长度都是有限的，而一些归纳列表是无限长的。您的示例需要共同归纳。

更一般地，归纳定义可以被认为是“仿函数的最小固定点”，而协约定义可以被认为是“仿函数的最大固定点”。仿函数的“最小固定点”只是它的“初始代数”，而“最大固定点”是它的“最终代数”。使用它作为您的语义工具可以更轻松地在集合类别之外的类别中定义事物。

我发现 Haskell 提供了一种很好的语言来描述这些仿函数

data ListGenerator a r = Cons a r | Nil

instance Functor (ListGenerator a) where
  fmap f (Cons a x) = Cons a (f x)
  fmap _ Nil        = Nil

尽管 haskell 提供了一种很好的语言来描述这些仿函数，因为它的函数空间是 CBN 并且语言不是全部的，我们无法定义我们想要的最小不动点类型 :( 虽然我们确实得到了最大固定点

data GF f = GF (f (GF f))

或存在量化的非递归

data GF f = forall r. GF r (r -> (f r))

如果我们使用严格或完整的语言工作，那么最少的固定点将是普遍量化的

data LF f = LF (forall r. (f r -> r) -> r)

编辑:因为“最小”是一个集合理论概念，尽管“最小”/“最大”的区别可能不是正确的。 LF的定义与 GF 基本同构是“自由初始代数”，它是“最小不动点”的分类形式。

至于

how can I convince you that it's not some finite number of "1-and-tuples" and then a non-productive ⊥?

你不能，除非我相信这篇文章中的那种结构。如果我这样做了，那么你的定义让我陷入困境!如果你说“ ones 是由 (1,ones) 对组成的互感流”，那么我必须相信!我知道 ones不是 _|_根据定义，因此通过归纳，我可以证明对于任何值 n 都不可能是这种情况我有 n一个，然后是底部。我可以尝试否认你的说法，只是否认共感应 Steam 的存在。