Lambda 演算转换

Question

如何获取 Haskell 数据类型或函数（例如，fold、list、String、zip）并将其转换或转换为 lambda 演算抽象？例子：如果总和计算列表中所有元素的总和，并且：类型sum = num a => [a] - > a。

    sum []     = 0
    sum (x:xs) = x + sum xs

我如何利用这些信息将其转换为 lambda 演算表达式，或者更确切地说是抽象？

我尝试在网上寻找指南，但他们只是给了我答案。我想知道如何实际从 Haskell 函数（如 add、sum、map、fold 等）进行转换/翻译。到 lambda 演算抽象。

​​

Answer 1

这里要注意的是你的函数 sum 是在列表上定义的，列表是归纳定义的。理论上，列表的归纳定义为每个类型 T 定义了一个术语

match_list :: T -> (a -> [a] -> T) -> ([a] -> T)

满足财产

match_list s t [] = s 
match_list s t (x::xs) = (t x xs)

此外，定义递归函数需要一个不可类型化的函数 定点组合器 fix 满足财产

fix F = F (fix F)

因此，将两者结合起来，我们可以通过首先定义来编写您的定义

F :: ([a] -> a) -> ([a] -> a)
F := λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))

进而

sum := λ x -> (fix F) x
     = λ x -> (fix (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs)))) x

为了让自己相信这是可行的，让我们在示例中尝试一下

sum [1,2] = (fix F) [1,2] 
          = (F (fix F)) [1,2]
          = (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1,2]
          = match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1,2]
          = 2 + ((fix F) [1])
          = 2 + ((F (fix F)) [1])
          = 2 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1])
          = 2 + (match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1])
          = 2 + (1 + ((fix F) []))
          = 2 + 1 + ((F (fix F)) [])
          = 2 + 1 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [])
          = 2 + 1 + (match_list 0 (λ x -> (λ xs -> x + (fix F) xs)) [])
          = 2 + 1 + 0

从理论上讲，这就是纯函数式语言中会发生的情况（例如 无类型的 lambda 演算），但是在 haskell、lisp 或 ocaml 等语言中（我不知道 python 中的归纳数据类型），这些术语 match_list 和 fix 是“内部”构造，并且不是语言中的明确术语。

Answer 2

试试这个....它应该通过步骤

帮助构建直觉

http：//页面。cs.wisc.edu/~horwitz/cs704-notes/2.lambda-calculus-part2.html

或者，因为它并不清楚你的意思，也许是你想要的东西的例子，你想要的东西比Sum更简单？