Определить комбинацию фиксированных точек в продолжении Проходной стиль

fix-point combinators - очень полезные инструменты для введения рекурсии.
Continuation-Passing style - это стиль исчисления лямбда, функции которого никогда не возвращаются. Вместо этого вы передаете остальную часть своей программы в качестве аргумента лямбда в вашу функцию и продолжаете ее. Это позволяет вам лучше контролировать поток выполнения и более легко определять различные конструкции, изменяющие поток (петли, сопрограммы и т. Д.)

Тем не менее, мне интересно, можете ли вы выразить один в другом? Все языки CPS-типа, которые я видел, имеют явную конструкцию FIX для определения рекурсии.Определить комбинацию фиксированных точек в продолжении Проходной стиль

Это потому, что невозможно определить комбинатор фиксированной точки (или аналогичный) в простой CPS, без FIX? Если да, то знаете ли вы доказательства такого?
Или это из-за типизации проблем?
Возможно, возможно, но по какой-то причине непрактично?
Или я просто не нашел решение, которое там ...?

Я бы ожидать Y-комбинатора, как функции CPS CPSY работать следующим образом: Если я определяю Y-готовую функцию CPS, такие как:

function Yready(this, return) = 
    return (lambda <args> . <body using 'this' as recursion>);

Я бы затем положить его в CPSY производить функцию, которая рекурсивно в себя:

function CPSY(F, return) = ????? 

CPSY(Yready, 
    lambda rec . <body where 'rec' names 'lambda <args>' from above, but with the loop closed> 
)

CPSY должна быть простой функцией продолжающей переход стиль без сам, опираясь на любой рекурсии. Y-комбинатор может быть определен таким образом в простом лямбда-исчислении без встроенной рекурсии. Может ли она существовать и в некоторой форме в CPS?

Повторим разъяснений: Я ищу комбинатора, как функции CPSY, что:

позволило бы рекурсию функций СУЗ
Определение этого не опирается на рекурсии
Определение его дано в стиле продолжения (без возврата лямбда в любом месте тела CPSY)

источник

2016-03-10 CygnusX1

"...IOW, без использования 'letrec' в любой форме, только' let' (в терминах Scheme). «Я считаю, что это то, что вы имеете в виду. Интересный вопрос ... –

Это «тривиальное решение», а не нерекурсивное, которое требуется OP - его оставляют для сравнения.

Если у вас есть язык, обеспечивающий рекурсивные привязки, вы можете определить fix для функций СУЗ (здесь с помощью Haskell):

Prelude> let fixC f = \c -> f (fixC f c) c 
Prelude> :t fixC 
fixC :: (t -> t1 -> t) -> t1 -> t 
Prelude> let facC' = \rec c n -> if n == 0 then c 1 else c (n * rec (n-1)) 
Prelude> let facC = fixC facC' 
Prelude> take 10 $ map (facC id) [1..10] 
[1,2,6,24,120,720,5040,40320,362880,3628800]

Возможно предоставление fixC как примитив влияет на производительность, хотя (если у вас есть продолжения, представленные не просто как замыкания), либо связано с тем, что «традиционное» лямбда-исчисление не имеет имен для функций, которые могут быть использованы рекурсивно.

(Возможно, есть и более эффективный вариант аналогичен fix f = let x = f x in x.)

источник

2016-03-10 19:11:01 phg

Рекурсивное связывание действует как встроенный комбинатор исправлений. это некоторые из них более явны (например, 'let' vs' letrec'). Однако я ищу решение, которое не полагается на встроенную 'FIX' в любой форме. Y-combinator можно определить с помощью средства равного лямбда-исчисления, а также фактические языки, которые моделируют исчисление. Но можно ли это сделать в CPS? – CygnusX1

Отредактировал вопрос, чтобы сделать себя немного более понятным :) – CygnusX1

@ CygnusX1 А теперь я знаю, после. Это, безусловно, более интересно, но я оставлю ответ. – phg

TL; DR: applictive же порядка Y работы для СУЗ функций, написанных на продолжение-кэрри стиле.

В комбинаторной стиле, обычное определение факториала с Y, конечно,

_Y (\r -> \n -> { n==0 -> 1 ; n * r (n-1) })  , where 
           ___^______ 
_Y = \g -> (\x-> x x) (\x-> g (\n-> x x n)) -- for applicative and normal order

КПС определения факториала

fact = \n k -> equals n 0   -- a conditional must expect two contingencies 
       (\True -> k 1) 
       (\False -> decr n 
           (\n1-> fact n1   -- *** recursive reference 
              (\f1-> mult n f1 k)))

CPS- Y увеличивается для дополнительного непредвиденных расходов аргумент (я говорю «cont чтобы «устранить несогласие с истинными продолжениями». In Scheme,

(define (mult a b k)  (k (* a b))) 
(define (decr c k)  (k (- c 1))) 
(define (equals d e s f) (if (= d e) (s 1) (f 0))) 

(((lambda (g) 
    ((lambda (x) (x x)) 
     (lambda (x) (g (lambda (n k) ((x x) n k)))))) 

    (lambda (fact) 
    (lambda (n k) 
     (equals n 0 (lambda (_) (k 1)) 
        (lambda (_) (decr n 
           (lambda (n1) (fact n1 
               (lambda (f1) (mult n f1 k)))))))))) 

    5 (lambda (x) (display x)))

This returns 120.

Конечно же, на этом языке, который является стандартным языком, но не обозначенным в тексте, эта ссылка на CPS-Y равна точно так же, как и обычный Y сам.

Но что, если наша рекурсивная функция имеет два действительных параметра и продолжение ⁄ непредвиденные расходы — третья? На языке, подобном Схеме, должен ли мы иметь еще один Y, а внутри (lambda (n1 n2 k) ((x x) n1 n2 k))?

Мы можем всегда включать аргумент непредвиденных обстоятельств и всегда указывать код в карри (каждая функция имеет ровно один аргумент, возможно, производя другую такую функцию или, наконец, конечный результат). И it works тоже:

(define (mult k) (lambda (x y) (k (* x y)))) 
(define (decr k) (lambda (x) (k (- x 1)))) 
(define (equals s f) (lambda (x y) (if (= x y) (s) (f)))) 

((((lambda (g)        ; THE regular, 
    ((lambda (x) (x x))      ; applicative-order 
     (lambda (x) (g (lambda (k) ((x x) k)))))) ; Y-combinator 

    (lambda (fact) 
    (lambda (k) 
     (lambda (n) 
     ((equals (lambda() (k 1)) 
        (lambda() ((decr (lambda (n1) 
             ((fact 
              (lambda (f1) ((mult k) n f1))) 
             n1))) 
           n))) 
      n 0))))) 

    (lambda (x) (display x))) 
    5)

Есть способы to type such a thing тоже, если ваш язык набирается. Или, в нетипизированном языке, мы могли бы собрать все аргументы в списке.

источник

2016-03-11 01:14:57

Исправьте меня, если я ошибаюсь, но я думаю, вы говорите об использовании функции Y-combinator * для * CPS. Я прошу определить сам комбинатор * * CPS. '\ G -> (\ x-> xx) (\ x-> g (\ nk -> (xx) nk))' не является функцией CPS. – CygnusX1

Да, я тоже об этом думал. но, что мешает нам определять '(CPSY k) f = k (Y f)'? –

Я имею в виду, позволяет ли ваш гипотетический язык использовать лямбды? Лямбда-функция возвращает результат непосредственно, а не через продолжение. Или ваш язык запрещает лямбды? Я думаю, что здесь нужны более специфические особенности; как ваш вопрос немного расплывчатый в этом отношении. Вы говорите о языках CPS. Я не знаком ни с одним из таких языков; Я знаком с методикой программирования CPS, дисциплиной программирования CPS ... AFAIK любая функция может быть преобразована механически в CPS; так что Y тоже может показаться. –

Anonymous Рекурсия в продолжении обходя стиль может быть сделана следующим образом (с использованием JS6 в качестве языка):

// CPS wrappers 
const dec = (n, callback)=>{ 
    callback(n - 1) 
} 
const mul = (a, b, callback)=>{ 
    callback(a * b) 
} 
const if_equal = (a, b, then, else_)=>{ 
    (a == b ? then : else_)() 
} 

// Factorial 
const F = (rec, n, a, callback)=>{ 
    if_equal(n, 0, 
     ()=>{callback(a)}, 
     ()=>{dec(n, (rn)=>{ 
      mul(a, n, (ra)=>{ 
       rec(rec, rn, ra, callback) 
      }) 
     }) 
    }) 
} 

const fact = (n, callback)=>{ 
    F(F, n, 1, callback) 
} 

// Demo 
fact(5, console.log)

Чтобы избавиться от двойного использования этикетки F, мы можем использовать функцию полезности как так :

const rec3 = (f, a, b, c)=>{ 
    f(f, a, b, c) 
} 
const fact = (n, callback)=>{ 
    rec3(F, n, 1, callback) 
}

Это позволяет встраивать F:

const fact = (n, callback)=>{ 
    rec3((rec, n, a, callback)=>{ 
     if_equal(n, 0, 
      ()=>{callback(a)}, 
      ()=>{dec(n, (rn)=>{ 
       mul(a, n, (ra)=>{ 
        rec(rec, rn, ra, callback) 
       }) 
      }) 
     }) 
    }, n, 1, callback) 
}

мы можем перейти к строковым rec3 сделать fact selfcontained:

const fact = (n, callback)=>{ 
    ((f, a, b, c)=>{ 
     f(f, a, b, c) 
    })((rec, n, a, callback)=>{ 
     if_equal(n, 0, 
      ()=>{callback(a)}, 
      ()=>{dec(n, (rn)=>{ 
       mul(a, n, (ra)=>{ 
        rec(rec, rn, ra, callback) 
       }) 
      }) 
     }) 
    }, n, 1, callback) 
}

Следующий JavaScript использует тот же подход, чтобы реализовать цикл.

const for_ = (start, end, func, callback)=>{ 
    ((rec, n, end, func, callback)=>{ 
     rec(rec, n, end, func, callback) 
    })((rec, n, end, func, callback)=>{ 
     func(n,()=>{ 
      if_equal(n, end, callback,()=>{ 
       S(n, (sn)=>{ 
        rec(rec, sn, end, func, callback) 
       }) 
      }) 
     }) 
    }, start, end, func, callback) 
}

Это часть полностью асинхронного FizzBuzz я сделал https://gist.github.com/Recmo/1a02121d39ee337fb81fc18e735a0d9e

источник

2017-02-01 09:02:09 Remco

Давайте выведут сначала КПС-Y для оценки нормального порядка в лямбда-исчислении, а затем преобразовать его в Аппликативный заказе.

Wikipedia page определяет фиксированной запятой комбинатора Y по следующему уравнению:

Y f = f (Y f)

В форме КПС, это уравнение будет выглядеть скорее так:

Y f k = Y f (λh. f h k)

Теперь рассмотрим следующий не КПС определение нормального порядка Y:

Y f = (λg. g g) (λg. f (g g))

Преобразуйте его в CPS:

Y f k = (λg. g g k) (λg.λk. g g (λh. f h k))

Теперь, бета-свертка Это определение несколько раз, чтобы проверить, что это действительно удовлетворяет «CPS с фиксированной точкой» состояние выше:

Y f k = (λg. g g k) (λg.λk. g g (λh. f h k)) 
     = (λg.λk. g g (λh. f h k)) (λg.λk. g g (λh. f h k)) k 
     = (λg.λk. g g (λh. f h k)) (λg.λk. g g (λh. f h k)) (λh. f h k) 
     = Y f (λh. f h k)

Voila!

Теперь, для оценки прикладного заказа, конечно, нам нужно немного изменить это. Аргументация здесь такая же, как и в не-КПС случае: мы должны «санк» рекурсивное (g g k) вызов и перейти только при вызове в следующий раз:

Y f k = (λg. g g k) (λg.λk. f (λx.λk. g g (λF. F x k)) k)

Вот прямая трансляция в Ракетка:

(define (Y f k) 
    ((λ (g) (g g k)) 
    (λ (g k) (f (λ (x k) (g g (λ (F) (F x k)))) k))))

Мы можем проверить, что это на самом деле работает - например, вот рекурсивное вычисление треугольного числа в КПСЕ (для арифметических операций, за исключением, для простоты):

(Y (λ (sum k) (k (λ (n k) (if (< n 1) 
           (k 0) 
           (sum (- n 1) (λ (s) (k (+ s n)))))))) 
    (λ (sum) (sum 9 print))) 
;=> 45

Я считаю, что это отвечает на вопрос.

источник

2017-05-03 06:55:48 eush77

Определить комбинацию фиксированных точек в продолжении Проходной стиль

ответ

Смежные вопросы