拉姆达演算问题

发布于 2024-12-02 06:47:32 字数 450 浏览 1 评论 0原文

我要解决 lambda 演算问题。我达到了某个点，但我不知道如何继续：

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> g::a5 (f::a2 x::a3 g::a5)::a6)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a4

a1 = (a3 -> a5 -> a4) -> a3 -> a4
a1 = (a3 -> (a6->a4) -> a4) -> a3 -> a4

有什么方法可以结束吗？我使用“a1,a2,a3...”来表示元素或函数的类型。例如，1::Int、2.4::Float、f::a1、x::a3 等。我不知道它是否足够清楚...

非常感谢！

原文

I gotta solve a lambda calculus problem. I reached certain point and I don´t know how to continue:

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> g::a5 (f::a2 x::a3 g::a5)::a6)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a4

a1 = (a3 -> a5 -> a4) -> a3 -> a4
a1 = (a3 -> (a6->a4) -> a4) -> a3 -> a4

is there any way of finishing?. I use "a1,a2,a3..." to represent a type for the element or function. For example, 1::Int, 2.4::Float, f::a1, x::a3 and so on. I don´t know if it is clear enought...

Thank you so much!!

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

非要怀念 2024-12-09 06:47:32

你犯了一个错误。 g=a5: a6 --/-> a4. 第 2 行的括号是错误的。

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> (g::a5 (f::a2 x::a3 g::a5)::a6)::a7)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a7
a4 = a5 -> a7

a1 = (a3 -> a5 -> a6) -> a3 -> a4
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> a5 -> a7
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> (a6 -> a7) -> a7

因此，这是 h 的正确类型（您可以通过输入 fun hfx = (fn g => g (fxg) 来检查您是否偏执) ) 进入 SML 提示并获得完全相同的结果；对于具有适当语法的 Haskell 来说也是如此）。 h 是一个多态函数，因此所有的 a 都是任意的，但表达了 h 的参数类型与应用 h 的结果的参数之间的关系等等。

You've made a mistake. g=a5: a6 -/-> a4. Your brackets are wrong on line 2.

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> (g::a5 (f::a2 x::a3 g::a5)::a6)::a7)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a7
a4 = a5 -> a7

a1 = (a3 -> a5 -> a6) -> a3 -> a4
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> a5 -> a7
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> (a6 -> a7) -> a7

That is therefore the correct type for h (you can check if you're paranoid just by typing fun h f x = (fn g => g (f x g) ) into an SML prompt and getting the exact same result; same goes for Haskell with appropriate syntax). h is a polymorphic function, so all the a's are arbitrary, but express the relationship between the types of h's argument and the argument of the result of applying h and so on.

回复收藏 0 原文

~没有更多了~