问题标签 [denotational-semantics]

我的意思是，从定义来看：

fix f是函数的最小不动点f

换句话说：

最小的定义x使得f x = x.

任何空值类型的最少定义值是undefined。这里仍然存在一些歧义，undefined可能意味着“将引发错误”（更好）或“永远不会终止”（更糟）。正如推理和试验所表明的那样，fix (+1)两者fix pred :: Word似乎都从未接近终止（即使pred 0是一个错误），所以“永不终止”中最糟糕的一个很可能总是在这两种选择之间被选择。（能逃脱fix的就是无聊const 1，以后再说吧。）

这不是有用的申请方式fix。

有用的应用方式fix是：

-- 即使用fix来神奇地产生一个递归函数。（这总是让我感到惊讶。）这可以被视为在 2 个函数之间进行选择：\f x -> f (x - 1)和\_ x -> x，其中一个永远不会评估其第一个绑定变量。这是一个危险的玩具，因为我们仍然可以很容易地获得一个在其一半域内不终止的函数，就像意外翻转>到<或-to一样容易+。

所以，不知何故，这两个功能：

-- 后者是“最少定义的”。如果我们用力眯起眼睛，我们实际上可以认出我们无聊的家伙const，只是flip'd。

现在，这是违反直觉的。f2实际上更具容错性，因此从某种意义上说，它被定义为比f1. （特别是，这是让它逃脱否则无限循环的原因fix）。具体来说，f2为所有相同(f, x)的输入对定义为f1加上(undefined, x). 同样，const 1是所有一元函数中容错能力最强的。

那么，我现在如何理解定义性？

这个问题的一些理由

附近有这个答案fix，它提供了与这个问题中提出的不同的直觉。它还强调，为了全面理解，必须通过关于指称语义的外部教程。

我想得到一个答案，要么支持，要么解释这里提出的直觉的错误，而且，如果领域理论真的是评论中提出的草书顺序的背后，至少包括一些经验法则，允许，不管多么有限，但领域理论的实际应用。我希望看到的问题的一个特定部分是一个有fix能力的函数是否总是可以分解为一个常量函数和一个归约函数，以及这些函数类的定义是什么。

我的愿望是在可靠的数学推理的支持下，就构建有用且安全fix的编码递归提供一个实际的、实用的答案。

我想写一个haskell程序来实现一种基于其指称语义的简单命令式语言。我在 Windows 上使用 GHCi，版本 8.4.2。我在实现下面描述的函数和过程抽象时遇到了一些问题。

让我描述一下。我称之为 IMP。首先，我定义了抽象语法。IMP 只接受整数。和标识符将是字符串。

简要说明：在 Command 中，Skip 什么都不做。分配会将表达式的值赋予标识。Letin 将在命令中声明一些变量。Cmdcmd 将依次运行 2 个命令。ifthen 是条件命令，如果第一个表达式被评估为真，则运行第一个命令，否则运行第二个命令。Whiledo 是循环。IdentifierC ( ActualParameter )：IdentifierC 表示本地环境中的某些功能。这个 ActualParameter 是一些带有一些值的表达式。这个命令只是在指定的值上调用这个函数。

在Expression中，从上到下依次是： numeric bool false bool true negate of expression 从本地环境中获取Ident的值。sum 2 个表达式减去 2 个表达式的乘积 2 < 在表达式中声明某个变量 IdentifierE ( ActualParameter ) IdentifierE 表示本地环境中的某个函数。这个 ActualParameter 是一些带有一些值的表达式。这个命令只是在指定的值上调用这个函数。最后得到一个新值作为这个表达式的结果。

然后是语义域

我的代码在这里：https ://github.com/sanyuwen/IMP/blob/master/DSemImp.hs 。我的测试代码在这里：https ://github.com/sanyuwen/IMP/blob/master/ImpTest.hs

当我使用 GHC 导入 DSemImp 模块时，我遇到了很多错误。

考虑以下包装器：

我想反驳（作为围绕这个有趣帖子的练习）存在一个合法Functor F实例，它允许我们将Int -> Int类型函数应用于实际内容并〜忽略〜所有其他函数（即fmap nonIntInt = id）。

我相信这应该用一个自由定理来完成（我在这里fmap读到）： 对于给定的 ,和,这样: ,给定构造函数的自然映射在哪里。fghkg . f = k . h$map g . fmap f = fmap k . $map h$map

什么定义了自然地图？我是否正确地假设它是一个简单flip const的 for F？

据我所知：$map f是我们Ff在范畴论中所指的。因此，从分类的意义上说，我们只是想要下图中的一些东西来通勤：

然而，我不知道用什么代替???s （也就是说，我们应用什么函子来得到这样的图，我们如何表示这个几乎fmap-？）。

那么，一般来说，什么是自然地图F？的自由定理的正确图是什么fmap？

我要去哪里？

考虑：

很容易看出f . g是h . k。然而，不存在的fmap只会执行，而f不是k，给出不同的结果。如果我对自然性的直觉是正确的，那么这样的证明就会奏效。这就是我想要弄清楚的。

@leftaroundabout提出了一个更简单的证明：fmap show . fmap (+1)改变内容，不像fmap $ show . (+1). 这是一个很好的证明，但我仍然想将自由定理作为练习。

Edward Kmett 的这篇 Reddit 帖子提供了自然地图的建设性定义，它来自自由定理（fmap我在另一篇Edward Kmett 的帖子中读到）：

对于给定f的 ,和g,这样: , 其中是给定构造函数的自然映射。hkf . g = h . k$map f . fmap g = fmap h . $map k$map

我不完全理解算法。让我们一步一步地接近它：

我们可以通过对您给出的任何特定具体选择的归纳来定义“自然地图” 。F最终，任何这样的 ADT 都是由 sum、products、(->)'s、1s、0s、a's、其他仿函数的调用等组成的。

考虑：

没有箭头。让我们看看fmap（我认为这是任何没有 s 的 ADT 的自然选择(->)）在这里如何操作：

这看起来很自然。更正式地说，我们适用xy于 every x，适用fmap xy于 every T x，其中Ta Functor，我们保持每个单元不变，然后将 every 传递Void给absurd。这也适用于递归定义！

对于非归纳类型：（_{链接帖子下此答案的详细说明。）}

这部分很清楚。

当我们允许时，(->)我们现在有了第一个混合方差的东西。的左侧类型参数(->)处于逆变位置，右侧处于协变位置。因此，您需要通过整个 ADT 跟踪最终类型变量，并查看它是否出现在正和/或负位置。

现在我们包括(->)s。让我们尝试继续进行这种归纳：

我们以某种方式推导出和的自然映射。因此，我们要考虑以下几点：T aS a

我相信这是我们开始选择的起点。我们有以下选择：

• （幻影） a既不在T也不在S。ainT2S是幻像，因此，我们可以同时实现fmap和contramapasconst phantom。
• （协变） a出现在S a和不出现在 中T a。因此，这在ReaderTwith S a（实际上并不依赖于a）作为环境的行中，它?Class?用Functor、?map?with fmap、???、??with代替xy：
• （逆变） a出现在T a，不出S a。我看不到让这个东西成为协变函子的方法，所以我们Contravariant在这里实现一个实例，它?map?用contramap、??withyx、???with 代替：
• （不变量） a同时出现在T a和S a。我们不能再使用phantom，它派上用场了。Edward Kmett有一个模块Data.Functor.Invariant。它为以下类提供了一个地图： 然而，我看不出有什么方法可以把它变成我们可以加入 fmap 的自由定理id的东西——这种类型需要一个额外的函数参数，我们不能把它当作什么东西刷掉。无论如何，我们将invmap代替?map?,xy yx代替??, 并将以下内容代替???:

那么，我对这种算法的理解正确吗？如果是这样，我们如何正确处理Invariant情况？