问题标签 [lambda-calculus]

我应该采用以下代码：

并在没有 where（或 let）的情况下重写它。

他们的意思是用 Lambda 函数 (\x ->...)

我正在尝试在 Haskell 上重用 Lambda 函数。有任何想法吗？

It is by now a well known theorem of the lambda calculus that any function taking two or more arguments can be written through currying as a chain of functions taking one argument:

This has proven to be extremely powerful not just in studying the behavior of functions but in practical use (Haskell, etc.).

Functions returning values, however, seem to not be discussed. Programmers typically deal with their inability to return more than one value from a function by returning some meta-object (lists in R, structures in C++, etc.). It has always struck me as a bit of a kludge, but a useful one.

For instance:

Questions

1. Does the lambda calculus have anything to say about a multiplicity of return values? If so, do any surprising conclusions result?
2. Similarly, do any languages allow true multiple return values?

我无法比 Wikipedia 更好地解释lambda cube一词：

[...] λ-cube 是一个框架，用于探索 Coquand 构造演算中的细化轴，从简单类型的 lambda 演算开始，作为放置在原点的立方体的顶点，以及构造演算（高阶依赖类型的多态 lambda 演算）作为其截然相反的顶点。立方体的每个轴都代表一种新的抽象形式：

• 术语取决于类型或多态性。System F，又称二阶 lambda 演算，是通过仅施加此属性而获得的。
• 类型取决于类型或类型运算符。仅通过强加此属性即可获得具有类型运算符 λω 的简单类型 lambda 演算。与系统 F 结合产生系统 Fω。
• 类型取决于术语或依赖类型。仅施加此属性会产生 λΠ，这是一个与 LF 密切相关的类型系统。

所有八个演算都包括最基本的抽象形式、依赖于术语的术语、简单类型的 lambda 演算中的普通函数。立方体中最丰富的演算，包含所有三个抽象，是构造演算。所有八个结石都在强烈规范化。

是否可以为每个改进找到 Java、Scala、Haskell、Agda、Coq 等语言的代码示例，而这些改进在缺乏这种改进的微积分中是不可能实现的？

我不明白为什么在无类型的 lambda 演算中允许以下 beta 减少：

具体来说，我无法理解如何将两个参数传递给零件中u的v单个参数。为了允许上述情况，我不应该使用柯里化并有两个参数吗？像这样-xλx.x

给定

和

如果我从 (SKK) 形式或等效的扩展形式开始，我无法理解同一表达式 (SKK) 的两个 beta 等效形式如何在无类型 lambda 演算中产生不同的结果：

似乎压缩和扩展形式有不同的括号，实际上第一个括号为：

而第二个为：

有人对此有任何见解吗？？？谢谢

我以前从未在 typeclass 中看到过方程式（或函数声明？）。为什么 typeclass 中有一个方程？

我知道_是匹配任何东西的术语。但是m >>= \_ -> n匹配什么？

我被 Wikipedia 对 lambda 演算中前任函数的描述所困扰。

维基百科说的是以下内容：

有人可以逐步解释减少过程吗？

谢谢。

（我确信这个问题肯定已经在这个网站上得到了回答，但是搜索被 C 中的一个变量调用 free() 的概念所淹没。）

我遇到了“eta减少”一词，它的定义类似于f x = M x ==> M如果x“在M中不是自由的”。我的意思是，我想我理解它想说的要点，当你将一个函数转换为无点样式时，这似乎是你所做的，但我不知道关于 x 不是免费的限定词是什么意思。

我一直在阅读的《计算机程序的结构和解释》一书通过定义零和增量函数来介绍 Church 数字

这对我来说似乎很复杂，我花了很长时间才弄清楚并推导出一个 ( λf.λx. f x) 和两个 ( λf.λx. f (f x))。

用这种方式编码数字不是更简单吗，零是空的 lambda？

现在很容易推导出一个 ( λ. λ) 和两个 ( λ. λ. λ)，依此类推。

这似乎是用 lambda 表示数字的一种更直接、更直观的方式。这种方法是否存在问题，因此有充分的理由说明教堂数字以它们的方式工作吗？这种方法是否已经得到证实？

可以通过高阶函数对无类型 lambda 演算中的各种类型进行编码。

我想知道是否有任何研究涉及嵌入其他不太传统的类型。如果有一些定理断言可以嵌入任何类型，那就太好了。也许有一些限制，例如只能嵌入 kind * 类型。

如果确实可以表示不太传统的类型，那么看到一个例子会很棒。我特别热衷于看看 monad 类型类的成员长什么样。