Definire il combinatore di punti fissi in Continuation Passing Style

I fix-point combinators sono strumenti molto utili per introdurre la ricorsione.
Lo Continuation-Passing style è uno stile di lambda calcolo in cui le funzioni non ritornano mai. Invece passi il resto del tuo programma come argomento lambda nella tua funzione e prosegui attraverso di essi. Ti permette di avere un controllo migliore sul flusso di esecuzione e più facilmente definire vari costrutti che alterano il flusso (loop, coroutine, ecc ...)

Tuttavia, mi chiedo se è possibile esprimere uno in un altro? Tutti i linguaggi in stile CPS che ho visto hanno un costrutto esplicito FIX per definire la ricorsione.Definire il combinatore di punti fissi in Continuation Passing Style

È perché è impossibile definire un combinatore di punto di correzione (o simile) in CPS semplice, senza FIX? Se è così, conosci la prova di una cosa del genere?
Oppure a causa di problemi di digitazione?
O forse è possibile, ma per qualche motivo non pratico?
O semplicemente non ho trovato una soluzione che è là fuori ...?

ci si aspetterebbe un Y-combinatore come funzione CPS CPSY a lavorare come questo: Se definisco una funzione CPS Y-ready, come ad esempio:

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

avrei poi messo in CPSY per produrre una funzione che recurses in sé:

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

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

Il CPSY dovrebbe essere una funzione semplice stile continuazione-passing senza prendere affidamento su qualsiasi rec ursion. Il combinatore Y può essere definito in modo simile al calcolo lambda senza ricorsione incorporata. Può esistere, in qualche modo, anche in CPS?

Per ribadire un chiarimento: Sto cercando una funzione combinatore simile CPSY che:

consentirebbe ricorsione di funzioni di CPS
La definizione di esso non si basa su ricorsione
La definizione di esso è data in stile passaggio continuo (nessun ritorno lambda in qualsiasi parte all'interno del corpo di CPSY)

fonte

2016-03-10 CygnusX1

"...IOW, senza usare 'letrec' in nessuna forma, solo' let' (in termini Scheme). "Credo che sia quello che intendi. Interessante domanda ... –

Questa è la "soluzione banale", non quella non ricorsiva che l'OP voleva - è lasciata al confronto.

Se si dispone di un linguaggio che fornisce binding ricorsive, è possibile definire fix per le funzioni di CPS (qui utilizzando 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]

Forse fornendo fixC come un primitivo ha implicazioni di prestazioni, anche se (se avete continuazione rappresentata non semplicemente come chiusure), o è dovuta al fatto che il calcolo lambda "tradizionale" non ha nomi per funzioni che possono essere usate in modo ricorsivo.

(Probabilmente c'è anche una variante più efficiente analogo a fix f = let x = f x in x.)

fonte

2016-03-10 19:11:01 phg

Un binding ricorsivo agisce come un combinatore di correzioni incorporato. alcuni sono più espliciti (es. 'let' vs' letrec'). Tuttavia, sto cercando una soluzione che non faccia affidamento su un 'FIX' incorporato in alcuna forma. il mezzo del semplice calcolo lambda, così come i linguaggi reali che modellano il calcolo, ma può essere fatto in CPS? – CygnusX1

Modificato la domanda per rendermi un po 'più chiaro :) – CygnusX1

@ CygnusX1 Ah, ora so cosa sei dopo .Questo è certamente più interessante.Mi lascerò la risposta, però. – phg

TL; DR: stesso applictive ordine Y opere per funzioni CPS scritte in stile continuation curry.

In stile combinatorio, l'usuale definizione di fattoriale Y è, naturalmente,

_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

CPS definizione fattoriale è

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 viene aumentata per l'argomento supplementare (sto dicendo " contingenza "per disambiguare dalle vere continuazioni). Nello Schema,

(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.

Naturalmente in un linguaggio pigro auto-currying (ma non tipizzato!) Di eta-contrazione della sopra CPS-Y è esattamente lo stesso del normale Y sé.

Ma cosa succede se la nostra funzione ricorsiva ha due parametri effettivi e la continuazione ⁄ contingenza — il terzo? In linguaggio simile a Scheme, dovremmo avere un altro Y allora, con il (lambda (n1 n2 k) ((x x) n1 n2 k)) all'interno?

Possiamo passare ad avere sempre l'argomento contingenza primo, e sempre il codice in modo curry (ogni funzione ha esattamente un argomento, possibilmente producendo un altro tale funzione, oppure un risultato finale dopo tutto sono applicati). E it works, troppo:

(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)

ci sono modi to type such a thing, anche se la lingua viene digitato. Oppure, in un linguaggio non tipizzato, potremmo impacchettare tutti gli argomenti in una lista, forse.

fonte

2016-03-11 01:14:57

Correggimi se sbaglio, ma penso che tu parli dell'uso di Y-combinator * per la funzione * CPS. Sto chiedendo un combinatore stesso definito * in * CPS. '\ G -> (\ x-> xx) (\ x-> g (\ nk -> (xx) nk))' non è una funzione CPS. – CygnusX1

sì, stavo pensando anche a questo. ma, cosa ci impedisce di definire '(CPSY k) f = k (Y f)'? –

Voglio dire, il tuo linguaggio ipotetico consente assolutamente il lambda? Una funzione lambda restituisce il risultato direttamente, non attraverso una continuazione. O è la tua lingua che vieta i lambda? Penso che siano necessari più dettagli qui; come richiesto la tua domanda è un po 'vaga a riguardo. Parli di "lingue CPS". Non ho familiarità con nemmeno una di queste lingue; Ho familiarità con una tecnica di programmazione CPS, una disciplina di programmazione CPS ... AFAIK qualsiasi funzione può essere convertita meccanicamente in CPS; così anche Y può farlo, sembra. –

Anonymous ricorsione in continuazione-passing-stile può essere fatto come segue (utilizzando JS6 come lingua):

// 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)

per sbarazzarsi del duplice uso di etichette F, possiamo usare una funzione di utilità in questo modo :

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

Questo ci permette di INLINE 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) 
}

Possiamo procedere inline rec3 per rendere 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) 
}

Il seguente JavaScript utilizza lo stesso approccio per implementare un ciclo for.

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) 
}

Fa parte del FizzBuzz completamente asincrono feci https://gist.github.com/Recmo/1a02121d39ee337fb81fc18e735a0d9e

fonte

2017-02-01 09:02:09 Remco

Let primo derivare CPS-Y per la valutazione normale ordine in lambda calcolo, e poi convertirlo applicativo-ordine.

Wikipedia page definisce-punto fisso combinatore Y dalla seguente equazione:

Y f = f (Y f)

Nella forma CPS, questa equazione sarebbe piuttosto simili:

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

Ora, si consideri il seguente non CPS definizione dell'ordine normale di Y:

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

Trasformalo in CPS:

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

Ora, beta-ridurre questa definizione un paio di volte per verificare che soddisfi effettivamente il “punto fisso-CPS” condizione di cui sopra:

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!

Ora, per la valutazione applicativa-ordine, naturalmente, ci sarebbe bisogno di cambiare questo un po '. Il ragionamento è lo stesso che nel caso in cui non CPS: abbiamo bisogno di “thunk” il ricorsivo (g g k) chiamata e procedere solo quando viene chiamato per la prossima volta:

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

Ecco una traduzione diretta in Racket:

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

possiamo controllare che effettivamente funziona - per esempio, ecco la ricorsivo triangolare calcolo numero in CPS (tranne le operazioni aritmetiche, per semplicità):

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

Credo che questo risponda alla domanda.

fonte

2017-05-03 06:55:48 eush77

Definire il combinatore di punti fissi in Continuation Passing Style

risposta

Problemi correlati