标签: lambda-calculus

我正在用F#写一个lambda演算,但是我坚持实现beta-reduction(用形式参数代替实际参数).

(lambda x.e)f
--> e[f/x]

用法示例:

(lambda n. n*2+3) 7
--> (n*2+3)[7/n]
--> 7*2+3

因此,我希望听到一些关于其他人如何做到这一点的建议.任何想法将不胜感激.

谢谢!

考虑这个组合子:

S (S K)

将其应用于参数XY:

S (S K) X Y

它签订合同:

X Y

我将S(SK)转换为相应的Lambda术语并得到了这个结果:

(\x y -> x y)

我使用Haskell WinGHCi工具获取(\ xy - > xy)的类型签名,并返回:

(t1 -> t) -> t1 -> t

这对我来说很有意义.

接下来,我使用WinGHCi获取s(sk)的类型签名并返回:

((t -> t1) -> t) -> (t -> t1) -> t

这对我来说没有意义.为什么类型签名不同？

注意:我将s,k和i定义为:

s = (\f g x -> f x (g x))
k = (\a x -> a)
i = (\f -> f)

我最近偶然发现了这篇文章,它描述了如何仅使用Ruby中的Procs来编写FizzBu​​zz,并且因为我感到无聊,所以认为尝试使用lambdas在Python中实现相同的东西是很好的.

我到了使用嵌套函数创建数字的部分,并编写了以下Python脚本:

#!/usr/bin/env python

zero  = lambda p : (lambda x: x)
one   = lambda p : (lambda x: p(x))
two   = lambda p : (lambda x: p(p(x)))
three = lambda p : (lambda x: p(p(p(x))))
five  = lambda p: (lambda x: p(p(p(p(p(x))))))

fifteen = lambda p : (lambda x: p(p(p(p(p( \
                                p(p(p(p(p( \
                                p(p(p(p(p(x))))))))))))))))


hundred = lambda p: (lambda x: p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( \
                               p(p(p(p(p(p(p(p(p(p( …

在lambda演算中我没有看到任何二进制数字的提及.教会数字是一元制.我在Haskell问了一个如何做到这一点的问题:如何在Haskell 中实现二进制数 但是即使在我看到并理解了这个答案后,我也无法理解如何在纯粹的无类型lambda演算中做到这一点.

所以这是我的问题:二进制数字是否在无类型lambda演算中定义,并且还为它们定义了后继函数和前导函数？

我正在寻找一个弱正规化lambda项的例子.我是否正确地说以下内容:

(?a.b)((?x.xx)(?x.xx))

减少到:

b

要么:

没有终止(如果你试图减少(?x.xx)(?x.xx))

我不确定第一次减少是否正确所以只需要一些澄清,谢谢.

我想使用functools中的partial来部分应用函数的第二个参数,我知道使用lambda很容易,而不是部分如下

>>> def func1(a,b):
...     return a/b
...
>>> func2 = lambda x:func1(x,2)
>>> func2(4)
2

但我严格要在这里使用局部(为了学习)所以我想出了这个.

>>> def swap_binary_args(func):
...     return lambda x,y: func(y,x)
...
>>> func3 = partial(swap_binary_args(func1),2)
>>> func3(4)
2

是否可以将此策略扩展到我可以在任何地方部分应用任何参数的级别,如下面的伪代码

>>>def indexed_partial(func, list_of_index, *args):
...     ###do_something###
...     return partially_applied_function

>>>func5=indexed_partial(func1, [1,4,3,5], 2,4,5,6)

在我们的例子中,我可以使用此功能如下

>>>func6=indexed_partial(func1, [1], 2)

是否有可能像我想要的索引部分？我有什么类似的东西,我不知道吗？更重要的是索引部分的想法一般是一个好的或坏的想法为什么？

这个问题已被标记为可能的重复可以部分应用不带关键字参数的函数的第二个参数吗？ 在那个问题中,OP问是否有可能部分应用第二个参数但在这里我问的是如何烹饪一个可以部分应用任意参数的函数

在lambda演算中,如果一个术语具有正常形式,则正常的降阶策略将始终产生它.

我只是想知道如何严格证明上述命题？

好的,所以我正在尝试实现lambda演算的基础知识.在这里.

我的号码:

def zero[Z](s: Z => Z)(z: Z): Z = z
def one[Z](s: Z => Z)(z: Z): Z = s(z)
def two[Z](s: Z => Z)(z: Z): Z = s(s(z))

部分(实际上,非)应用它们的版本是这样的:

def z[Z]: (Z => Z) => (Z => Z) = zero _

在继续之前,我定义了一些类型:

type FZ[Z] = Z => Z
type FFZ[Z] = FZ[Z] => FZ[Z]

很好,succ功能就像(应用程序顺序应该完全一样!我在这里定义了):

def succ[Z](w: FFZ[Z])(y: FZ[Z])(x: Z): Z = y((w(y))(x))

并且未应用的版本变得如此可怕:

def s[Z]: FFFZ[Z] …

我正在尝试制作用于计算lambda演算中的列表元素总和和列表长度的函数。
列表示例：a := [1, 2, 3] = ?cn.c 1 (c 2 (c 3 n))
sum a应返回6并len a应返回3。

我写了递归版本：

len = ?l.if (empty l) 0 (plus 1 (len (tail l)))
sum = ?l.if (empty l) 0 (plus (head l) (sum (tail l)))

如果if，empty，plus，tail是其他lamda函数。

然后，我使用定点组合器做了一些技巧：

len = ?l.if (empty l) 0 (plus 1 (len (tail l))) 
len = ?fl.if (empty l) 0 (plus 1 (f (tail l))) len
len = Y ?fl.if (empty l) 0 (plus 1 (f …

我在haskell中具有以下结构，该结构实现了一些用于打印的机制并调用了统一器。我从main收到以下错误：

0 =/= int

似乎认为0是数字而不是变量。以下是完整的实现。

 data CType 
      = CVar Int 
      | CArr CType CType
      | CInt
      | CBool
      deriving (Eq, Data)

data Constraint 
  = Equality CType CType
    deriving (Eq, Data)

我有一些基本类型（int和bool），箭头类型和类型变量。然后，我运行一些生成相等约束的算法，这些约束以上述方式表示。

我的目标是给定约束列表，我想找到最通用的统一器。

我遇到了这个库：http : //hackage.haskell.org/package/compdata-0.1/docs/Data-Comp-Unification.html

由于我是Haskell的新手，所以我无法立即弄清楚是否可以直接应用它。我可以使用该库还是建议从头开始编写统一器？

更新

我目前正在对代码进行以下更改，但方程式出现统一错误

f =克

module SolveEq where
import Data.Data
import Data.Void
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Maybe (fromJust)
import Data.Maybe (isJust)
import Control.Monad
import TypeCheck
import Data.Comp.Variables
import Data.Comp.Unification
import Data.Comp.Term
import Data.Comp.Derive
import Constraint …