¿Cuál es el punto de llamar -calculus un álgebra?

11

¿Cuál es la diferencia de llamar a -calculus un álgebra en lugar de un cálculo? Planteo esta pregunta porque leí en alguna parte la línea " -calculus no es un cálculo sino un álgebra" (iirc, atribuido a Dana Scott). ¿Cual es el punto? Gracias.λλλ

día
fuente
Procedente de un aprendiz del tema que probablemente no tenga ninguna idea: ¿no está determinando si dos expresiones de cálculo lambda son indecidibles equivalentes? ¿Tiene eso alguna influencia sobre por qué no se consideraría un "cálculo"? Porque esa es una pregunta fundamental que no se puede calcular algorítmicamente ...
Jeremy Kun

Respuestas:

14

Un cálculo es un sistema de computación basado en la manipulación de expresiones simbólicas. Un álgebra es un sistema de expresiones simbólicas y relaciones entre ellos [*]. Es decir, un cálculo es un sistema para encontrar respuestas, y un álgebra es una forma de expresar las relaciones entre los términos.

El cálculo es un cálculo o un álgebra, dependiendo de si desea pensar en las reglas y como reglas de reducción orientadas o ecuaciones no orientadas. Si piensa que las reglas están orientadas, entonces ha fijado un orden de evaluación, y las reglas le dicen cómo tomar un término y producir una forma normal. Si piensa que las reglas no están orientadas, le dan la relación de igualdad en -terms.β η λλβηλ

[*] También hay una definición categórica de álgebra, que es una definición formal algo más restrictiva que la idea informal. Hablando en términos generales, la diferencia es que la definición formal de álgebra abarca solo aquellos sistemas sin enlace variable. Entonces los combinadores de SKI forman un álgebra, pero el cálculo no.λ

Neel Krishnaswami
fuente
Como mencioné en mi comentario, se puede demostrar que la definición categórica de álgebras abarca estructuras con operaciones de unión. La idea principal es que, mientras que las estructuras sin ligantes pueden representarse como álgebras en conjuntos, las estructuras con ligantes pueden representarse mediante álgebras en -presheafs-.
cody
AFAIK, es la definición de álgebra en álgebras universales que no permite operaciones con firmas de orden superior (de acuerdo con los Fundamentos de Lenguajes de Programación de John Mitchell).
Blaisorblade
10

Tradicionalmente, un álgebra es un conjunto de portadores con operaciones que satisfacen algunas ecuaciones (piense en "grupo"). Hay muchas formas de generalizar la noción:

  • las álgebras de clasificación múltiple tienen varios conjuntos de portadores. Un ejemplo sería un módulo sobre un anillo , donde queremos considerar todo como un solo álgebra. Otro ejemplo, más bien tonto, es un gráfico dirigido, que tiene dos conjuntos de portadores, de bordes y de vértices, y dos operaciones, fuente y objetivo , sin satisfacer ecuaciones.R E V s : E V E VMREVs:EVEV

  • Se pueden permitir axiomas más generales que no sean solo ecuaciones. Por ejemplo, los axiomas para un campo son todas las ecuaciones, excepto para . Otro ejemplo es algo así como un dominio integral.x0xx1=1

  • pueden permitirse operaciones más generales , en particular las de aridad infinita, u operaciones de orden superior que toman funciones como argumentos. Un ejemplo de una operación infinita es la en álgebras de punto medio de Martin Escardo y Alex Simpson. Si vas lejos en esta dirección llegas a las mónadas.M

En este sentido, el cálculo tipo es un álgebra porque se especifica en términos de un conjunto de portadores con algunas operaciones (de orden superior) que satisfacen algunas ecuaciones ( y ).β ηλβη

Andrej Bauer
fuente
6

Hay una definición bastante precisa de lo que es un álgebra en la teoría de categorías: vea este artículo, por ejemplo. Tomó algunos años entender cómo una estructura con variables ligadas podría entenderse en el mismo contexto que el término estructura de álgebra comúnmente utilizada en matemáticas e informática, y resulta que el concepto categórico de álgebras F es capaz de unificar el dos. No estoy seguro de los aspectos históricos de la solución, pero un enfoque posible es que las álgebras anteriores a la introducción de Fiore, Plotkin y Turi (disponibles aquí ) resolvieron la cuestión e impulsaron enfoques diferentes pero similares, ver, por ejemplo, Hirshowitz et al. y su estudiante de doctorado Julianna Zsido .

Queda por hacer una investigación interesante sobre cómo usar los conceptos categóricos para refactorizar y profundizar nuestra comprensión de las estructuras con variables ligadas, con la esperanza de eliminar el "cruft" sintáctico que generalmente comprende los capítulos más aburridos de las tesis sobre -calculi y estructuras relacionadas.λ

cody
fuente
Las álgebras F generalmente son álgebras libres, es decir, no permiten ecuaciones; La introducción de la teoría de categoría de Pierce (desde 1992) afirma que no hay desarrollo de ecuaciones para álgebras F. Solo he leído sobre soluciones en el resumen de la tesis doctoral de Chung-Kil (Gil) Hur, de 2010: "Sistemas ecológicos categóricos: modelos algebraicos y razonamiento equitativo". ¿Es eso lo que supongo, y es el primer tratamiento del tema?
Blaisorblade
No creo que haya ninguna razón por la cual el enfoque de F-álgebra no se aplique a las teorías con ecuaciones. La idea es que puedes formar álgebras iniciales con ecuaciones de las libres (sin ecuaciones) "cociente" por la teoría apropiada. No sé mucho sobre el trabajo de Gil o lo que Pierce quiso decir con su comentario.
cody
Anexo: después de una mirada superficial, el trabajo de Gil con Marcello Fiore parece tratar una noción general de teorías equitativas para las álgebras F.
cody
5

Si bien es cierto que la noción de "cálculo" está menos bien definida que la noción de "álgebra", en general el "cálculo" generalmente implica un proceso de cálculo, mientras que las álgebras tienen patrones de construcción con teorías equitativas.
Se podría decir que existe una sensación de que las álgebras "ya existen" como estructuras y que simplemente estamos descubriendo verdades sobre ellas, en lugar de utilizar algún método para producir nuevas respuestas que antes no existían.

Si piensa en lo que Scott estaba tratando de lograr con los dominios de Scott, su afirmación tiene sentido: estaba tratando de encontrar estructuras matemáticas y algebraicas predefinidas que sirvieran como una semántica fija para LC. Quería eliminar la sensación de que el significado de un término era lo que resultaba de un proceso en particular.

Quizás le interese una respuesta previa sobre una pregunta relacionada: ¿Qué constituye la semántica denotacional?

Marc Hamann
fuente
4

Sería muy reacio a llamar al cálculo lambda un "álgebra" por una razón muy simple. Es un sistema formal definido puramente usando sintaxis, sin ninguna referencia al significado. Las equivalencias y están en un meta-nivel, usando variables como y que se extienden sobre los términos. Eso no es lo que los algebraistas llamarían "álgebra". Por otro lado, los lógicos han usado durante mucho tiempo el término "cálculo" para referirse a los sistemas formales donde las reglas se expresan a nivel meta.η M NβηMN

Si Scott alguna vez llamó al cálculo lambda un "álgebra" (lo cual dudo bastante), entonces habría estado haciendo un punto bastante sutil, a saber, que se puede pensar que el cálculo lambda tiene un significado a priori .

Aún así, tendría dificultades para convencer a los algebraistas de su afirmación, porque no tiene ecuaciones en el cálculo lambda, tiene equivalencias (es decir, en el nivel meta). "Álgebra combinatoria", por otro lado, es perfectamente normal.

Uday Reddy
fuente
3

No existe un cálculo , pero hay un objeto matemático bien definido llamado álgebra , aunque la palabra tiene muchos usos . Sin embargo, supongo que el nombre se dio en el sentido de

(...) el estudio abstracto de sistemas numéricos y operaciones dentro de ellos.

dado que, en -calculus, usted define objetos ( términos , que puede llamar números ) y operaciones dentro de esos objetos.λ

Janoma
fuente
Mira la respuesta de Neel.
Dave Clarke
Sí. Eso ciertamente parece una definición, pero no es una definición estándar. Estoy de acuerdo con Neel en que puede ser lo que quieras dependiendo de tu interpretación de las reglas, pero eso también depende de tu definición de "cálculo" y "álgebra", ninguno de los cuales es estándar (aparte del objeto formal que viene de un espacio vectorial, que no es el caso con -calculus). λ
Janoma