Come si definisce y-combinator senza "let rec"?

Question

In quasi tutti gli esempi, una y-Combinator in lingue ML-tipo è scritto così:

let rec y f x = f (y f) x 
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1)) 

Questo funziona come previsto, ma ci si sente come barare a definire la y-combinatore utilizzando let rec ....

voglio definire questa Combinator senza usare la ricorsione, utilizzando la definizione standard:

Y = λf·(λx·f (x x)) (λx·f (x x)) 

una traduzione diretta è la seguente:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));; 

Tuttavia, F # lamenta che non riesco a capire i tipi:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));; 
    --------------------------------^ 

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a 
    'a  
but given a 
    'a -> 'b  
The resulting type would be infinite when unifying ''a' and ''a -> 'b' 

Come faccio a writ e il combinatore y in F # senza usare let rec ...?

Answer 1

Come il compilatore fa notare, non v'è alcun tipo che può essere assegnato a x in modo che l'espressione (x x) è ben tipizzato-(questo non è del tutto vero, è possibile digitare esplicitamente x come obj->_ - vedere il mio ultimo paragrafo) . È possibile aggirare il problema dichiarando un tipo ricorsivo in modo che un'espressione molto simile funzionerà:

type 'a Rec = Rec of ('a Rec -> 'a) 

Ora la Y-Combinator può essere scritta come:

let y f = 
    let f' (Rec x as rx) = f (x rx) 
    f' (Rec f') 

Purtroppo, troverete questo non è molto utile perché F # è un linguaggio rigoroso, , quindi qualsiasi funzione che si tenta di definire utilizzando questo combinatore causerà un sovraccarico dello stack. Invece, è necessario utilizzare la versione applicativa di ordine inferiore del Y-Combinator (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f = 
    let f' (Rec x as rx) = f (fun y -> x rx y) 
    f' (Rec f') 

Un'altra opzione sarebbe quella di utilizzare la pigrizia esplicito per definire il normale ordine Y-Combinator:

type 'a Rec = Rec of ('a Rec -> 'a Lazy) 
let y f = 
    let f' (Rec x as rx) = lazy f (x rx) 
    (f' (Rec f')).Value 

Questo ha lo svantaggio che le definizioni di funzioni ricorsive devono ora una forza esplicita del valore pigro (utilizzando la proprietà Value):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1))) 

Tuttavia, ha il vantaggio che è possibile definire i valori ricorsive non funzione, proprio come si potrebbe in un linguaggio pigro:

let ones = y (fun ones -> LazyList.consf 1 (fun() -> ones.Value)) 

Come alternativa finale, si può provare a approssimare meglio il lambda calcolo tipizzato dal usando il pugilato e il downcasting. Questo darebbe (sempre utilizzando la versione applicativa di ordine inferiore del Y-Combinator):

let y f = 
    let f' (x:obj -> _) = f (fun y -> x x y) 
    f' (fun x -> f' (x :?> _)) 

Questo ha lo svantaggio ovvio che causerà la boxe non necessari e unboxing, ma almeno questo è del tutto interno alla realizzazione e in realtà non porterà mai a un errore in fase di runtime.

Answer 2

Direi che è impossibile, e ho chiesto il motivo per cui avrei fatto il handwave e ho invocato il fatto che il semplice lambda calcolo ha il normalization property. In breve, tutti i termini del calcolo lambda tipizzato semplicemente terminano (di conseguenza, Y non può essere definito nel calcolo lambda semplicemente digitato).

Il sistema di tipo F # non è esattamente il tipo di sistema di lambda calcolo semplice, ma è abbastanza vicino. F # senza let rec si avvicina molto al semplice lambda calcolo - e, per reiterare, in quel linguaggio non è possibile definire un termine che non termina, e che esclude anche la definizione di Y.

In altre parole, in F #, "let rec" deve essere almeno una primitiva del linguaggio, perché anche se fosse possibile definirlo dalle altre primitive, non sarebbe possibile digitare questa definizione. Avere una primitiva ti permette, tra le altre cose, di dare un tipo speciale a quel primitivo.

MODIFICA: kvb mostra nella sua risposta che le definizioni di tipo (una delle caratteristiche assenti dal lambda-calculus semplicemente dattilografato ma presente in F # senza scrittura) consentono di ottenere una sorta di ricorsione. Molto intelligente.

Answer 3

Case e let dichiarazioni in derivati ​​ML sono ciò che rende Turing Complete, credo che siano basate su System F e non semplicemente digitate, ma il punto è lo stesso.

Il sistema F non riesce a trovare un tipo per qualsiasi combinatore di punti fissi, se così fosse, non si stava normalizzando fortemente.

mezzi Nei fortemente normalizzazione è che ogni espressione ha esattamente un forma normale, in cui una forma normale è un'espressione che non può essere ridotta ulteriormente, questo differisce da untyped dove ogni espressione ha dur una forma normale, può anche non avere alcuna forma normale.

Se i calcoli lambda digitati potevano costruire un operatore a punto fisso in qualunque modo, era possibile che un'espressione non avesse una forma normale.

Un altro famoso teorema, l'arresto problema, implica che i linguaggi fortemente normalizzazione non sono Turing completa, si dice che è impossibile decidere (diverso da dimostrare) di un linguaggio completo Turing quanto sottoinsieme dei suoi programmi si ferma su ciò che di ingresso . Se una lingua è fortemente normalizzata, è decidibile se si ferma, vale a dire sempre fermate. Il nostro algoritmo per decidere questo è il programma: true;.

Per risolvere questo problema, i derivati ​​ML estendono System-F con case e let (rec) per superare questo problema. Le funzioni possono quindi riferirsi di nuovo a se stesse nelle loro definizioni, non rendendole più effettive, quindi non è più possibile fare affidamento solo su funzioni anonime per tutte le funzioni computabili. Possono così di nuovo entrare in loop infiniti e riguadagnare la loro completezza.

Answer 4

Risposta breve: non è possibile.

Risposta lunga: Il calcolo lambda è semplicemente normalizzato. Ciò significa che non è equivalente a Turing. La ragione di ciò si riduce fondamentalmente al fatto che un combinatore Y deve essere primitivo o definito in modo ricorsivo (come hai trovato).Semplicemente non può essere espresso in System F (o più semplici calcoli dattiloscritti). Non c'è modo di aggirare questo (è stato dimostrato, dopo tutto). Il combinatore Y si può implementare funziona esattamente nel modo desiderato, però.

Ti suggerisco di provare lo schema se vuoi un vero combinatore Y in stile Chiesa. Utilizzare la versione applicativa fornita sopra, poiché le altre versioni non funzioneranno, a meno che non si aggiunga esplicitamente la pigrizia o si usi un interprete di schema pigro. (Schema non è tecnicamente del tutto tipizzato, ma è dinamicamente tipizzato, che è abbastanza buono per questo.)

vedere questo per la prova della normalizzazione forte: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

Dopo averci pensato un po ', io sono abbastanza certo che l'aggiunta di un combinatore Y primitivo che si comporta esattamente come viene definito da letrec, rende System F Turing completo. Tutto quello che devi fare per simulare una macchina di Turing è implementare il nastro come un intero (interpretato in binario) e uno spostamento (per posizionare la testa).