Y Combinator: Alcune funzioni non hanno punti fissi

Question

Il Wikipedia article on the Y combinator fornisce la seguente implementazione JavaScript del combinatore Y:

function Y(f) { 
    return (
     (function (x) { 
      return f(function (v) { return x(x)(v); }); }) 
     (function (x) { 
      return f(function (v) { return x(x)(v); }); }) 
    ); 
} 

L'esistenza di un combinatore Y in JavaScript dovrebbe implicare che ogni funzione JavaScript ha un punto fisso (poiché per ogni funzione g, Y(g) e g(Y(g)) dovrebbe essere uguale).

Tuttavia, non è difficile trovare funzioni senza punti fissi che violano lo Y(g) = g(Y(g)) (vedere here). Anche alcuni funzionali non hanno punti fissi (vedi here).

In che modo la dimostrazione che ogni funzione ha un punto fisso si concilia con i contro-esempi indicati? JavaScript non è un calcolo lambda non tipizzato in cui è valida la prova che si applica Y(g) = g(Y(g))?

Answer 1

Il problema con le espressioni lambda è che non possono essere interpretate come funzioni in senso matematico, vale a dire mappature da un set all'altro.

La ragione è la cardinalità dell'insieme di funzioni da un insieme A su se stesso è sempre maggiore della cardinalità A, quindi non tutte le funzioni di A a A può essere un elemento di A. Cioè, c'è una funzione f: A -> A per la quale l'espressione f(f) non ha senso.

Questo è come il "set di tutti gli insiemi che non contengono se stesso", che non ha senso logicamente.

JavaScript non è un modello del calcolo lambda.

Il problema con il vostro esempio è che

(lambda x.g(x x)) (lambda x.g(x x)) 

dovrebbe essere equivalente a

g((lambda x.g(x x)) (lambda x.g(x x))) 

ma non è nel programma JavaScript in cui g è la funzione di indicatore di 0.

x x è sempre undefined. Quindi la prima riga restituisce g (undefined) = 0. La seconda riga viene valutata su g (g (undefined)) = g (0) = 1. Ciò significa che il tuo modello JavaScript del calcolo lambda non è, in effetti, un modello.

Poiché per ogni set non vuoto D esiste una funzione da D a D senza un punto fisso, ovviamente non può esserci alcun modello del calcolo lambda. Penso che dovrebbe essere anche possibile dimostrare che non ci può essere un'implementazione del combinatore Y in qualsiasi lingua completa di Turing.

Answer 2

Per quanto comprendo l'articolo di Wikipedia, non implica da nessuna parte che "ogni funzione JavaScript abbia un punto fisso" e questo esempio mostra semplicemente come implementare il combinatore Y per le funzioni che lo hanno in base alle loro specifiche.

E no, in base alle definizioni di tale articolo e an article on fixed point, JavaScript non può essere un lambda calcolo tipizzato, perché può formulare le funzioni che, ovviamente, fallire "avere un punto fisso" check, come function f(x){ return x + 1 } o x^1 se si desidera includere non numeri e quindi fallire anche il controllo di "ogni funzione ha almeno un punto fisso".

Answer 3

La teoria dei punti fissi viene nei sapori. Quelli per i linguaggi di programmazione sono studiati sotto la voce semantica denotativa. Esse dipendono dai valori che formano un insieme numerabile strutturato con proprietà speciali. Lattices e Complete Partial Orders sono due esempi. Tutti questi set hanno un elemento "in basso", che risulta essere il punto fisso che significa "nessun risultato utile". In effetti, gli unici operatori a punto fisso a cui sei interessato con i programmi per computer sono almeno operatori a punto fisso: quelli che trovano il punto fisso minimo unico più basso nel set di valori strutturato. (Nota tutti gli interi sono sullo stesso "livello" in questi set strutturati, solo l'elemento inferiore vive al di sotto. Il resto degli strati sono composti da tipi più complessi come tipi di funzioni e tuple, cioè strutture.) Se hai qualche calcolo matematico discreto , this distribuisce molto bene. Il teorema del punto fisso di Tarsky in realtà dice che ogni funzione che è monotone (o alternativamente continua) ha un punto fisso. Vedi il riferimento sopra per le definizioni. Nei programmi informatici operativi, l'elemento inferiore corrisponde a un calcolo non terminante: una ricorsione infinita.

Il punto di tutto questo è che se si dispone di un rigoroso modello matematico di calcolo, è possibile iniziare a provare cose interessanti sui sistemi di tipi e sulla correttezza del programma. Quindi non è solo un esercizio accademico.