Lambda 演算转换
-
29-09-2020 - |
题
如何获取 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 演算抽象。
解决方案
这里要注意的是你的函数 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
是“内部”构造,并且不是语言中的明确术语。
其他提示
试试这个....它应该通过步骤
帮助构建直觉http://页面。cs.wisc.edu/~horwitz/cs704-notes/2.lambda-calculus-part2.html
或者,因为它并不清楚你的意思,也许是你想要的东西的例子,你想要的东西比Sum更简单?不隶属于 cs.stackexchange