Ign*_*rov 2 recursion haskell denotational-semantics
我的意思是,从定义来看:
fix f是函数的最不固定点f
换一种说法:
最不明确的
x那样f x = x.
任何nullary类型的最小定义值是undefined.这里仍有一些含糊不清,undefined可能意味着"将抛出错误"(更好)或"永远不会终止"(更糟糕).正如推理和试验所显示的那样,fix (+1)并且fix pred :: Word两者似乎都没有接近终止(即使pred 0是一个错误),因此在这两种选择之间可能总是选择"永不终止"的更糟糕的一种.(可以逃脱的fix是无聊const 1,但稍后会.)
这不是有用的应用方式fix.
有用的应用方式fix是:
fix (\f x -> if x > 7 then f (x - 1) else x)
- 也就是说,使用fix神奇地产生递归函数.(这永远不会让我感到惊讶.)这可以被视为在两个函数之间进行选择:\f x -> f (x - 1)并且\_ x -> x,其中一个函数永远不会评估它的第一个绑定变量.这是一个危险的玩具,因为我们仍然可以得到意外地翻转即非终止了半个其领域一样容易作为一个函数>来<或-来+.
所以,不知何故,这两个功能:
f1 = \f x -> f (x - 1)
f2 = \_ x -> x
- 后者是" 最不明确的 ".如果我们眯着眼睛,我们实际上可以认出我们这个无聊的家伙const,只是flip'd.
现在,这是违反直觉的.f2实际上更容错,所以,从某种意义上说,它的定义是更多的输入值f1.(特别是,这是让它逃脱无限循环的原因fix).具体来说,f2定义为所有相同(f, x)的输入对f1加上(undefined, x).沿着同一条线,const 1是所有一元函数最容错的.
那么,我现在如何理解定义？
这个问题的一些理由
附近有这样的答案,提供了与fix此问题中提出的不同的直觉.它还强调,为了充分理解,必须传递给指称语义的外部教程.
我想得到一个答案,要么支持,要么解释这里提出的直觉的错误,而且,如果领域理论真的落后于评论中提出的草书排序,至少包括一些允许的经验法则,然而,领域理论的有限但实际应用.我希望看到的问题的一个特定部分是能否fix始终在一个常数函数和一个约简函数上分解一个能函数,以及这些函数类的定义是什么.
我的愿望是建立有用且安全的fix编码递归的实际,实用的答案,并得到坚实的数学推理的支持.
在Haskell中,函数是纯粹的.他们接受输入和产量输出.所以出现了一个自然的问题:那些不会终止的函数呢？
f x = 1 + f x
此函数将使解释器锁定在无限循环中.但在数学上,我们不得不说它"返回"某些东西,否则它不是一个函数.我们将这种特殊的"出问题"称为"底部"值,我们用符号表示它?.
因此,从数学上讲,Haskell Int类型包含每个整数,以及一个额外的特殊元素:?.我们称之为包含?"提升"类型的类型,并且几乎所有在Haskell中使用的类型都被提升.[1]事实证明,无限循环不是唯一的调用方式?.我们也可以通过其他方式"崩溃"解释器来实现.您将看到的最常见的方法是使用undefined内置函数,该函数通过一般错误来暂停程序.
但还有另一个问题.具体来说,停止问题.如果?应该表示无限循环和其他不可预测的问题,那么我们无法在Haskell中编写某些函数.例如,以下伪代码是荒谬的.
doesItHalt :: a -> Bool
doesItHalt ? = False
doesItHalt _ = True
这将检查结果值是否为?,这将解决暂停问题.显然,我们不能在Haskell中做到这一点.那么我们可以在Haskell中定义哪些函数？我们可以定义那些与定义性排序有关的单调性.我们定义?为这种排序.我们说?是最不明确的价值,所以? ? x对所有人而言x.?是部分排序,因此无法比较某些元素.虽然1 ? 1,这是不正确的,要么1 ? 2 或 2 ? 1.在纯粹的英语中,我们说这1肯定是低于或等同定义的1(显然;它们是相同的值),但是说1或多或少定义没有意义2.他们只是......不同的价值观.
在Haskell中,我们只能定义与此排序有关的单调函数.所以,我们只能定义其功能,所有的值a和b,如果a ? b再f a ? f b.我们上面的doesItHalt失败,因为,例如,? ? "foo"而是f ? = False和f "foo" = True.正如我们之前所说,两个完全定义但不相等的值无法比较.所以这个功能无法正常工作.
简单来说,我们定义这种方式的顺序的原因是,当我们使用模式匹配"检查"一个值时,它作为一个断言,必须至少定义它足以让我们看到我们匹配的部分.如果不是,那么我们总会得到?,因为程序会崩溃.
在我们讨论之前fix,值得注意的是,存在"部分定义"的值.例如,1 : ?(在Haskell中,我们可以将其写为1 : undefined)是一个列表,其第一个元素已定义,但列表的尾部未定义.在某种意义上,这个值比"简单"更"定义" ?,因为我们至少可以模式匹配并提取第一个值.所以我们会说? ? (1 : ?) ? (1 : []).因此,我们最终得到了"定义"的层次结构.
现在,fix它说它返回最不明确的定点.的函数的固定点f是一个值x,使得x = f x.让我们试试看几个例子,看看我们是否可以弄清楚它为什么这么说.让我们定义一个函数
f 0 = 1
f x = x
这个功能有很多固定点.x除了零以外的任何其他f x = x.根据我们的"最不明确"原则,哪一个将被退回？?实际上,f ?将会回归?.如果我们传递undefined给f第一个模式匹配将导致程序崩溃,因为我们正在比较未定义的值0.这?是一个定点,因为它是最不可能定义的值,它将返回fix f.在内部,fix通过将函数无限地应用于自身来工作,因此这具有一定的意义.应用f (f (f ...))将继续尝试比较内部参数,0并永远不会终止.现在让我们尝试不同的功能.
g x = 0
无限地将此功能应用于自身0.事实证明,fix g = 0.为什么0在这种情况下返回而不是?？事实证明,它?不能成为这个功能的定点.g ? = 0.由于争论从未检查和Haskell是一种非严格的语言,g将返回0,即使你通过undefined或error "Oops!"或一些荒谬的无限递归值作为参数.因此,只有固定点g,即使在升起类型,是0,由于g 0 = 0.因此,0确实是最不明确的定点g.
因此,总而言之,我们定义了一个数学框架,以便严格描述某些函数不会终止的概念."最不明确的"只是一种非常数学上精确的说法,它fix不适用于对其论证总是严格的函数.如果f ?要返回,?那么fix f也将返回?.
*大部分答案都是在deotational Semantics的wiki页面上进行了解释和总结.我鼓励阅读该页面以获取更多信息; 对于非数学家来说,这是非常容易理解的,并且非常有用.
[1]一些原始类型未被解除.例如,GHC特定Int#是一种整数类型,它不包含?并在某些地方内部使用.