Cálculo lambda escrito

El cálculo lambda tipado  es una versión del cálculo lambda que asigna etiquetas sintácticas especiales denominadas tipos a los términos lambda. Se permiten diferentes conjuntos de reglas para construir y asignar tales etiquetas, y dan lugar a diferentes tipos de sistemas.

Los cálculos de tipos son lenguajes de programación primitivos fundamentales que proporcionan la base para los lenguajes de programación funcionales basados ​​en tipos  ( lenguajes aplicativos), entre ellos ML y Haskell , así como los lenguajes de programación imperativos genéricos.

-el cálculo con tipos es el lenguaje de la categoría cerrada cartesiana , que establece una conexión directa con un modelo de computación como la máquina abstracta categórica . Desde un punto de vista, type -calculi puede considerarse como especializaciones de untyped -calculi, y desde otro punto de vista, por el contrario, los lenguajes tipificados pueden considerarse más fundamentales, de los cuales los no tipificados se obtienen como casos especiales. La teoría de la computación de D. Scott [1] proporciona un análisis de este fenómeno .

-El cálculo con tipos sirve como base para el desarrollo de nuevos sistemas de tipificación para lenguajes de programación, ya que es por medio de tipos y dependencias entre ellos que se expresan las propiedades deseadas de los programas.

En programación, los bloques informáticos independientes (funciones, procedimientos, métodos) de los lenguajes de programación con tipificación fuerte corresponden a expresiones de tipo.

Véase también

Notas

  1. ↑ Scott DS The lattice of flow diagrams.- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.- Berlín, Heidelberg, Nueva York: Springer-Verlag, 1971, pp. 311-372.

Literatura