El siguiente libro gratuito está dirigido para todas aquellas personas interesadas en aprender sobre la teoría de tipos de Martin-Löf.
Sobre el Libro (Por el Autor)
En los últimos años se han introducido varios formalismos para la construcción de programas. Uno de esos formalismos es la teoría de tipos desarrollada por Per Martin-Löf.
Es muy adecuado como teoría para la construcción de programas, ya que es posible expresar tanto especificaciones como programas dentro del mismo formalismo.
Además, las reglas de prueba se pueden utilizar para derivar un programa correcto a partir de una especificación, así como para verificar que un programa dado tiene una determinada propiedad. Este libro contiene una introducción a la teoría de tipos como teoría para la construcción de programas.
Como lenguaje de programación, la teoría de tipos es similar a los lenguajes funcionales tipificados como Hope y ML, pero la principal diferencia es que la evaluación de un programa bien tipificado siempre termina.
En la teoría de tipos también es posible escribir especificaciones de tareas de programación, así como desarrollar programas demostrablemente correctos.
Por lo tanto, la teoría de tipos es más que un lenguaje de programación y no debe compararse con lenguajes de programación, sino con lógicas de programación formalizadas como LCF y PL/CV.
La Teoría
La teoría de tipos se desarrolló originalmente con el objetivo de ser una aclaración de las matemáticas constructivas, pero a diferencia de la mayoría de las otras formalizaciones de las matemáticas, la teoría de tipos no se basa en la lógica de predicados de primer orden.
En cambio, la lógica de predicados se interpreta dentro de la teoría de tipos a través de la correspondencia entre proposiciones y conjuntos. Una proposición se interpreta como un conjunto cuyos elementos representan las pruebas de la proposición.
Por lo tanto, una proposición falsa se interpreta como un conjunto vacío y una proposición verdadera como un conjunto no vacío.
El Capítulo 2 contiene una explicación detallada de cómo las constantes lógicas se corresponden con los conjuntos, explicando así cómo una proposición podría interpretarse como un conjunto.
Un conjunto no puede verse únicamente como una proposición; también es posible ver un conjunto como una descripción del problema.
Esta posibilidad es importante para la programación, porque si un conjunto puede verse como una descripción de un problema, puede, en particular, usarse como una especificación de un problema de programación.
Cuando un conjunto se ve como un problema, los elementos del conjunto son las posibles soluciones al problema; o de manera similar si vemos el conjunto como una especificación, los elementos son los programas que satisfacen la especificación. Por lo tanto, la pertenencia al conjunto y la corrección del programa son el mismo problema en la teoría de tipos, y dado que todos los programas terminan, corrección significa corrección total.
Contenido (Temas)
- Introducción
- La identificación de conjuntos, proposiciones y especificaciones.
- Expresiones e igualdad definitoria
- La semántica de las formas de juicio
- Reglas generales
- Y más…
Ficha Técnica
Año: 2004
Editor: Universidad de Göteborg
Idioma: Inglés
Tamaño: 693 KB
Licencia: Pendiente de revisión
Acerca de OpenLibra
OpenLibra busca reunir bajo una misma plataforma el mayor número de publicaciones libres posible. Esto implica una serie de riesgos en cuanto a los contenidos que han de asumirse y sobre los que queremos informar a nuestros usuarios.
En OpenLibra, los libros son responsabilidad exclusiva de sus autores. Esto significa que OpenLibra, no puede garantizar la validez de sus contenidos.
Preguntas Frecuentes
¿Qué quiere decir Biblioteca Libre?
Quiere decir que todos los libros que la componen están licenciados bajo alguno de los muchos tipos de licencia libre que existen y que, por tanto, el autor da su autorización para su reproducción y redistribución.
¿Son entonces todos los libros de esta biblioteca gratis?
Sí; al menos para su versión digital. Muchos autores, además, ofrecen la versión impresa (ya sea directamente o a través del circuito comercial habitual) por la que pueden cobrar lo que estimen oportuno.
Pero algunos de los libros que hay en la Biblioteca tienen Copyright…
El copyright y las licencias libres no son excluyentes. De hecho, las segundas se basan en la legislación sobre la primera para otorgar los derechos de copia y distribución. Es por eso que toda obra bajo una licencia libre, posee un copyright que garantiza la voluntad de su autor. Lo importante es qué permite ese copyright con respecto a la obra licenciada.
Pues he visto algún libro por aquí que tiene un Copyright y un ‘todos los derechos reservados’.
Cierto; en estos casos, lo más habitual es que la editorial haya devuelto los derechos de explotación al autor. Suele ocurrir con los manuales técnicos una vez pasado un tiempo prudencial o, por ejemplo, cuando se han agotado las ediciones impresas y no se pretende una reedición. Una vez los autores vuelven a tener el control, pueden ceder su trabajo al dominio público o permitir su redistribución libre para volver a poner su obra en circulación.
Si los libros son libres y gratis, ¿puedo hacer con ellos lo que quiera? ¿Los puedo imprimir, traducir y/o vender?
No; no puedes hacer aquello que su licencia no permita. Cómo se explica en el enlace de más arriba, algunas licencias solo permiten la descarga y redistribución sin ánimo de lucro. Si por ejemplo, quieres traducir la obra y editarla de forma ordinaria, algunos autores te exigirán que pagues los derechos pertinentes.
Descarga el Libro
Si te interesaron los temas, te dejamos aquí abajo el enlace de descarga.
¿Quieres Más?
Encuentra cursos y libros gratuitos, además de cupones de Udemy, en nuestros Telegram.
