diff options
| -rwxr-xr-x | bib.bib | 15 | ||||
| -rwxr-xr-x | memoria.tex | 46 |
2 files changed, 47 insertions, 14 deletions
@@ -103,4 +103,19 @@ journal-URL = "http://onlinelibrary.wiley.com/journal/10.1002/(ISSN)1538-7305/issues/", remark = "The Wikipedia entry credits this paper as the foundation of modern cryptography.", +} +@Misc{Sorensen98, + author = {Morten Heine B. Sørensen and Pawel Urzyczyn}, + title = {Lectures on the Curry-Howard Isomorphism}, + year = {1998} +} +@article{Church40, + author = {A. Church}, + title = {A formulation of a simple theory of types}, + journal = {Journal of Symbolic Logic}, + year = {1940}, + volume = {5}, + pages = {56--68}, + note = {http://www.jstor.org/stable/2266866Electronic Edition}, + url = {http://www.jstor.org/stable/2266866} }
\ No newline at end of file diff --git a/memoria.tex b/memoria.tex index db67bbe..e05e085 100755 --- a/memoria.tex +++ b/memoria.tex @@ -185,16 +185,27 @@ Estos lenguajes se usan para declarar y definir tipos, funciones, axiomas, juegos, oráculos, adversarios, entidades involucradas en las pruebas, etc. \paragraph{Lenguaje de expresiones} -El lenguaje principal de especificación de EasyCrypt es el de las -\textbf{expresiones}, que define una serie de tipos y operadores sobre -ellos. EasyCrypt soporta tipos polimórficos de orden superior. Los operadores -son funciones totales definidas sobre tipos (conjuntos de valores). Aunque los -operadores se definen de forma abstracta (sin proporcionar una implementación), -EasyCrypt asume que todos los tipos están habitados, por lo que cualquier -aplicación de un operador debe generar un tipo habitado al menos por un -valor. La semántica de los operadores viene de la definición de lemas y axiomas -que describen su comportamiento de forma observacional, o extensional. Para -soportar operadores que reciban varios argumentos se usa la técnica de la +El lenguaje principal de especificación de EasyCrypt es el de las expresiones, +que define una serie de \textbf{tipos} (conjuntos de valores) y +\textbf{operadores} sobre ellos. En EasyCrypt, siguiendo la notación del cálculo +lambda tipado \cite{Church40}, la relación de tipado se representa con los dos +puntos. Así, (\rawec{b:bool}) denota la pertenencia del valor \rawec{b} al tipo +\rawec{bool}. EasyCrypt posee un potente sistema de tipos que soporta +polimorfismo y tipos de orden superior. Los tipos de orden superior están +parametrizados por otros tipos que se colocan delante: <<\rawec{int + list}>> significa <<lista de enteros>>. Los tipos se pueden generalizar +usando una variable de tipo (variable precedida de una comilla simple): +<<\rawec{'a list}>> significa <<lista de cualquier tipo>>. + +Los \textbf{operadores} son funciones definidas sobre tipos, y se introducen con +la palabra reservada <<\rawec{op}>>: (\rawec{op par : nat -> bool}). La aplicación +de un operador a un valor se realiza poniendo un espacio entre el operador y su +argumento: (\rawec{par 3}). Aunque los operadores se definen de forma abstracta (sin +proporcionar una implementación), la semántica de los operadores viene de la +definición de lemas y axiomas que describen su comportamiento de forma +observacional, o extensional. EasyCrypt asume que todos los tipos están +habitados, por lo que los operadores son funciones totales. Para soportar +operadores que reciban varios argumentos se usa la técnica de la \textbf{currificación} (\textit{currying}), que convierte una función de múltiples argumentos en una que al ser aplicada al primer argumento devuelve una nueva función que recibe el segundo argumento, y así sucesivamente. Por ejemplo @@ -202,10 +213,8 @@ $f : (A \times B\times C) \rightarrow D$ pasaría a ser $f : A \rightarrow (B \rightarrow (C \rightarrow D))$, o lo que es lo mismo, $f : A \rightarrow B \rightarrow C \rightarrow D$. -Los argumentos de los tipos polimórficos se colocan delante del tipo en -cuestión (\rawec{int list} significa <<lista de enteros>>), y se usa una comilla -simple delante de las variables de tipo (\rawec{'a list} significa <<lista de -cualquier tipo>>). +En este ejemplo se ilustra la metodología general de definición de tipos y +operadores en el lenguaje de expresiones de EasyCrypt: \begin{easycrypt}[caption=Lenguaje de expresiones]{}{} type 'a predicate = 'a -> bool. @@ -216,6 +225,15 @@ axiom find_head : hd l = x => find (lambda e, e = x) l = Some x. \end{easycrypt} +Las primeras dos líneas defininen los tipos \rawec{predicate} y +\rawec{option}. A continuación se define el operador \rawec{find}, que dado un +predicado y una lista de elementos, devuelve el elemento de la lista que +satisface el predicado (o \rawec{None} si ninguno lo satisface). Por último, se +define un axioma llamado \rawec{find_head}: si dado un elemento \rawec{x} y una +lista, siendo \rawec{x} el primer elemento de la lista, se llama a \rawec{find} +con el predicado <<igual a \rawec{x}>>, el resultado deberá ser (\rawec{Some + x}). + \paragraph{Lenguaje de expresiones probabilísticas} Para poder razonar sobre distribuciones de probabilidad, EasyCrypt proporciona un tipo (\rawec{'a distr}) que representa sub-distribuciones discretas sobre |