Проблема лямбда-исчисления - PullRequest
Новая
       9

Проблема лямбда-исчисления

2 голосов
/ 31 августа 2011

Я должен решить проблему лямбда-исчисления. Я достиг определенной точки, и я не знаю, как продолжить: 

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 и так далее. Я не знаю, достаточно ли это ясно ...

Спасибо большое !!

1 Ответ

3 голосов
/ 31 августа 2011

Вы сделали ошибку. 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 h f x = (fn g => g (f x g) ) в приглашении SML и получив точно такой же результат; то же самое относится и к Haskell с соответствующим синтаксисом). h является полиморфной функцией, поэтому все а являются произвольными, но выражают связь между типами аргумента h и аргументом результата применения h и т. д.

...