标签: lambda-calculus

我一直在阅读的计算机程序书的结构和解释通过定义零和增量函数来呈现教会数字

zero: ?f. ?x. x
increment: ?f. ?x. f ((n f) x)

这对我来说似乎相当复杂,我花了很长时间才弄清楚它并派生出一个(?f.?x. f x)和两个(?f.?x. f (f x)).

以这种方式编码数字会不会更简单,零是空的lambda？

zero: ?
increment: ?f. ?. f

现在,派生一个(?. ?)和两个(?. ?. ?)等等是微不足道的.

这似乎是用lambda表示数字的更直接明显和直观的方式.这种方法是否存在一些问题,因此教会数字的工作原理是一个很好的理由？这种方法已经证实了吗？

（图1）

简单类型 lambda 演算的一部分（图 1），它在 Haskell 中实现，如下所示。

 evaluate expression = do
        case expression of
        (Application (Lambda x ltype term) value) | isValue value = True -> substitute term x value
        (Application value e2) | isValue value = True  -> let e22 = evaluate e2 in Application value e22
        (Application  e1 e2) -> let e11 = evaluate e1 in Application e11 e2

但是，这不适用于这些测试用例，

1) print (evaluate (Application (Var "x") (Var "y")))

2）print (evaluate (Application (Constant 3) (Var "y")) “（常量3）是一个值”

但是，第一次测试时，我知道这是因为 …

在另一个问题中,Bob 为无类型lambda演算提供了以下解释器.

data Expr = Var String | Lam String Expr | App Expr Expr

data Value a = V a | F (Value a -> Value a)

interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case …

通过阅读lambda 立方体和此线程的维基百科条目，当应用于 Haskell 时，我的理解是

\n
1. 按术语索引的术语族 - 从值到值的典型函数
\n
2. 按类型索引的术语族 - ??
\n
3. 按类型索引的类型族 - 类型构造函数、类型族中的参数多态性
\n
4. 按术语索引的类型系列 - pi 类型（在 Haskell 中使用单例类型进行伪造）、sigma 类型等...
\n

如果我上面列出的示例有误，请纠正我。引用维基百科的那篇文章：

\n

\n
• 术语取决于类型或多态性。系统 F，又名二阶 lambda 演算（图中写为 \xce\xbb2），是通过仅施加此属性获得的。
\n

\n

我不知道 Haskell 如何适应上面的（2）。Haskell 在术语和类型以及类型擦除之间有很强的区别，因此 OOP 中没有反射的东西，例如typeof(a)或b.GetType()，然后在运行时根据类型信息返回一些值。

所以我在 Haskell 中唯一能想到的与 (2) 有关的可能是

\n
• 比如说memptyin 中的返回类型多态性Data.Monoid，其中值取决于实例类型
\n
• 在左侧接受类型并在右侧具有值构造函数的数据族
\n

那是正确的吗？虽然我觉得我没有建立所有联系......

说特设多态性满足 (2) 而参数多态性满足 (3) 是否正确？但是，临时与参数与类型与数据系列的 RHS 差异有何关系？ …

堆!是否有可能在现代Haskell中定义Omega组合器(λx.xx)？我想,Haskell98的类型系统旨在使这样的事情变得不可能,但现代扩展呢？

我想在Haskell中的多态lambda演算中实现该对的Church编码.

在Peter Selinger关于lambda演算的注释的第77页第8.3.3节中,他给出了两种类型的笛卡尔积的构造.

A×B =∀α.(A→B→α)→
α⟨M,N⟩=Λα.λfA ^→B→ α.fMN

对于另一个来源,在第54页,DiderRémy关于lambda演算的注释的第4.2.3节,他将多态λ演算/系统F中的对的教会编码定义为

Λα₁.Λα₂.λx₁:α₁.λx₂:α₂.Λβ.λy:α₁→α₂→β.y x 1 x 2

我认为雷米和塞林格一样,更加啰嗦.

无论如何,根据维基百科,Haskell的类型系统基于System F,所以我希望可以直接在Haskell中实现这个Church编码.我有:

pair :: a->b->(a->b->c)->c
pair x y f = f x y

但我不知道如何进行预测.

Λα.Λβ.λp ^α×β .pα(λx ^α .λy ^β .X)

我是否将Haskell forall用作首都lambda类型量词？

这与我之前的问题基本相同,但在Haskell而不是Swift中.我认为额外的环境和场地的变化可能会让它变得更加明智.

我正在基于一些使用未绑定库的现有代码开发项目.

代码使用unsafeUnbind了一堆,这导致我的问题.

我尝试过使用freshen,但是我收到以下错误:

error "fresh encountered bound name! 
Please report this as a bug."

我在想:

• 该库是否打算完全在FreshMmonad中使用？或者他们的方式来做lambda应用程序而不是在做Fresh什么？
• 我可以给出什么样的价值freshen,以避免他们列出的错误？
• 如果我最终使用unsafeUnbind,在什么条件下使用是否安全？

我一直在深入研究FP及其周围的一切,我发现了某种类型的投影仪的概念,没有细节也没有解释.

我发现的唯一一件事是这个github项目,我开始考虑它是指这个特定项目,还是FP中的一些通用概念？

那么,什么是投影仪？为什么有用？(如果可能的话,你能提供例子,资源等吗？)

我想明白,为什么教会定义数字如下:

0 = ? f . ? x . x
1 = ? f . ? x . f x
2 = ? f . ? x . f f x
3 = ? f . ? x . f f f x
4 = ? f . ? x . f f f f x

背后的逻辑是什么？

为什么0表示如下:

0 = ? f . ? x . x

我想了解let绑定在Haskell中是如何工作的(或者如果Haskell实现不同,可能是lambda演算？)

我从阅读中理解为你写了一个Haskell,它对单个let绑定有效.

let x = y in e == (\x -> e) y

这对我来说很有意义,因为它与lambda演算中绑定的工作方式一致.我很困惑的地方是使用多个let绑定,其中一个绑定可以引用上面的绑定.我将提供一个简单的例子.

原始代码:

let times x y = x * y
    square x = times x x
in square 5

我对实施的猜测:

(\square times -> square 5) (\x -> times x x) (\x -> x * x)

这似乎不起作用,因为times当lambda调用square时没有定义.但是,这可以通过此实现解决:

(\square -> square 5) ((\times x -> times x x) (\x -> x * x))

这是实现此绑定的正确方法,至少在lambda演算中是这样吗？