Come posso definire il combinatore y senza "let rec"?

Question

In quasi tutti gli esempi, un combinatore y nei linguaggi di tipo ML è scritto in questo modo:

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

Funziona come previsto, ma sembra un imbroglio definire l'utilizzo del combinatore y let rec ....

Voglio definire questo combinatore senza usare la ricorsione, usando 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# si lamenta di non riuscire 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 scrivo il combinatore y in F# senza usare let rec ...?

Answer 1

Come sottolinea il compilatore, non v'è alcun tipo che può essere assegnato a x in modo che il (x x) espressione è ben digitato (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 che questo non è molto utile in quanto F # è un linguaggio rigoroso, in modo che qualsiasi funzione che si tenta di definire utilizzare questo combinatore causerà un overflow 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, si 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 utilizzando boxe e 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 non sarà mai effettivamente portare al fallimento in fase di esecuzione.

Answer 2

Direi che è impossibile, e ha chiesto perché, mi handwave e invocare il fatto che semplicemente digitato lambda calcolo ha il la normalizzazione di proprietà . In breve, tutti i termini del lambda calcolo semplicemente digitato terminano (Y conseguentemente non può essere definito nel lambda calcolo semplicemente digitato).

tipo di sistema 's F # non è esattamente il tipo di sistema di lambda calcolo semplicemente digitato, ma è abbastanza vicino. F #, senza let rec arriva davvero vicino al lambda calcolo semplicemente digitato - e, per ribadire, in quella lingua non è possibile definire un termine che non pone fine, e che esclude la definizione di Y troppo.

In altre parole, in F #, "let rec" deve essere un linguaggio primitivo per lo meno, perché anche se tu fossi in grado di definire dalle altre primitive, non si sarebbe in grado di digitare questa definizione. Avendo come un primitivo si permette, tra le altre cose, di dare un tipo speciale a quella primitiva.

EDIT: KVB mostra nella sua risposta che le definizioni di tipo (una delle caratteristiche assenti dalla lambda-calcolo semplicemente digitato ma presenti in let-rec-meno F #) permettono di ottenere una sorta di ricorsione. Molto intelligente.

Answer 3

Le istruzioni Case e Let nei derivati ​​ML sono ciò che lo rende Turing Complete, credo che siano basati sul Sistema F e non semplicemente digitati, ma il punto è lo stesso.

Il sistema F non riesce a trovare un tipo per qualsiasi combinatore di punto fisso, se potesse, non era fortemente normalizzante.

Ciò che significa fortemente normalizzante è che qualsiasi espressione ha esattamente uno forma normale, dove una forma normale è un'espressione che non può essere ulteriormente ridotta, questo differisce da untyped dove ogni espressione ha al massimo una forma normale, può anche non avere alcuna forma normale.

Se i lambda calcoli digitati potessero costruire un operatore di punto fisso in qualsiasi modo, sarebbe del tutto possibile che un'espressione non abbia una forma normale.

Un altro famoso teorema, l’Halting Problem, implica che i linguaggi fortemente normalizzanti non sono Turing completi, dice che è impossibile decidere (diverso da dimostrare) di un linguaggio completo quale sottoinsieme dei suoi programmi si fermerà su quale input.Se una lingua è fortemente normalizzatrice, è possibile decidere se si ferma, cioè se si ferma Sempre si ferma.Il nostro algoritmo per decidere questo è il programma: true;.

Per risolvere questo problema, i derivati ​​​​ML estendono System-F con case e lasciano (rec) per superare questo problema.Le funzioni possono quindi fare nuovamente riferimento a se stesse nelle loro definizioni, rendendole in effetti non più lambda calcoli, non è più possibile fare affidamento solo su funzioni anonime per tutte le funzioni calcolabili.Possono così entrare di nuovo in cicli infiniti e ritrovare la loro completezza turing.

Answer 4

Risposta breve:. Non è possibile

Risposta lunga: Il lambda calcolo semplicemente digitato è fortemente normalizzante. Ciò significa che non di Turing equivalente. La ragione di questo si riduce in sostanza al fatto che un combinatore Y deve essere o primitiva o definite in modo ricorsivo (come hai trovato). Semplicemente non può essere espresso in (più semplice dattiloscritta calcoli o) Sistema F. Non c'è modo per aggirare questo (è stato dimostrato, dopo tutto). La Y Combinator possono implementare lavori esattamente nel modo desiderato, però.

Vorrei suggerire di provare schema se si vuole un vero e proprio stile di Y Combinator-Chiesa. Utilizzare la versione applicativa di cui sopra, come le altre versioni non funzionerà, a meno che non si aggiunge in modo esplicito la pigrizia, o utilizzare un interprete Scheme pigro. (Schema tecnicamente non è del tutto priva di tipo, ma è dinamicamente tipizzato, che è abbastanza buono per questo.)

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

Dopo aver riflettuto un po ', sono abbastanza sicuro che l'aggiunta di un combinatore Y primitiva che si comporta esattamente come il letrec definito lo fa rende Sistema F Turing completo. Tutto quello che devi fare per simulare una macchina di Turing poi è applicare il nastro come un intero (interpretato in binario) e uno spostamento (per posizionare la testa).