Я впервые написал решение в нетипизированном лямбда-исчислении, используя определения верхнего уровня для таких вещей, как ноль? , true , false и т. Д., Определеноиспользуя церковные кодировки.В этой реализации предполагается, что функции с несколькими аргументами каррируются и функции частично применяются (например, Haskell).
Церковное кодирование натуральных чисел выглядит следующим образом:
(define 0 λf x. x)
(define 1 λf x. f x)
(define 2 λf x. f (f x))
(define 3 λf x. f (f (f x)))
Церковные логические значения true и false определены ниже
(define const λx y. x)
(define U λf. f f)
(define true λt f. t)
(define false λt f. f)
(define succ λn f x. f (n f x))
(define 0 λf x. x)
(define * λm n f x. m (n f) x)
(define zero? λn. n (const false) true)
(define pred λn f x. n (λg h. h (g f)) (const x) id)
После того, как эти предварительные условия определены, теперь мы определяем факториальную функцию, используя самоприменение для рекурсии.Это определение является хвостово-рекурсивным.
(define !
U (lambda loop acc n.
zero? n -- branches wrapped in lambdas
-- to accomodate call-by-value
(lambda _. acc)
(lambda _. (loop loop (* n acc) (pred n))))
n) -- dummy argument to evaluate selected branch
1)
Отсюда я обманул и выполнил обычную оценку порядка на !;это по сути частичная оценка.Чтобы это работало, мне пришлось удалить определение U, чтобы предотвратить расхождение, а затем добавить его обратно после.
Вот результирующий термин.Это довольно загадочно (хотя мне было бы трудно написать что-то такое короткое от руки, без переводчика), поэтому я добавил комментарии, идентифицирующие части, которые я все еще могу распознать.
(λx. x x) -- self application
(λloop acc n.
n (λy t f. f) -- const false
(λt f. t) -- true
(λ_. acc) -- zero? branch
(λ_. loop loop -- other branch
(λf. n (acc f))
(λf x. n (λg h. h (g f)) (λy. x) (λx. x))) -- pred
n) -- dummy argument
(λf. f) -- 1
Умножение может бытьтрудно заметить, но это есть.Теперь, чтобы проверить это, я оценил термин, примененный к 3, или (λf x. f (f (f x))).Гибридная аппликативная и гибридная нормальная оценка приводят к нормальному сроку без отклонения, приводя к λf x. f (f (f (f (f (f x))))) или 6. Другие стратегии сокращения либо расходятся (из-за самостоятельного применения), либо не приводят к нормальной форме.