Y Combinator: Algunas funciones no tienen puntos fijos

Question

El Wikipedia article on the Y combinator proporciona la siguiente implementación de JavaScript del combinador 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); }); }) 
    ); 
} 

La existencia de un combinador Y en JavaScript debe entender que cada función JavaScript tiene un punto fijo (dado que para cada función g, Y(g) y g(Y(g)) deben ser iguales).

Sin embargo, no es difícil encontrar funciones sin puntos fijos que violen Y(g) = g(Y(g)) (ver here). Incluso ciertos funcionales no tienen puntos fijos (vea here).

¿Cómo se compara la evidencia de que cada función tiene un punto fijo con los contraejemplos dados? ¿JavaScript no es un cálculo lambda sin tipo en el que se aplica la prueba de que Y(g) = g(Y(g))?

Answer 1

El problema con las expresiones lambda es que no se pueden interpretar como funciones en un sentido matemático, es decir, asignaciones de un conjunto a otro.

La razón es la cardinalidad del conjunto de las funciones de un conjunto A en sí mismo es siempre mayor que la cardinalidad de A, por lo que no todas las funciones de A a A puede ser un elemento de A. Es decir, hay una función f: A -> A para la cual la expresión f(f) no tiene sentido.

Esto es como el "conjunto de todos los conjuntos que no se contiene", lo cual no tiene sentido lógicamente.

JavaScript no es un modelo del cálculo lambda.

El problema con el ejemplo es que

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

debe ser equivalente a

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

pero no lo es en su programa JavaScript, donde g es la función indicadora de 0.

x x es siempre undefined. Por lo tanto, la primera línea evalúa a g (undefined) = 0. La segunda línea se evalúa como g (g (undefined)) = g (0) = 1. Esto significa que su modelo de JavaScript del cálculo lambda, en realidad, no es realmente un modelo.

ya que para cada conjunto no vacío D hay una función D-D sin un punto fijo, obviamente, no puede haber ningún modelo del cálculo lambda. Creo que debería ser posible incluso probar que no puede haber una implementación del Y-combinator en ningún lenguaje de Turing completo.

Answer 2

Por lo que entiendo el artículo de Wikipedia, no implica que "cada función de JavaScript tenga un punto fijo" y este ejemplo simplemente muestra cómo implementar el combinador Y para las funciones que lo tienen según sus especificaciones.

Y no, de acuerdo a las definiciones de ese artículo y an article on fixed point, JavaScript puede no ser un cálculo lambda sin tipo, ya que puede formular funciones que obviamente fallar "tener un punto fijo" cheque, como function f(x){ return x + 1 } o x^1 si quieres incluye no números y, por lo tanto, falla la comprobación de "cada función tiene al menos un punto fijo".

Answer 3

La teoría de los puntos fijos viene en sabores. Los de lenguajes de programación se estudian bajo el encabezado de semántica denotacional. Dependen de los valores que forman un conjunto contable estructurado con propiedades especiales. Lattices y Complete Partial Orders son dos ejemplos. Todos estos conjuntos tienen un elemento "inferior", que resulta ser el punto fijo que significa "ningún resultado útil". De hecho, los únicos operadores de punto fijo que le interesan con los programas informáticos son menos operadores de punto fijo: aquellos que encuentran el único punto fijo mínimo que es el más bajo en el conjunto estructurado de valores. (Tenga en cuenta que todos los enteros están en el mismo "nivel" en estos conjuntos estructurados. Solo el elemento inferior vive debajo. El resto de las capas se componen de tipos más complejos como tipos de funciones y tuplas, es decir, estructuras). Si tiene algunas matemáticas discretas , this lo presenta muy bien. El teorema del punto fijo de Tarsky en realidad dice que cada función que es monótona (o alternativamente continua) tiene un punto fijo. Ver la referencia anterior para las definiciones. En los programas informáticos operacionales, el elemento inferior corresponde a un cálculo no terminante: una recursión infinita.

El punto de todo esto es que si tiene un modelo matemático riguroso de computación, puede comenzar a probar cosas interesantes acerca de los sistemas de tipo y la corrección del programa. Entonces no es solo un ejercicio académico.