Aquí hay un puñado de elementos de respuesta, algunos de los cuales probablemente ya conozca.
1) La correspondencia CH se extiende a modelos de cómputo que incluyen el cálculo lambda simplemente tipado. Por ejemplo, sus versiones polimórficas, o los sistemas con tipos dependientes, y más generalmente todos los llamados “sistemas de tipo puro” (las extensiones del “cubo de Barendregt”). Pero supongo que lo sabes, ya que todos esos son modelos que se parecen al cálculo lambda.
2) Aparentemente menos conocido para el teórico de los lenguajes de programación genéricos, la correspondencia CH tiene sentido también para formalismos que sustentan el cálculo lambda simplemente tipado. En particular, desde el punto de vista de Curry-Howard, Linear Logic es una especie de cálculo lambda simplemente tipado ” examinado con rayos X “: hace formalmente explícito el uso de recursos (sub-términos) aprobados durante la ejecución (cuando beta -reducir un término). Por cierto, la Geometría de interacción de Girard, un modelo completamente nuevo de cómputo basado en álgebras de operadores, surgió de eso a lo largo de los años 90.
Tenga en cuenta que este punto 2) no tiene nada que ver con la respuesta anterior que se refiere al uso que hace Pfenning de (elementos de) lógica lineal para la concurrencia.
3) La correspondencia se extiende a la lógica clásica por un lado, y a modelos de computación que agregan características imperativas para funcionar con modelos de estilo de programación en el otro lado.
Este hecho se basa en una idea de T. Griffin. Se ha explotado principalmente para agregar funciones de control al cálculo lambda simplemente tipado. Pero teóricamente nos dice que también los formalismos puramente imperativos (más cercanos a las Máquinas de Turing) posiblemente puedan recibir una contrapartida lógica. Pocas personas han estado trabajando o siguen trabajando en estas cosas (sobre todo D. Ghica y G. McCusker, creo), pero no sé nada al respecto.
Desde una perspectiva más matemática, J.-L. Krivine ha usado esta idea para extender la correspondencia CH a la teoría de conjuntos: en su programa de investigación llamado realizabilidad clásica, ¡ toda la teoría de conjuntos con una forma débil de axioma de elección se usa como modelo de cálculo!
- Con respecto a la naturaleza de la verdad, ¿se puede probar que 2 + 2 = 4?
- Cómo demostrar que [matemáticas] \ displaystyle \ tan \ left (x – \ frac {\ pi} {4} \ right) = \ frac {\ tan x – 1} {\ tan x + 1} [/ math]
- Filosofía de la ciencia: ¿Por qué el razonamiento matemático es más válido que el razonamiento empírico? ¿Las matemáticas no se basan en la observación?
- He cubierto las pruebas de las leyes de reciprocidad cuadrática (los símbolos Legendre y Jacobi). Sin embargo, este tratamiento de residuos cuadráticos ha sido bastante seco. ¿Existen aplicaciones de la vida real de los residuos cuadráticos?
- Cómo mejorar en las pruebas
4) La correspondencia CH puede aplicarse a formalismos lógicos diferentes de la deducción natural. El caso de la lógica combinatoria / sistemas de estilo Hilbert es bien conocido (pero tal vez no sea tan útil desde la perspectiva de la informática). Más recientemente, el estudio de la correspondencia CH para cálculos posteriores ha florecido. Los modelos de cómputo correspondientes siguen siendo modelos funcionales orientados a la programación como el cálculo lambda, pero en los que tanto los programas como los entornos de ejecución (“coprogramas”) tienen una ciudadanía de primera clase (simétrica). Además, estos modelos incorporan las características imperativas del punto 3) anterior. P. Wadler tiene un artículo muy bien escrito que explica esto a una amplia audiencia. La intuición proviene de obras de P.-L. Curien y H. Herbelin de finales de los 90.
De todos modos, me temo que esta no es la respuesta que estabas buscando, ya que estos modelos siguen siendo muy “lambda-calculish”.
5) En lo que respecta al cálculo lambda sin tipo , no tiene sentido pedir una lógica correspondiente. Pero para muchos modelos de denotación específicos del cálculo lambda sin tipo se puede encontrar una lógica correspondiente: un sistema de tipos que formaliza de manera finita la habitación de las interpretaciones de los términos. Estas “lógicas” se conocen como sistemas de tipo intersección .