我正在研究Lambda微积分。我需要定义一个辛迪加的lambda图像，该图像根据输入数组是否与中心对称而返回true或false。 对于您的任何帮助，我都会感到非常高兴，因为这个主题对我来说很难。 我了解如何定义基本构造函数，例如true或false，以及加法和乘法。 我想做一些算法：
查找堆栈中的元素数。
将堆栈的一半（四舍五入）拉到另一个堆栈上。
如果元素数为奇数，则从第一个堆栈中删除该元素。
更新
1.lenght =λl.l（λx.succ），其中succ =λnfx.nf（f x）
在纯λ微积分中，您无权访问任何数据类型，但仍可以使用所谓的Church-encodings表示它们。
例如，一元表示形式的自然数可以是0（z）或另一个自然数s的后继者（n），即表示n+1。
因此，您有z，s z，s (s z)，s (s (s z))等。
为了用λ微积分表示它们，可以使用以z和s作为参数的函数：
λz.λs.z，λz.λs.s z，λz.λs.s (s z)，λz.λs.s (s (s z))等。
此表示法的一个很酷的地方是它还为您提供了自然数的递归，即一种在自然数上归纳构建内容的方法。
假设您要测试n是否为0，只需输入n true (λm. false)（其中true和false代表布尔值，但它们可以是任何值真）。然后，您有
0 true (λm. false) = true
1 true (λm. false) = (λm. false) true = false
2 true (λm. false) = (λm. false) ((λm. false) true) = false
...
表示您可以将0与其他教堂数字区分开。
基本上，当您输入教堂数字b和f时，您将0的图像表示为b，并将函数f赋予{{ 1}}到n的图片。
要编写n+1函数以在自然数上加一个，您想在其表示法前面添加一个succ：
s succ n = λz.λs.s (n z s)
相当于删除了前两个n z s。
现在列表可以用相同的方式表示。列表可以是空列表（λ或[]），也可以是附加到其他列表（nil）上的某个元素（head）：tail或head :: tail。
我们执行相同的技巧：
cons head tail是nil，λn.λc.n是cons x nil，λn.λc.c x n是cons y (cons x nil)，等等。
类似地，您可以将基本情况和函数提供给列表以执行 fold 。
λn.λc.c y (c x n)要获取长度，您必须注意cons x (cons y nil) b f = f x (f y b)
(cons x1 (cons x2 (... (cons xn nil) ...))) b f = f x1 (f x2 (... (f xn b) ...)))
的长度为nil，而0的长度为cons x l，而不取决于{{1 }}。
succ (length l)。
您应该继续构建这样的基元，以最终解决您的问题。
接下来，您要编写x函数，该函数采用整数length l = l 0 (λ_.λn. succ n)和列表firstn并返回n前几个元素。
基本上你有
l所以您首先要对自然数进行分析，然后对列表进行分析。 我将其写为一个函数，该函数采用自然数，然后返回一个带有列表并返回列表的函数。
n其中的firstn 0 l = nil
firstn (n+1) nil = nil
firstn (n+1) (cons a l) = cons a (firstn n l)
代表我在定义firstn = λn. n (λl. nil) (λr.λl. l nil (λa.λl. cons a (r l)))
时的递归调用r。
这有点棘手，说实话，知道如何用适当的功能语言和模式匹配来编写它会有所帮助。我亲自在Coq中测试了这些。
也许更容易理解的是，首先在列表上编写一个案例分析功能，但是为此，我们需要构建配对。
一对是由两个元素组成的，因此从任何一个对中，您都希望能够观察到这两个元素。
firstn n换句话说
firstn (n+1)然后您可以轻松地拍摄一对的第一和第二个投影。
pair a b = λp. p a b
你可以看到
pair = λa.λb.λp. p a b
列表上的案例分析就像模式匹配，在ocaml中，您会编写
fst = λp. p (λx.λy.x)
snd = λp. p (λx.λy.y)
表示如果fst (pair a b) = (pair a b) (λx.λy.x)
= (λp. p a b) (λx.λy.x)
= (λx.λy.x) a b
= a
是match l with
| nil -> b
| cons h t -> f h t
，我想返回l，如果是nil，我想返回b。
这里没有递归调用，但是，应用cons h t将自动进行递归。特别是，您无法访问f h t，而是可以访问l上的递归调用的值。
为了避免这种情况，我们将使用成对返回原始列表和我们要返回的值。
t如此
t我们想要的。
现在，我们可以再次写caseL = λl.λb.λf. snd (l (pair nil b) (λx.λr. pair (cons x (fst r) (f x (fst r)))
。请记住，caseL nil b f = b
caseL (cons x l) b f = f x l
在列表上计算一个函数，除去了firstn个头元素之外的所有元素。
firstn n它遵循以下结构
n对应于firstn = λn. n (λl. nil) (λr.λl. caseL l nil (λh.λt. cons h (r t)))
上的归纳。
对于n b (λr. f r)
，我们返回基本情况n；对于0，我们获得递归调用b的值，以产生答案n+1。
在我们的案例中，基本案例是函数r，这意味着该函数获取列表并将其全部丢弃。
定义f r时，递归调用对应于firstn 0，在这种情况下，我们想对上面的列表进行案例分析，使用firstn n（即firstn (n+1)）如果列表不为空，则为尾巴。
firstn n因此，如果您看上去很努力，那么您已经可以看到它只是一个只获取列表的前两个元素的函数。
r