【问题标题】:Haskell: Alternative, non-circular definition of Redex?Haskell:Redex 的替代、非循环定义?
【发布时间】:2026-02-07 11:05:04
【问题描述】:

我对 Haskell 中的 redex 是什么和不是 redex 感到很困惑,所以我花了一些时间来研究它,但我想知道我是否做对了。

我找到了 redex 的这个定义,它是循环的; Etymology : From "reducible expression" Definition: Redex (plural redexes): (mathematics) Something to be reduced according to the rules of a formal system. http://en.wiktionary.org/wiki/redex

上述定义假定一个人知道如何减少。所以对我来说,这就像说“蓝色是看起来蓝色的品质”,这也是圆形的。

然后我找到了一篇博文,定义redex如下; Any subgraph that matches a rule is called a reducible expression, or redex for short. https://hackhands.com/lazy-evaluation-works-haskell/

这好多了,但是,从字面上看,它意味着它是特定于实现的,这似乎很奇怪。换句话说,如果我可以使用不同的评估树以两种不同的方式定义 myfunc,那么什么是 redex 的定义就会有所不同。我不认为这是真的。

似乎重要的是评估解析树,以及什么是原语的定义。我找不到 Haskell 原语的定义,但我找到了一个可能不完整的列表:“重要的 Haskell 原语函数”http://www.cs.sjsu.edu/faculty/smithj/oldclass/152f11/haskell-primitives.html

有没有我错过的 Haskell 原语的真正定义?

接下来,该列表有助于识别一些原始和非原始示例。 -- Primitive: *, / , div -- Not-Primitive (not on the list): mul

综上所述,原始函数评估是可简化的,它是评估树上的叶节点。减少从函数调用减少到数据点。

那么,这个定义是怎样的呢? Redex: In Haskell, evaluation proceeds with the base case that any primitive function application constitutes a leaf node of the evaluation tree. Such leaves are reducible from function applications into pure data elements. Thus we define all leaf nodes as reducible expressions, or "redexs" for short.

谢谢!

编辑;这里有一些我试图适应的例子,我相信这些例子是正确的。 第一个来自 Graham Hutton,Haskell 编程。 -- Consider these cases; -- 1.An expression using a function mult ::(Int, Int)-> Int -- pg.126 mult (x,y) = x*y mult(1+2, 3+4) -- This has 3 redexes, one for each argument and one for the call, per the book

-- 2.现在考虑使用原语'*',而不是函数mul, 7 + (6*8) -- 每个讨论都有一个 redex,只有 6*8。

-- 3.最后,对比所有不带括号的原语表示新的评估级别 1+2*3 -- 我相信这应该有零个redexes,因为它们只是可以一次评估的原始表达式。

【问题讨论】:

  • -1 票的原因?我在 Graham Hutton 的书中也找到了这个循环定义,所以这似乎是一个重要的问题。
  • 您可以根据实现内部的原语来考虑什么是可约化的,但您也可以独立于实现来考虑就语言而言什么是可约化的。对于 Haskell 来说,后者的一个版本是“lambda 的应用是可约的。构造函数对可约表达式的应用是可约的。lambda 是不可约的。构造函数对不可约表达式的应用是不可约的。”
  • 我不是在批评你的说法,我建议你也可以从表达式的含义而不是解释器的实现方式来考虑减少。如果这样做,则无需区分原始函数与由 lambda 和函数声明定义的函数。相反,您可以认为所有函数都是由 lambdas “构造”的。在任何一种情况下,任何函数应用都是可简化的。 (另外,我什至没有乌鸦。)
  • 是的,您需要知道如何减少。它在您的正式系统定义中。例如,阅读关于 lambda 演算的*条目,其中明确列出了减少量。
  • 您的最后一个示例仍然有一个 redex,2 * 3。括号无所谓。此外,*对“redex”的定义不是“循环的”。定义是指正式系统的规则,是的。因此,除非您了解正式系统,否则您无法定义“redex”是什么。但只要正式系统的规则不是基于“redex”是什么,就没有循环性。

标签: haskell lazy-evaluation primitive reduction


【解决方案1】:

函数式语言中的redex,一旦你超越了语法(即把1 + 2从中缀翻译成(+) 1 2)就是任何看起来像f x的东西——即一个函数和一个参数,这样该函数尚未应用于参数。

不必担心哪些是“原始”函数,哪些不是“原始”函数

事实上,反对赫顿,我会说1+2两个 redexes,因为它实际上是非咖喱的,所以“去糖”的形式是((+) 1) 2

【讨论】: