Lambda calculus problem

Question

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!!

Answer 1

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.