- Alonzo Church no es tan conocido por el público como Alan Turing, pero fue un lógico que sentó las bases lógicas de la computación con el λ-calculus y la teoría de la computabilidad
- La Church-Turing thesis de 1936 ofreció un marco según el cual toda función efectivamente computable puede calcularse con una Turing machine o con un sistema equivalente
- Frente al Entscheidungsproblem de Hilbert, respondió que no existe un algoritmo determinista capaz de decidir todas las proposiciones matemáticas, dejando claros los límites de la computación
- En Princeton dirigió a Stephen Kleene, J. Barkley Rosser, Alan Turing y otros; Turing completó su Ph.D. bajo la supervisión de Church
- Su trabajo abstracto permanece en la genealogía de la computación que llega hasta los compiladores modernos, los intérpretes, la programación funcional, las apps de smartphones y la IA
Una influencia teórica mayor que su fama pública
- Alan Turing aparece con más frecuencia en la historia popular de la computación y la inteligencia artificial por el Turing Test, pero Church fue una figura que influyó profundamente en el pensamiento y el trabajo de Turing
- El trabajo de Church se convirtió en una base importante para entender qué es la computación y para formar conceptos con los que se evalúa la IA
- Sin los aportes de Church, las ideas actuales sobre la inteligencia artificial y sus formas de evaluación podrían haber sido bastante distintas
Vida y perfil académico
- Church fue un lógico tranquilo y de pocas palabras, nacido el 14 de junio de 1903 en Washington, D.C.
- Hay registros de que en su niñez perdió la vista total o parcialmente en un ojo por un accidente con una pistola de aire comprimido
- Tras terminar una preparatory school en Connecticut en 1920, ese mismo año inició sus estudios universitarios en Princeton y completó el doctorado en 1927
- Después de pasar tiempo en Harvard, Göttingen y Amsterdam como National Research Fellow, regresó a Princeton, donde desarrolló gran parte de su obra académica
- Era conocido por su letra prolija en el pizarrón y por su carácter meticuloso; incluso llegó a cubrir artículos importantes con Duco cement para conservarlos
λ-calculus y computabilidad
- La contribución más profunda de Church fue el λ-calculus, que se convirtió en una base de la computación antes de que existiera el nombre ciencia de la computación
- En 1936, Church formalizó la Church-Turing thesis, un concepto central de la informática teórica
- Sostiene que una función efectivamente computable puede calcularse con una Turing machine o con un sistema equivalente
- Proporciona un marco para entender qué puede hacer una máquina en teoría
- También revela los límites que pueden alcanzar los procedimientos algorítmicos
- Aunque esta tesis es un concepto fundacional, siguen existiendo debates y límites en torno a la interpretación de la “effective computability”, la computación física y la naturaleza de la inteligencia humana
- Si Turing propuso la Turing machine para trasladar procedimientos mecánicos a una forma lógica, Church aportó la abstracción pura que respaldaba teóricamente esas máquinas
Programación moderna y pensamiento funcional
- La influencia del λ-calculus también se ve hoy en los principios de escritura de programas, y se vincula con enfoques que enfatizan la composición, las funciones de orden superior y la inmutabilidad
- Este sistema formal permitió codificar problemas matemáticos abstractos y resolverlos mecánicamente, y se convirtió en una base para las arquitecturas de compiladores e intérpretes modernos
- Para un programador moderno, el λ-calculus puede verse como un conjunto de funciones anidadas, similar a lo que aparece en Lisp, Haskell y en algunos paradigmas de Python o JavaScript
- La abstracción del λ-calculus se convirtió en la base de la programación funcional, donde las funciones se tratan como first-class citizens
Entscheidungsproblem y los límites de la computación
- Church también hizo aportes importantes a otras áreas de la lógica y la filosofía, y un ejemplo representativo es su trabajo sobre el Entscheidungsproblem
- El Entscheidungsproblem era un problema de decisión planteado por David Hilbert en 1928, que preguntaba si existía un algoritmo determinista capaz de decidir la verdad de cualquier proposición matemática
- Church dio una respuesta negativa: tal algoritmo no existe, y este resultado se conoce como Church's Theorem
- Este hallazgo influyó profundamente en la teoría de la decisión y subrayó los límites de lo que puede lograrse solo mediante computación
El centro intelectual de Princeton y sus discípulos
- Church fue un mentor de lógicos e informáticos importantes de su época
- Su linaje académico incluye a Stephen Kleene, J. Barkley Rosser y Alan Turing
- Turing completó su Ph.D. en Princeton bajo la supervisión de Church
- Se cuenta que David Kaplan recomendaba a los nuevos estudiantes de posgrado tomar las clases de Church, diciendo que, aunque no fuera su área de interés, sería una experiencia que podrían contarles a sus nietos
- En la década de 1930, Princeton fue un centro intelectual del desarrollo de la lógica moderna, con John von Neumann, Kurt Gödel y Church reunidos allí
Un legado poco visible
- Church no alcanzó el mismo nivel de fama pública que Turing, von Neumann o Gödel
- Su legado no tenía una forma fácil de capturar la imaginación popular, como los relatos heroicos del descifrado de códigos en tiempos de guerra o la tragedia de una muerte temprana
- Los miles de millones de programas que se ejecutan en smartphones pueden rastrear su lógica hasta las funciones abstractas del λ-calculus
- Desde apps simples hasta la inteligencia artificial, el ADN invisible de la computación hereda una línea importante del trabajo de Church
- La genialidad de Church no estuvo en el espectáculo, sino en las estructuras rigurosas y la elegancia silenciosa que cambian el mundo
1 comentarios
Comentarios en Hacker News
Me gustó el origen del nombre lambda que aparece en Paradigms of Artificial Intelligence Programming (PDF/EPUB: https://github.com/norvig/paip-lisp)
La historia dice que Alonzo Church tomó el acento circunflejo que Russell y Whitehead escribían sobre una variable ligada en la notación de Principia Mathematica,
x̂(x + x), y al intentar convertirlo en una cadena unidimensional lo movió al frente como^x(x + x); luego, como el circunflejo vacío se veía raro, lo cambió por una lambda mayúsculaΛx(x + x), y después por una lambda minúsculaλx(x + x)para evitar confusionesTambién cuenta que John McCarthy fue alumno de Church en Princeton y que, cuando creó Lisp en 1958, como las tarjetas perforadas no tenían letras griegas, usó
(lambda (x) (+ x x)), y así quedó hasta hoyPor eso, como sugiere el tema de este artículo, Church aparece con frecuencia en las retrospectivas sobre Lisp, y solo puede ser una figura “olvidada” para gente con casi ningún interés en la historia de la computación
Según Dana Scott, el propio Church dijo que fue una elección arbitraria, tipo “eeny, meeny, miny, moe”, y también se dice que la explicación al estilo de Barendregt fue refutada en una charla reciente en la University of Birmingham
En el ámbito francófono, “personne lambda” significa una persona común o anónima, así que encaja bien con una función anónima, y el adjetivo lambda también significa “general/común”, así que da la sensación de que una letra a media tabla del alfabeto griego representa algo promedio
https://math.stackexchange.com/questions/64468/why-is-lambda...
Trata muchos temas de programación y también abre la puerta a paradigmas que pueden resultar extraños para quienes han tenido poca exposición a la programación funcional
Hay otro caso en el que Church da a entender que fue más bien una elección arbitraria entre letras griegas, en https://en.wikipedia.org/wiki/Lambda_calculus#Origin_of_the_...
También me pregunto si fue antes o después de que McCarthy empezara Lisp
“El cálculo lambda de Church y las máquinas de Turing tienen una capacidad computacional equivalente, pero las máquinas de Turing se diferencian en que usan estado mutable. Que hasta hoy siga habiendo una fractura entre lenguajes funcionales e imperativos se debe a la separación entre Church y state”
Conozco esa cita desde hace mucho, pero no he podido encontrar la fuente original
Edit: podría venir de Guy Steele: “Hay personas que no quieren mezclar la parte funcional o de cálculo lambda de un lenguaje con la parte que produce efectos secundarios. Parecen creer en la separación entre Church y state”
El archivo original está aquí: https://people.csail.mit.edu/gregs/ll1-discuss-archive-html/...
La broma es que los europeos por lo general pronuncian bien su nombre, “Nick-louse Veert”, mientras que los estadounidenses lo arruinan diciendo “Nickel's Worth”
O sea, los europeos lo llaman por su nombre, y los estadounidenses por su valor
https://en.m.wikiquote.org/wiki/Niklaus_Wirth
Si quieren leer un texto realmente asombroso sobre Church, recomiendo la semblanza de Rota
Es la primera sección de https://www34.homepage.villanova.edu/robert.jantzen/princeto...
Como enlaces relacionados, están Alonzo Church, 92, Theorist of the Limits of Mathematics (1995) - https://news.ycombinator.com/item?id=12240815 - agosto de 2016, y Gian-Carlo Rota on Alonzo Church (2008) - https://news.ycombinator.com/item?id=9073466 - febrero de 2015
Vale la pena leer el libro completo
El lenguaje de programación Alonzo, que lleva su nombre, está casi olvidado
https://dl.acm.org/doi/pdf/10.1145/68127.68139
En particular, la filosofía de la lógica y la teoría del significado/referencia que conectan el trabajo de Frege y Russell han sido mayormente olvidadas
Church publicó muchos artículos sobre este tema, pero casi no se trata en lugares como Wikipedia
Aun así, la entrada de la Stanford Encyclopedia of Philosophy está algo mejor: https://plato.stanford.edu/entries/church/
Pero incluso esa, según entiendo, deja fuera parte de su trabajo principal, y da la impresión de que era demasiado filosófico para los matemáticos y demasiado técnico para los filósofos
No es el punto central, pero preferiría que se evitara usar ilustraciones generadas por IA en entradas de blog como esta
Hay fotos reales de Church incluso en dominio público, y esta ilustración ni siquiera se parece mucho a él; además, como el artículo se hizo popular, ya aparece en resultados de búsqueda de imágenes
Si es una ilustración que ni siquiera vale los más de 5 minutos que tomó generarla, quizá sería mejor simplemente omitirla
Aun así, si de verdad se va a usar una imagen generada por “IA”, como mínimo debería llevar esa leyenda
No me entusiasmaba tomar una foto de internet, y esta imagen fue el séptimo resultado que hice para evitar que pareciera un falso parecido; sentí que se parecía hasta cierto punto
La imagen de JvN quedó bastante bien, pero en adelante probablemente sea mejor usar imágenes simbólicas en lugar de falsos parecidos que parecen personas reales
La expresión “arquitecto de la inteligencia computacional” parece exagerada
Es cierto que Church fue un gran lógico, pero si aquí inteligencia computacional significa AI/ML, en realidad su contribución fue prácticamente nula
Aparte, ni siquiera estoy muy seguro de que el cálculo lambda sea realmente matemáticas; parece más bien una notación ingeniosa
Las ventajas de una notación son subjetivas, y también resulta interesante que a Church no le interesara especialmente que sus ideas inspiraran el diseño de ciertos lenguajes de programación
La STT también suele identificarse con la lógica de orden superior, porque con solo dos tipos primitivos, el “individuo” básico y los valores de verdad T/F, además del tipo funcional
(a --> b), se puede expresar cualquier objeto lógico arbitrarioLa STT es claramente una invención de Church, influyó mucho en las teorías de tipos modernas y también en lenguajes de programación con sistemas de tipos complejos como Haskell
No puedo demostrarlo por completo, pero intuitivamente me parece que Turing y lo que él simboliza terminan siendo valorados del lado de la IA, mientras que Church parece lo contrario
El primero partía de la pureza, de las condiciones mínimas posibles, del cómputo abstracto y “puro”; el segundo parecía más interesado en cómo realmente podemos pensar, y más atento a la expansión de la representación y la abstracción que a la implementación
Church no tenía experiencia práctica con computadoras y estaba más cerca de querer expandir la propia teoría matemática
La colaboración entre ambos y su comunicación a través del Atlántico combinaron lo práctico y lo teórico para consolidar teorías clave como la dualidad imperativo/funcional, el teorema de Church-Turing y la relación entre el problema de la parada y el teorema de Church
Verlo como una rivalidad es un error, y decir que la informática tiene “dos padres” es apropiado por varias razones
Más aún si se considera la muerte de Turing
Además, no hay que pasar por alto que Turing no carecía de interés por la implementación; quería volver a ella en la práctica, pero no se lo permitieron
Queda la gran tragedia y la pregunta de qué habría cambiado si la clasificación secreta del gobierno británico hubiera sido distinta, aunque también es posible que entonces hubiéramos perdido, en nuestra línea temporal, la colaboración con Church que permitió consolidar tan bien la teoría
Fue una suerte haber podido conocer a Alonzo Church y Haskell Curry en el ACM Symposium on LISP and Functional Programming realizado en CMU en agosto de 1982
Curry claramente no estaba bien de salud y falleció unas dos semanas después del congreso, pero Church se veía saludable y vivió unos 13 años más
En la recepción, Gerry Sussman estaba muy entusiasmado mientras recorría la sala presentando a ambos, y para nosotros también fue muy emocionante haberlos conocido
Una de las grandes contribuciones de Church fueron sus estudiantes
De un mismo lugar salieron pensadores extraordinarios