Рекурсивные лямбда в Haskell

Question

Давайте посмотрим, анализировать код для факториала в Haskell, используя функцию лямбда:

y f x = f (y f) x 

factorial = y (\t n -> if n == 1 then 1 else n * t(n-1)) 

И я не могу понять, как это работает. Я знаю, что это связано с исчислением лямбда, но в настоящее время я не знаком с этим, поэтому я должен понимать без него или с минимальными знаниями. Мое сомнение есть: Что такое f в определении factorial? Я имею в виду это f: y f x = f (y f) x.

Итак, что здесь? y (\ t n -> if n == 1 then 1 else n * t (n-1))

Пожалуйста, объясните мне, что, возможно, рекурсия?

Answer 1

f в factorial является (\t n -> if n == 1 ...)лямбда

y является так называемая fix-point combinator и используется для того, чтобы рекурсивные определения в лямбда-исчислении (это относится f к, это аргумент снова и снова рекурсивно)

, чтобы понять, как это работает, вы можете просто сделать некоторые оценки вручную:

factorial 3 
= y (\t n -> ...) 3 
{ def y and y (\t n -> ...) = factorial by eta-red. } 
= (\t n -> ...) factorial 3 
{ t = factorial, n = 3 -> else case } 
= 3 * factorial 2 
= 3 * (y (\t n -> ...) 2) 
= 3 * ((\t n -> ...) factorial 2) 
= { t = factorial, n = 2 -> else case } 
= 3 * (2 * factorial 1) 
= 3 * (2 * (y (\t n -> ...) 1)) 
= 3 * (2 * ((\t n -> ...) factorial 1))) 
{ t = factorial n = 1 -> then case } 
= 3 * (2 * 1) 
= 6 

Answer 2

y - fixed-point combinator, также известный как y-combinator. В

factorial = y (\t n -> if n == 1 then 1 else n * t(n-1)) 

лямбда (\t n -> if n == 1 then 1 else n * t(n-1)) обязан f в определении y. Вы можете сделать расширение:

(\t n -> if n == 1 then 1 else n * t(n-1)) (y (\t n -> if n == 1 then 1 else n * t(n-1))) 

так внутри лямбда, t будет связано с самой лямбды, что позволяет ему называть себя рекурсивно.

Answer 3

Возможно, это легче, если вы выписывать у комбинатор, таким образом, с двумя ETA-расширений:

y :: ((a->b) -> a->b) -> a->b 
y f x a = f (\q a' -> y f q a') x a 

Так f в основном получает рекурсивный вызов (с a' вместо a) в качестве первого аргумента ,