J. *_*son 12 haskell formal-semantics
对于我对这个问题的不良表达表示歉意,我不确定我是否有适当的词汇量.
我写了(最近)类似的东西
?let x = x in x? = ?
但是我真的没有理解这里棘手的事情.我可以断言这句话是真的,? 因为我知道这是一个非生产性的无限循环.此外,我可以断言像
?let ones = 1:ones in ones? = ?(?x.(1,x)) = (1, (1, (1, ... )))
但是什么进入了省略？据推测,它是无限数量的"一元组",如果你对AFA没问题,这是一个非常明确的数学对象,但我怎么能说服你,它不是一些有限数量的"一元组"然后是非生产性的?？
显然,这涉及到解决停止问题,所以我不能一般.
那么在这种情况下,我们如何计算语义映射,就像它们是一个完整的函数一样？对于图灵不完整的语言,语义必然是不确定的吗？我想这意味着语义总是只是一种语言的近似,非正式的描述,但这个"洞"是否会更进一步？
没有完整语言的集合理论模型.如果你的语言正在强烈规范化,那么就会有一个完整的功能来"解释"它.您可能已经或可能没有用非图灵完整语言设置理论语义.无论如何,图灵完整,非图灵完整,语言可以具有非集合理论语义和全部语义映射函数.
我认为这不是问题所在.
归纳和归纳定义之间存在差异.我们可以从理论上探索这个集合:
整数列表的归纳定义如下:
设定
[Z]为最小的集合S,使得所述空列表是在S,并使得对于任何ls在S和n在Z该对(n,ls)中S.
这也可以以"步骤索引"的方式呈现,[Z](0) = {[]}并[Z](n) = {(n,ls) | n \in Z, ls \in [Z](n-1)}允许您定义[Z] = \Union_{i \in N}([Z](n)(如果您相信自然数!)
另一方面,Haskell中的"列表"与"coinductive streams"更密切相关,"coinductive streams"是由coinductively定义的
集合
[Z](coinductive)是最大的集合S,使得forallxinS,x = []或x = (n,ls)withninZ和lsinS.
也就是说,同性恋的定义是倒退的.虽然归纳定义定义了包含一些元素的最小集合,但是同感定义定义了所有元素采用某种形式的最大集合.
很容易证明所有归纳列表都有有限的长度,而一些同源列表是无限长的.你的例子需要共同诱导.
更一般地说,归纳定义可以作为"仿函数"的"最小定点",而同构定义可以被认为是"仿函数的最大定点".仿函数的"最小修正点"只是它的"初始代数"而"最大修正点"是它的"最终代数".使用它作为语义工具可以更容易地在类别集之外的类别中定义事物.
我发现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是由这对组成的coinductive流(1,ones)"那么我必须相信!我知道ones不是_|_根据定义,因此通过归纳我可以证明,对于任何价值而言,n我都不能是这样,n然后是底部.我可以试图否认你的主张只是否认存在共同描述的蒸汽.