¿Hay algún Modelo matemático o teoría detrás de los lenguajes de programación?

Question

Los RDBMS se basan en Relational Algebra y en el Modelo de Codd. ¿Tenemos algo similar a los lenguajes de programación o OOP?

Answer 1

¿Tenemos [un modelo subyacente ] para lenguajes de programación?

Cielos, sí. Y debido a que hay tantos muchos lenguajes de programación, hay múltiples modelos para elegir. Más importante primero:

• de sin tipo cálculo lambda es un modelo de computación que es tan poderoso como una máquina de Turing (ni más ni menos) Iglesia. La famosa "hipótesis de Church-Turing" es que estos dos modelos equivalentes representan el modelo más general de computación que sabemos cómo implementar. El cálculo lambda es extremadamente simple; en su totalidad el lenguaje es

  e ::= x | e1 e2 | \x.e 
  

  que constituyen las variables , aplicaciones de función y definiciones de funciones. El cálculo lambda también viene con una colección bastante grande de "reglas de reducción" para simplificar expresiones. Si encuentra una expresión que no se puede reducir, eso se llama una "forma normal" y representa un valor.

  El cálculo lambda es tan general que puede tomarlo en varias direcciones.

  • Si desea utilizar todas las reglas disponibles, puede escribir herramientas especializadas como evaluadores parciales y partes de compiladores.

  • Si evita reducir cualquier subexpresión bajo una lambda, pero use todas las reglas disponibles, terminará con un modelo de lenguaje funcional vago como Haskell o Clean. En este modelo, si una reducción puede terminar, está garantizado y es fácil representar estructuras de datos infinitas. Muy poderoso.

  • Si no reducir cualquier subexpresión bajo una lambda, y si también insiste en la reducción de cada argumento a una forma normal antes de aplicar una función, entonces usted tiene un modelo de un lenguaje funcional ansiosos como F #, Lisp , Objetivo Caml, Esquema o Estándar ML.

• También hay varios sabores de escriben cálculos lambda, de los cuales el más famoso se agrupan bajo el sistema de nombres F, que fueron descubiertos independientemente por Girard (en la lógica) y por Reynolds (en Ciencias de la Computación). System F es un excelente modelo para lenguajes como CLU, Haskell y ML, que son polimórficos pero tienen verificación de tipos en tiempo de compilación. Hindley (en lógica) y Milner (en informática) descubrieron una forma restringida del Sistema F (ahora llamado sistema de tipo Hindley-Milner) que permite inferir expresiones del Sistema F a partir de algunas expresiones del cálculo lambda sin tipo. Damas y Milner desarrollaron un algoritmo para hacer esta inferencia, que se usa en ML estándar y se ha generalizado en otros idiomas.

• Lambda calculus solo está presionando los símbolos. El trabajo pionero de Dana Scott en semántica denotacional mostró que las expresiones en el cálculo lambda en realidad corresponden a las funciones matemáticas — y él identificó cuáles. El trabajo de Scott es especialmente importante para dar sentido a las "definiciones recursivas", que son comunes en la informática pero carecen de sentido desde el punto de vista matemático. Scott y Christopher Strachey demostraron que una definición recursiva es equivalente a la solución menos definida para una ecuación de recursión, y además demostraron cómo se podría construir esa solución. Cualquier lenguaje que permita la recursión, y especialmente los lenguajes que permiten la recursión en un tipo arbitrario (como Haskell y Clean), debe algo al modelo de Scott.

• Hay toda una familia de modelos basados ​​en máquinas abstractas. Aquí no hay tanto un modelo individual como una técnica. Puede definir un idioma utilizando una máquina de estados y definiendo transiciones en la máquina. Esta definición abarca desde máquinas de Turing hasta máquinas de Von Neumann hasta sistemas de reescritura de términos, pero en general la máquina abstracta está diseñada para "estar lo más cerca posible del lenguaje". El diseño de tales máquinas, y el negocio de probar teoremas acerca de ellas, se incluye bajo el encabezado de Semántica operacional.

¿Qué pasa con la programación orientada a objetos?

No soy tan educado como debería sobre los modelos abstractos utilizados para OOP. Los modelos con los que estoy más familiarizado están estrechamente relacionados con las estrategias de implementación. Si quisiera investigar más esta área, comenzaría con la semántica denotativa de William Cook para Smalltalk. (Smalltalk como lenguaje es muy simple, casi tan simple como el cálculo lambda, por lo que es un buen caso de estudio para modelar lenguajes más complicados orientados a objetos.)

Wei Hu me recuerda que Martin Abadi y Luca Cardelli han puesto juntos un ambicioso cuerpo de trabajo sobre cálculos fundacionales (análogos al cálculo lambda) para lenguajes orientados a objetos. No entiendo el trabajo lo suficientemente bien como para resumirlo, pero aquí hay un pasaje del Prólogo de su libro, que creo que vale la pena citar:

Los lenguajes de procedimiento en general son bien conocidos; sus construcciones son ahora estándar, y sus fundamentos formales son sólidos. Las características fundamentales de estos lenguajes se han destilado en formalismos que resultan útiles para identificar y explicar cuestiones de implementación, análisis estático, semántica y verificación.

Aún no se ha llegado a una comprensión análoga de los lenguajes orientados a objetos. No existe un acuerdo generalizado sobre una colección de construcciones básicas y sobre sus propiedades ... Esta situación podría mejorar si tuviéramos una mejor comprensión de los fundamentos de los lenguajes orientados a objetos.

... tomamos los objetos como primitivos y nos concentramos en las reglas intrínsecas que los objetos deben obedecer. Introducimos cálculos de objetos y desarrollamos una teoría de objetos a su alrededor. Estos cálculos de objetos son tan simples como cálculos funcionales, pero representan objetos directamente.

Espero que esta cita le dé una idea del sabor del trabajo.

Answer 2

Un concepto puede ser Turing Machine.

Answer 3

Como sé, Formal grammars se usa para la descripción de la sintaxis.

Answer 4

Los lenguajes de programación es producto de la aplicación de las siguientes teorías:

• teoría de algoritmos
• teoría de la computación
• autómatas Estado
• y más

Answer 5

Los lenguajes funcionales como Lisp heredan su Conceptos básicos de "lambda calculs" de la Iglesia (artículo de Wikipedia here) Saludos

Answer 6

El history section de de programación orientada a objetos de Wikipedia podría ser esclarecedor.

Answer 7

La analogía más cercana que puedo pensar es Gurevich Evolving Algebras que, hoy en día, son más conocidos bajo el nombre de "Gurevich Abstract State Machines" (GASM).

Tengo la esperanza de ver aplicaciones más reales de la teoría cuando Gurevich se unió a Microsoft, pero parece que muy pocos están saliendo. Puede verificar la página ASML en el sitio de Microsoft.

Lo bueno de GASM es que se parecen mucho a los pseudocódigos incluso si su semántica está formalmente especificada. Esto significa que los practicantes pueden comprenderlos fácilmente.

Después de todo, creo que parte del éxito de álgebra relacional es que es la base formal de conceptos que pueden ser captadas fácilmente, es decir, tablas, claves foráneas, se une, etc.

Creo que necesitamos algo similar para los componentes dinámicos de un sistema de software.

Answer 8

Lisp se basa en Lambda Calculus, y es la inspiración de gran parte de lo que vemos hoy en los idiomas modernos.

Las máquinas Von-Neumann son la base de las computadoras modernas, que primero se programaron en lenguaje ensamblador, luego en FORmula TRANslator. Luego se aplicó la teoría lingüística formal de gramáticas libres de contexto, y subyace a la sintaxis de todos los lenguajes modernos.

La teoría de la computabilidad (autómatas formales) tiene una jerarquía de tipos de máquina que es paralela a la jerarquía de las gramáticas formales, por ejemplo, regular-gramática = finita-estado-máquina, contexto-libre-gramática = pushdown-autómata, contexto- sensible-gramática = turing-máquina.

También existe la teoría de la información, de dos tipos, Shannon y Kolmogorov, que se puede aplicar a la informática.

Existen modelos de informática menos conocidos, como la teoría de funciones recursivas, las máquinas de registro y las máquinas post-máquina.

Y no se olvide de la lógica de predicados en sus diversas formas.

Agregado: Olvidé mencionar matemáticas discretas: teoría de grupos y teoría de redes. Las rejas en particular son (en mi humilde opinión) un concepto particularmente ingenioso que subyace a toda la lógica booleana, y algunos modelos de computación, como la semántica de denotación.

Answer 9

Si estudias lenguajes de programación (p. Ej .: en una universidad), existe una gran cantidad de teoría y no solo un poco de matemáticas.

ejemplos son:

• Finite State Machines
• Formal Lanugages (y Context Free Grammars como BNF utiliza para describirlos)
• La construcción de LRish parser tables

Answer 10

Hay muchas dimensiones para responder a su pregunta, dispersas en las respuestas.

En primer lugar, para describir la sintaxis de un idioma y especificar cómo funcionaría un analizador, utilizamos las gramáticas libres de contexto.

Luego debe asignar significados a la sintaxis. La semántica formal es útil; los principales actores son la semántica operacional, la semántica denotacional y la semántica axiomática.

Para descartar los malos programas, tiene el sistema de tipos.

Al final, todos los programas de computadora pueden reducir (o compilar, si se quiere) modelos de computación muy simples. Los programas imperativos se asignan con mayor facilidad a las máquinas de Turing, y los programas funcionales se asignan al cálculo lambda.

Si estás aprendiendo todas estas cosas por sí mismo, lo recomiendo altamente http://www.uni-koblenz.de/~laemmel/paradigms0910/, debido a que las conferencias se graban en video y poner en línea.

Answer 11

Se ha mencionado mucho acerca de la aplicación de las matemáticas a la teoría computacional y la semántica. Me gusta la mención de la teoría de tipos y me alegro de que alguien haya mencionado la teoría del enrejado. Aquí hay solo algunos más.

Nadie ha mencionado explícitamente la teoría de categorías, que aparece más en los lenguajes funcionales que en cualquier otro lugar, como a través de los conceptos de mónadas y funtores. Luego está la teoría de modelos y las diversas encarnaciones de la lógica que realmente aparecen en los demostradores de teoremas o en el lenguaje lógico Prolog. También hay aplicaciones matemáticas para fundamentos y problemas en idiomas concurrentes.

Answer 12

No hay un modelo matemático para OOP.

Álgebra relacional en el modelo matemático para SQL. Fue creado por E.F. Codd. C.J. Date también fue un científico reconocido que ayudó con esta teoría. La idea es que puede realizar todas las operaciones como una operación de conjunto, lo que afecta una gran cantidad de valores al mismo tiempo. Esto, por supuesto, significa que al motor de la base de datos se le debe decir QUÉ salir, y la base de datos puede optimizar su consulta.

Tanto Codd como Date criticaron a SQL porque estaban involucrados en la teoría, pero no participaron en la creación de SQL.

ver este video: http://player.oreilly.com/videos/9781491908853?toc_id=182164

Hay una gran cantidad de información de Chris Fecha. Recuerdo que Date criticó el lenguaje de programación SQL por ser un lenguaje terrible, pero no puedo encontrar el documento.

La crítica fue básicamente que la mayoría de los lenguajes permiten escribir expresiones y asignar variables a esas expresiones, pero SQL no.

Dado que SQL es un tipo de lenguaje lógico, supongo que podría escribir álgebra relacional en Prolog. Al menos tendrías un lenguaje real. Entonces podrías escribir consultas en Prolog. Y dado que en prolog tienes muchos programas para interpretar el lenguaje natural, puedes consultar tu base de datos usando un lenguaje natural.

De acuerdo con Uncle Bob, las bases de datos no van a ser necesarias cuando todo el mundo tiene SSD, porque la arquitectura de las SSD significa que el acceso es tan rápido como la RAM. Entonces puedes tener todos tus objetos en la RAM.

https://www.youtube.com/watch?feature=player_detailpage&v=t86v3N4OshQ#t=3287

El único problema con zanjas SQL es que se podría terminar sin un lenguaje de consulta de la base de datos.

Así que sí y no, el álgebra relacional se utilizó como inspiración para SQL, pero SQL no es realmente una implementación de álgebra relacional.

En el caso del Lisp, las cosas son diferentes. La idea principal fue que la implementación de la función eval en Lisp podría tener todo el lenguaje implementado. Es entonces cuando la primera implementación de Lisp es solo media página de código.

http://www.michaelnielsen.org/ddi/lisp-as-the-maxwells-equations-of-software/

a reír un poco: https://www.youtube.com/watch?v=hzf3hTUKk8U

La importancia de la programación funcional todo se reduce a funciones al curry y llamadas perezosos. Y nunca te olvides de los entornos y cierres. Y map-reduce. Esto significa que codificaremos en lenguajes funcionales en 20 años.

Ahora volviendo a OOP, no hay formalización de OOP.

Curiosamente, el segundo lenguaje OO que se haya creado, Smalltalk, solo tiene objetos, no tiene primitivos ni nada de eso. Y el creador, Alan Kay, creó bloques explícitamente para funcionar exactamente como funciona Lisp.

Algunas personas afirman que la POO podría formalizarse utilizando la teoría de categorías, que es una especie de teoría de conjuntos pero con morfismos. Un morfismo es un mapa que preserva la estructura entre los objetos. Entonces, en general, puede tener un mapa (f, colección) y obtener una colección con todos los elementos que se aplican.

Estoy bastante seguro de que Lisp tiene eso, pero Lisp también tiene funciones que devuelven un elemento de una colección, que destruye la estructura, por lo que el morfismo es un tipo especial de función y por eso, necesitarías reducir y limite las funciones en Lisp para que sean todos morfismos.

https://www.youtube.com/watch?feature=player_detailpage&v=o6L6XeNdd_k#t=250

El principal problema con esto es que las funciones no existen independientemente de los objetos en programación orientada a objetos, pero en la teoría de categorías que hacen. Por lo tanto, son incompatibles. Podría desarrollar un nuevo lenguaje para expresar la teoría de categorías.

Un lenguaje teórico experimental creado explícitamente para tratar de formalizar OOP es Z. Z se deriva de los requisitos de formalismo.

Otro intento es el formalismo de Luca Cardelli:

Javahttp://lucacardelli.name/Papers/PrimObjImp.pdf Javahttp://lucacardelli.name/Papers/PrimObj1stOrder.A4.pdf Javahttp://lucacardelli.name/Papers/PrimObjSemLICS.A4.pdf

soy incapaz de leer y entender que la notación. Parece un ejercicio inútil, ya que, hasta donde yo sé, nadie lo ha implementado de la misma manera que se implementó el cálculo de lamba en Lisp.