标签: lambda-calculus

作为一种消遣，我正在尝试解决我在大学学习的课程（涉及 Lambda 微积分和各种编程概念）中提出的各种问题。因此，我尝试在 OCaml 中实现 Church 数字和相关运算符（也作为 OCaml 中的练习）。

这是到目前为止的代码：

let church_to_int n =
    n (fun x -> x + 1) 0;;

let succ n s z =
    s (n s z)

let zero = fun s z -> z

let int_to_church i =
    let rec compounder i cont =
        match i with
        | 0 -> cont zero
        | _ -> compounder (i - 1) (fun res -> cont (succ res))
    in
    compounder i (fun x -> x)

let add …

谁能解释类型检查和类型推断问题之间的区别？

我试图寻找差异，但我找不到任何令人信服的资料来清楚地解释差异。如果可能的话还包括示例。

有没有办法在 lambda 演算中模拟异常处理？
我问这个问题是因为在过程语言和派生范例中处理异常状态的多种方法是很常见的。setjmp.h即使在 C 语言中，您也可以使用,errno.h和 来非常简单地模拟这种行为signal.h。
我可以在脑海中想象图灵机状态图中的一种方式，一种可以被任何其他节点访问的“异常”节点，并且我猜过程语言会做这种事情来实现它。
但在 Haskell（我最新的痴迷）和一般的函数式编程中，你看不到关于异常的所有模糊之处。我知道它们存在（Control.Exception？）并且我知道函数式编程使用 monad 来模拟副作用，但我承认我不太明白它是什么以及它是如何工作的。
但我在另一次讨论中看到，所有函数式语言都是 lambda 演算的语法糖，那么这样的东西如何工作呢？

我是lambda演算的新手,并努力证明以下内容.

SKK和II是等效的.

哪里

S = lambda xyz.xz(yz)K = lambda xy.x I = lambda xx

我尝试通过打开它来测试减少SKK,但无处可去,它变得凌乱.不要认为SKK可以在不扩展S,K的情况下进一步减少.

我在Haskell中实现了一个不纯的无类型lambda-calculus解释器.

我目前仍然坚持实施"alpha-conruence"(在某些教科书中也称为"alpha-equivalence"或"alpha-equality").我希望能够检查两个lambda表达式是否相等或相等.例如,如果我在解释器中输入以下表达式,它应该产生True(\用于表示lambda符号):

>\x.x == \y.y
True

问题是要理解以下lambda表达式是否被视为alpha-equivalent:

>\x.xy == \y.yx
???

>\x.yxy == \z.wzw
???

在\x.xy == \y.yx我猜的情况下,答案是True.这是因为\x.xy => \z.zy和\y.yx => \z.zy两者的右侧相等(其中符号=>用于表示减少α).

在cae中\x.yxy == \z.wzw我也会猜到答案是True.这是因为\x.yxy => \a.yay与\z.wzw => \a.waw它(我认为)是相等的.

问题是我的所有教科书的定义都指出,只有两个lambda表达式需要更改绑定变量的名称才能被认为是相等的.它没有说明需要统一重命名的表达式中的自由变量.因此即使y并且w它们都在lambda表达式中的正确位置,程序如何"知道"第一个y代表第一个w而第二个y代表第二个w.我需要在实现中保持一致.

简而言之,我将如何实现函数的无错误版本isAlphaCongruent？为了实现这一目标,我需要遵循哪些准确的规则？

我更愿意在不使用de Bruijn指数的情况下这样做.

我正在学习计划,我遇到了这些功能:

(define t (lambda (x) (lambda (y) x))) 
(define f (lambda (x) (lambda (y) y))) 

显然,它们是真假的功能.我不知道为什么!

我有两个问题:

1)连续的lambdas是什么意思？我只习惯看到一个用于将参数传递给函数的lambda; 即

(define add
  (lambda (x y)
    (+ x y)))

通过调用(add 1 5)我将6作为输出提供.

2)如何使用这些真假函数？

我最近一直在研究lambda计算,我对减少和替换有很多疑问.什么是alpha和beta减少？他们何时以及为何使用？

如果有人能说出有关lambda caculus的减少和替代的任何好资源,那就太好了.

这可能不是一个非常实际的问题,我只是好奇我是否可以实现只有lambda表达式的堆栈.

堆栈支持3个操作:top,pop和push,因此,我首先定义堆栈是一个3元组:

data Stack a = Stack a (a -> Stack a) (Stack a)
             | Empty

这里Empty代表空堆,所以我们至少有一个居民开始.

根据这个定义,除了push操作之外,eveything看起来很好:

import Control.Monad.State
import Control.Monad.Writer
import Data.Maybe

data Stack a = Stack a (a -> Stack a) (Stack a)
             | Empty

safePop :: Stack a -> Maybe (Stack a)
safePop Empty = Nothing
safePop (Stack _ _ s) = Just s

safeTop :: Stack a -> Maybe a
safeTop Empty = Nothing
safeTop …

我为Core Haskell编写了一个定制漂亮的打印机,以便更好地研究Core的结构.这个漂亮的打印机的要点是它需要一个CoreModule并在输出中包含数据构造函数,默认Outputable实现似乎没有.

这是我运行漂亮的打印机的模块的代码:

module Bar2 where

add :: Int -> Int -> Int
add a b = a + b

add2 a b = a + b

这是漂亮的打印机输出:

------------------------------- Module Metadata --------------------------------
Module { "main" :: modulePackageId, "Bar2" :: moduleName }
-------------------------------- Type Bindings ---------------------------------
[r0 :-> Identifier ‘add’, rjH :-> Identifier ‘add2’]
-------------------------------- Core Bindings ---------------------------------
NonRec (Id "add2")
       (Lam (TyVar "a")
            (Lam (Id "$dNum")
                 (Lam (Id "a1")
                      (Lam (Id "b")
                           (App (App (App (App …

我一直在尝试用F#实现教堂数字.他们在大学的一个课程中被简要介绍过,从那以后我可能已经离开了兔子洞.我有Predecessor,Successor,Add和Operations工作,但我不能减去工作.我正在尝试多次执行减法b应用前任.我觉得奇怪的是我的代码中的倒数第二行有效,但我认为是等效的,最后一行是行不通的.存在类型不匹配.

我对F#很新,所以任何帮助都会受到赞赏.谢谢.

//Operations on tuples
let fst (a,b) = a
let snd (a,b) = b
let pair a b = (a,b)

//Some church numerals
let c0 (f:('a -> 'a)) = id
let c1 (f:('a -> 'a)) = f 
let c2 f = f << f
let c3 f = f << f << f
let c4 f = f << f << f << f

// Successor and predecessor
let cSucc (b,(cn:('a->'a)->('a->'a))) = if b then (b, fun f -> …