tbo*_*hev 12 haskell formal-semantics denotational-semantics
我对指称语义的概念有点困惑.据我所知,指称语义应该描述函数和表达式如何在特定的编程语言中工作.用于描述这些功能以及它们如何工作的正确形式究竟是什么？究竟什么是"域",以及如何构建映射函数？
举个例子,"做Y同时Y"的映射函数是什么？
我一直在网上阅读大量资料,但这很难理解.这些描述是否类似于无上下文语法？
请让我知道,谢谢!
J. *_*son 20
将表示视为从语法到"意义"的映射.您可能会看到它用双括号写成,因此您会将其读[[3]] = 3作"语法的表示[数字3]是数字3".
算术就是一个简单的例子.通常你有一个类似的外延
[[x + y]] = [[x]] + [[y]]
其中+左边是一个语法加和+右边的算术加.为了更清楚,我们可能会改为lispy语法.
[[(+ x y)]] = [[x]] + [[y]]
现在一个非常重要的问题是这个映射的范围(codomain)是什么？到目前为止,我一直认为将其视为"数字和加法生活的一些肮脏的域名"已经足够了,但这可能是不够的.重要的是,您的示例将快速打破它.
[[do X while True]] = ???
因为我们不一定有一个包含非终止概念的mathy域名.
在Haskell中,这可以通过将数学域称为"提升"域或CPO域来解决,该域实质上直接添加非终止.例如,如果您未提升域是整数I,则解除域? + I,其中?被称为"底部",它指未结束.
这意味着我们可能会写(在Haskell语法中)
[[let omega = 1 + omega in omega]] = ?
繁荣.我们有意义 - 无限循环的意义是......什么都没有!
在Haskell中提升域的技巧是因为Haskell是懒惰的(非严格的),所以可能有数据类型的有趣交互?.例如,如果我们有type IntList = Cons Int IntList | Nil提升域直接IntList包括?(一个完整的无限循环)以及Cons ? ?仍未完全解析的东西,但提供的信息比普通的旧?.
我刻意写了"更多信息".CPO形成"定义"的部分订单(即PO).?是最大的未定义,所以它<=是CPO中的任何其他内容.然后你会得到像Cons ? ? <= Cons 3 ?你的部分顺序形成链的东西.你经常说,如果x <= y那时" y包含的信息多于x"或" y比x" 更明确".
对我来说,最重要的一点是,通过在我们的表示域中定义这个CPO结构,我们可以非常准确地谈论严格和非严格评估之间的差异.在严格的语言中(或者实际上,在您的语言可能或可能没有的某些严格的域中),您的CPO都是"平坦的",因为您要么具有完全定义的结果,要么?没有别的.当您的CPO不平坦时,就会发生懒惰.
另一个重点是"你不能在底部进行模式匹配"这一概念......如果我们将底部视为一个无限循环(尽管使用这个新的抽象模型,它并不一定意味着......它例如,可能是一个段错误)然后这句格言只不过是表达停顿问题的另一种方式.结果是,如果那样的x <= y话,所有明智的功能必须是"单调的" f x <= f y.如果你花费一些时间来处理这个概念,你会发现它会使那些具有不同非底层行为的函数无论它们的参数是否为底.例如,停止神谕是非单调的
halting (?) = False -- we can't pattern match on bottom!
halting _ = True
但是"破碎的神谕"是
hahahalting (?) = ? -- we're still pattern matching,
-- but at least the behavior is right
hahahalting _ = True
我们用它写的 seq
hahahalting x = x `seq` True -- valid Haskell
这也使Haskell的非单调函数的危险性大大spoon减轻.我们可以通过利用表面上不合理的异常捕获来编写它们......但如果我们不小心它会导致非常不稳定的行为.
你可以从指称语义中学到更多东西,所以我将提供Edward Z. Yang关于指称语义的注释.