标签: lambda-calculus

我坚持下一步.如果有人可以帮助我,那将是很棒的:

2 = ?fx.f(f x)
3 = ?fx.f(f(f x))
ADD = ?m n f x. m f (n f x)

我的步骤是:

   (?m n f x. m f (n f x)) (?f x.f(f(f x))) (?f x.f(f x))
-> ((?n f x. (?f x.f(f(f x))) f (n f x))) (?f x.f(f x))
-> ((?f x. (?f' x'.f'(f'(f' x'))) f ((?f" x".f"(f" x")) f x)

括号好吗？我真的对替换和括号感到困惑.是否有一种正式的,更容易解决此类问题的技术？

为了了解固定点组合器是什么和用于什么,我写了自己的.但不是用严格的匿名函数编写它,比如维基百科的例子,我只使用了define:

(define combine (lambda (functional)
                  (functional (lambda args (apply (combine functional) args))))

我用factorial和fibonacci的函数来测试它,它似乎工作.这是否符合定点组合器的正式定义？

我很好奇Kiselyov和Shan 在" 功能性珍珠:隐式配置"一文中讨论的对隐式参数的反对意见.

在存在隐式参数的情况下内联代码(β-reduce)是不可靠的.

真？我希望GHC应该内联到与传递的隐式参数相同的范围,不是吗？

我相信我理解他们的反对意见:

如果添加,删除或更改其签名,则术语的行为可能会发生变化.

GHC的用户文档解释说,程序员必须注意多态递归和单态限制.这是不是因为内联问题意味着什么？

我假设这个多态递归示例还涵盖了"概括隐含参数"的意思吗？还要别的吗？

Data.Reflection的ReifiesStorable类型类是否真的是解决这些困难的合理解决方案？它似乎每次访问时都会对整个隐式数据结构进行反序列化,这听起来对性能来说是灾难性的.例如,我们可能希望我们的隐含信息是Cayley表或占用ram gig的字符表,并且必须在数百万代数运算期间访问.

是否有一些更好的解决方案采用隐式参数,或者编译器可以在幕后轻松优化的另一种技术,同时仍然通过类型系统使用状态线程或其他保证更多？

假设有一些数据类型来表达lambda和组合术语:

data Lam ? = Var ?                   -- v
           | Abs ? (Lam ?)           -- ?v . e1
           | App (Lam ?) (Lam ?)     -- e1 e2
             deriving (Eq, Show)

infixl 0 :@
data SKI ? = V ?                     -- x
           | SKI ? :@ SKI ?          -- e1 e2
           | I                       -- I
           | K                       -- K
           | S                       -- S
             deriving (Eq, Show)

还有一个函数来获取lambda术语的自由变量列表:

fv ? Eq ? ? Lam ? ? [?]
fv (Var v) = [v] …

在Haskell中编写一些lambda函数时,我最初编写的函数如下:

tru = \t f -> t
fls = \t f -> f

但是,我很快从网上的例子中注意到这些函数经常被写成:

tru = \t -> \f -> t
fls = \t -> \f -> f

具体而言,传递给函数的每个项都有自己的\,->而不是上面的.检查这些类型时,它们看起来是一样的.我的问题是,它们是相同的还是它们在某种程度上确实存在差异？不仅仅是这两个功能,而且它对一般的功能有什么影响？非常感谢!

lambda演算的n元组通常定义为:

1-tuple:     ? a t . t a
1-tuple-fst: ? t . t (? a . a)

2-tuple:     ? a b t . t a b
2-tuple-fst: ? t . t (? a b . a)
2-tuple-snd: ? t . t (? a b . b)

3-tuple:     ? a b c t . t a b c
3-tuple-fst: ? t . t (? a b c . a)
3-tuple-snd: ? t . t (? a b c . b)
3-tuple-trd: …

假设我有一个scott编码的列表,例如:

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

我想要一个接收这种类型的列表并将其转换为实际列表([1,2,3])的函数,除了这样的函数不能递归.也就是说,它必须是eta-beta正常形式.这个功能存在吗？

考虑在类型检查期间获得的以下标准化术语表示:

data Normal a
  = Neutral (Neutral a)
  | Type
  | Pi (Normal a) (Normal (Maybe a))
  | Abstract (Normal (Maybe a))

data Neutral a
  = Variable a
  | Apply (Neutral a) (Normal a)

我希望能够在此框架中表示一个修复点,或者至少以保留其head-normal属性的方式,这对于实现替换和定义相等非常方便.

起初,我想过使用微积分本身定义的固定点组合子.但是,Y组合器是不可能的,因为这个术语表示我不能将lambda应用于lambda.Z组合器接近我想要的,但假设结果是一个函数.

如果我只是简单地进行图形缩减,我会将结与Haskell本身联系起来,导致一个懒惰的无限语法树.但是,由于这是用于依赖类型检查器,我需要能够在术语上测试定义相等 - 它会以这种方式陷入无限循环.

我想在薄荷细节中理解我们如何设法从Y-combinator的lambda演算中获得:

Y = ?f.(?x.f (x x)) (?x.f (x x))

到以下实现(在Scala中):

def Y[A, B](f: (A => B) => A => B): A => B = (x: A) => f(Y(f))(x)

我对函数式编程很陌生,但我对lambda演算以及替换过程的工作方式有了不错的理解.然而,我很难理解我们是如何从正式表达式实现的.

此外,我想知道如何告诉我的函数的参数的类型和数量以及它的返回类型是什么lambda？

我正在用C＃编写lambda演算的解释器。到目前为止，我已经采用了以下几种解释方法。

1. 将术语编译为MSIL，这样仍然保留了惰性评估。
2. 对术语树进行评估（术语重写）。

目前，在我能够测试的大多数情况下，MSIL编译策略的速度都快一个数量级。但是，我正在通过确定通常在LC术语构建中使用的模式来优化术语重写器。到目前为止，我特别提出了一种方法，该方法提供了相对较小的加速：识别指数级应用程序。例如f (f (f (f x)))简化为f^4 x。然后，使用相等于申请人指数的规则，即f^m (f^n x) = f^(m + n) x。该规则特别适用于教堂数字的取幂。

我想知道这种优化：LC中是否还有其他基于模式的优化方法？