Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
teaching:formal-latex-how-to [2010/08/25 20:55] – oalvarezteaching:formal-latex-how-to [2010/08/30 16:07] (current) – oalvarez
Line 1: Line 1:
 +En el presente ejemplo vamos a escribir en **latex** la formalización del simply typed λ-calculus.  Puedes descargarte el ejemplo completo en {{:teaching:stlc.zip|}}.
 +
 +Primero necesitamos listar que paquetes (packages) de latex necesitamos:
 +
 +  * AmsMath.sty (incluido en texlive-2009, si no lo tiene, pueden descargar lo de: [[http://tug.ctan.org/tex-archive/macros/latex/required/amslatex/math/]])
 +  * Semantic.sty (incluido en texlive-2009, si no lo tiene, pueden descargar lo de: [[http://www.ctan.org/tex-archive/macros/latex/contrib/semantic/]])
 +  *  MathPartit.sty (no incluido en texlive-2009, deben descargar lo de: [[http://pauillac.inria.fr/~remy/latex/mathpartir.sty]], documentación en: [[http://pauillac.inria.fr/~remy/latex/mathpartir.html]])
 +
 +
 +Para nuestro ejemplo, el encabezamiento del archivo latex, debería contener:
 +<code latex>
 +\usepackage{amsmath}
 +\usepackage{semantic}
 +\usepackage{mathpartir}
 +</code>
 +
 +Vamos a definir dos nuevos enviroments para la definición de nuestro lenguaje y para nuestras reglas de tipos y evaluación:
 +
 +<code latex>
 +%% This new env. facilitates to write our lang. definition
 +\newenvironment{syntaxcategory}[1]
 +  {\begin{array}[l]{lcll} \multicolumn{4}{l}{\mbox{\textbf{#1}}}\\}
 +  {\end{array}}
 +
 +%% This new env. facilitates to write our typing and evaluation rules
 +\newenvironment{inferbox}[0]
 +  {\begin{minipage}{\textwidth}\begin{mathpar}}
 +  {\end{mathpar}\end{minipage}}
 +</code>
 + 
 +Siempre es útil agregar algunos //shortcuts// para símbolos matemáticos muy usados:
 +
 +<code latex>
 +%% Some symbol shortcuts
 +\mathlig{|-}{\vdash}
 +\mathlig{->}{\to}
 +\mathlig{-->}{\longrightarrow}
 +</code>
 +
 +En el cuerpo de nuestro documento vamos agregar tres partes: (1) la definición de nuestro lenguaje (2) las reglas de derivación de tipos y por último (3) las reglas de evaluación.
 +
 +====== Definición del lenguaje ======
 +
 +<code latex>
 +\begin{displaymath}
 +\begin{syntaxcategory}{Language definition}
 +e & ::= & x \mid \lambda x \colon T. ~e \mid e ~e & \textrm{(expressions)}\\
 +v & ::= & \lambda x \colon T. ~e & \textrm{(values)}\\
 +T & ::= & T -> T  & \textrm{(types)}\\
 +\Gamma & ::= & \cdot \mid \Gamma[x \colon T]  & \textrm{(type env.)}\\
 +\end{syntaxcategory}
 +\end{displaymath}
 +</code>
 +
 +====== Reglas de derivación de tipos ======
 +
 +<code latex>
 +{\bf Typing rules} \boxed{\Gamma |- e \colon T} 
 +
 +\begin{inferbox}
 +\inference[(t-var)]{\Gamma(x)=T} %premises
 +{\Gamma |- x \colon T} %conclusion
 +\and 
 +\inference[(t-abs)]{ \Gamma[x \colon T_1] |- e \colon T_2} %premises
 +{\Gamma |- \lambda x \colon T. ~e \colon T_1 -> T_2} %conclusion
 +\and
 +\inference[(t-abs)]{ \Gamma |- e_1 \colon T_1 -> T_2 %premise1
 +& \Gamma |- e_2 \colon T_1} %premise2
 +{\Gamma |- e_1 ~e_2 \colon T_2} %conclusion
 +\end{inferbox}
 +</code>
 +====== Reglas de evaluación ======
 +
 +<code latex>
 +{\bf Evaluation rules} \boxed{e --> e'} 
 +
 +\begin{inferbox}
 +\inference[(e-app1)]{e_1 --> e_1'} %premises
 +{e_1 ~e_2 --> e_1' ~e_2} %conclusion
 +\and 
 +\inference[(e-app2)]{e_2 --> e_2'} %premises
 +{e_1 ~e_2 --> e_1 ~e_2'} %conclusion
 +\and
 +\inference[(e-appabs)]{} 
 +{(\lambda x \colon T. ~e) v --> [v/x]e} %conclusion
 +\end{inferbox}
 +</code>
 +
 +Al final obtenemos: {{:teaching:stlc.pdf|}}
 +====== Problemas conocidos ======
 +
 +  * La combinación de los paquetes arriba mencionados, junto a:
 +
 +<code latex>
 +\usepackage[spanish]{babel}
 +</code>
 +
 +provoca resultados inesperados, i.e. algunos símbolos matemáticos (declarados como shortcuts) no son procesados.
 +
 +