Aplicaciones de la lógica y el álgebra en la informática

Question

He utilizado la lógica para la especificación de las políticas de seguridad en un modelo de seguridad. Uno de mis revisores me preguntó: "¿por qué has utilizado la lógica y no el álgebra para este fin, y cuál es tu justificación?". La primera respuesta que se me ocurre es que el álgebra es más adecuada para utilizarla en el modelado del comportamiento (aspectos dinámicos). Por ejemplo, para la especificación de protocolos de seguridad. Sin embargo, la lógica es más adecuada para la especificación de propiedades (aspectos estáticos). Por ejemplo, para la especificación de las propiedades de seguridad que necesitamos satisfacer en un entorno informático, o las propiedades de seguridad que deseamos que se satisfagan en un protocolo de seguridad. En otras palabras, el álgebra es adecuada para decir CÓMO, pero la lógica es adecuada para decir QUÉ.

Mis preguntas con respecto a este tema son:

1. ¿Es correcta mi respuesta inicial a esta pregunta o no?
2. ¿Cuáles son las otras respuestas a esta pregunta?
3. ¿Cuáles son las principales referencias que describen dónde debemos utilizar la lógica y dónde debemos utilizar el álgebra en sus aplicaciones en informática?

Answer 1

No me gustan este tipo de preguntas -no las tuyas, las de tu árbitro-, basta con que los autores resuelvan los problemas, la existencia de otras rutas que otras personas puedan preferir no viene al caso, a menos que haya alguna desventaja relativa que el árbitro pueda señalar.

1. ¿Es correcta mi respuesta inicial a esta pregunta o no? - No es lo que yo diría. Hay un montón de enfoques para manejar la mutabilidad en la lógica, de los cuales la lógica dinámica es probablemente el más ampliamente aplicado.
2. ¿Cuáles son las otras respuestas a esta pregunta? - Debería pensar que en su lugar diría algo como: "La elección de la lógica frente al álgebra es mucho menos importante que las decisiones de diseño tomadas al formalizar la especificación. Esto es lo que me pareció más adecuado en su momento".
3. ¿Cuáles son las principales referencias que describen dónde debemos utilizar la lógica y dónde debemos utilizar el álgebra en sus aplicaciones en informática? - No conozco nada en la línea de lo que preguntas. Blackburn, de Rijke & Venema (2001) Lógica Modal habla de las similitudes y diferencias entre las técnicas algebraicas y las teóricas de los modelos - me quedé con la impresión de que la mayor cuestión era si se prefería trabajar con teoremas de completitud o con teoremas de representación.

Para decir algo además de la respuesta de John, aquí había un hilo en Math Overflow, ¿Existe una relación entre la teoría de los modelos y la teoría de las categorías? Creo que eso da una idea de la poca distancia que se ve entre el álgebra y la lógica.

Answer 2

A cierto nivel, el álgebra y la lógica son equivalentes. Véase La lógica como álgebra por Paul Halmos y Steven Givant.

Answer 3

Tal vez quiera leer sobre el Isomorfismo de Curry-Howard que, por ejemplo, nos dice que los tipos en el cálculo lambda tipado (por lo tanto en lenguajes de programación como OCaml, SML, Haskell, entre otros) son en realidad proposiciones en algún formalismo lógico, y que los valores de estos tipos son pruebas de las proposiciones correspondientes. Se utiliza, por ejemplo, para desarrollar asistentes de pruebas que en realidad también son lenguajes de programación funcionales (Agda, Coq, Epigram, ...). En lo que respecta al álgebra, tal vez quieras leer "Elementos de programación", de Alexander Stepanov.