表达式的含义映射是否可判定？

Question

表达式的含义映射是否可判定？

12

对于我表达这个问题不好，我不确定我有适当的词汇来询问。

我最近写了类似于以下内容的东西：

⟦let x = x in x⟧ = ⊥

但是我确实没有理解这里的一些棘手之处。我可以断言这个语句真正的结果是⊥，因为我知道它是一个非生产无限循环。此外，我可以做出如下断言

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

那么，这个省略号代表了什么？假设它代表了无限数量的“1元组”，如果你对AFA没问题的话，那么这是一个完全定义良好的数学对象。但我如何说服你它不是有限数量的“1元组”，然后是一个非生产的⊥？

显然，这涉及到回答停机问题，所以一般情况下我不能回答。

那么，在这种情况下，我们如何计算语义映射，就好像它们是一个完全函数一样？对于图灵不完备语言，语义是否必须是非确定性的？我想这意味着语义始终只是一个关于语言的近似、非正式描述，但这个“漏洞”是否还有更深层次的东西？

- J. Abrahamson

略微评论一下...在你的第二个例子中，应该是$\nu$而不是$\mu$。(你正在取最大不动点，在Haskell中就是这样做的。) - Kristopher Micinski

1

你可能会对我之前在 Twitter 争论期间构建的这个程序感兴趣：https://gist.github.com/luqui/1379703 -- 它是一个 Haskell 值，因此不知道它是否表示 ⊥。 - luqui

2个回答

2

想了解更多有关共归结构证明技术的内容（扩展Philip JF非常好的回答），可以参考Hinze和James的论文“证明唯一不动点原理的正确性”：http://www.cs.ox.ac.uk/people/daniel.james/unique/unique-tech.pdf

- sclv

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Philip JF · Accepted Answer

图灵完备语言没有集合论模型。如果您的语言是强归一化的，则存在一个总函数将其“解释”为其他内容。非图灵完备语言可能具有非集合论语义。无论如何，无论是图灵完备还是非图灵完备的语言都可以具有具有总语义映射函数的非集合论语义。

我认为这里的问题不在于此。

归纳定义和余归纳定义之间有区别。我们可以从集合论角度探讨这个问题：

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

- 集合[Z]是包含空列表的最小集合S，并且对于任意在S中的ls和Z中的n，对偶(n, ls)也在S中。

这也可以以“步骤索引”的方式呈现，例如[Z](0)={[]}和[Z](n)= {(n,ls)| n∈Z, ls∈[Z](n−1)}，从而定义[Z]=\Union_{i \in N}([Z](n))（如果您相信自然数！）

另一方面，在Haskell中，“列表”更接近于“余归纳流”，其定义为：

- 集合[Z]（余归纳）是包含所有元素的最大集合S，其中对于S中的每个x，x=[]或x=(n,ls)，其中n∈Z，ls∈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 同构，并且是“自由初始代数”，这是“最小不动点”的范畴形式化。

至于：

我怎样才能说服你，它不是一些“1元组”的有限数量，然后是一个非生产的 ⊥？

除非我相信此帖子中的构造类型，否则您无法说服我。如果我这么做，那么您的定义将使我陷入困境！如果您说“ones 是由配对 (1,ones) 组成的共归纳流”，那么我必须相信！根据定义，我知道 ones 不是 _|_，因此通过归纳法，我可以证明任何值 n 都不可能是 n 个“1”然后是底部。我只能否认共归纳流的存在来否认您的主张。