En el presente ejemplo vamos a escribir en latex la formalización del simply typed λ-calculus. Puedes descargarte el ejemplo completo en 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:

\usepackage{amsmath}
\usepackage{semantic}
\usepackage{mathpartir}

Vamos a definir dos nuevos enviroments para la definición de nuestro lenguaje y para nuestras reglas de tipos y evaluación:

%% 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}}

Siempre es útil agregar algunos shortcuts para símbolos matemáticos muy usados:

%% Some symbol shortcuts
\mathlig{|-}{\vdash}
\mathlig{->}{\to}
\mathlig{-->}{\longrightarrow}

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

\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}

Reglas de derivación de tipos

{\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}

Reglas de evaluación

{\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}

Problemas conocidos

\usepackage[spanish]{babel}