
\documentstyle{article}

\setlength{\textheight}{20cm}
\setlength{\textwidth}{13cm}
\setlength{\oddsidemargin}{1.5cm}
\setlength{\evensidemargin}{1.5cm}
\setlength{\topmargin}{0cm}

\input spanish.ldf\relax

\title {  C\'alculo de Construcciones Inductivas, Model--checking,
$\mu$--c\'alculo, HOAS  y Matem\'atica Inversa}

%\author{J.E. Freire Bra\~ nas}

%\def\eg{{\it e.g.\ }}
%\def\etc{{\it etc}}
%\def\LaTeX{L\kern-.36em\raise.3ex\hbox{a}\kern-.15em
%    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}
\newtheorem{proposition}{Proposition}[section]

\newtheorem{lemma}{Lema}[section]
\newtheorem{theorem}{Teorema}[section]
\newtheorem{definition}{Definici\'on}[section]
\newtheorem{exercice}{Ejercicio}[section]

\newtheorem{remark}{ Remark}[section]\newtheorem{example}{ Example}[section]\renewcommand{\theequation}{\thesection.\arabic{equation}}\newcommand{\rtimes}{\mbox{$\times \hspace{-2mm} \mid$}}\newcommand{\cat}{categor\'{\i}a}
\newcommand{\r}{\rightarrow}
\newcommand{\st}{\stackrel}
\newcommand{\la}{\leftarrow}
\newcommand{\e}{\epsilon}
\newcommand{\lr}{\leftrightarrow}

\newcommand{\lre}{\mbox{the representation of the expresion}}
\newcommand{\lam}{\mbox{$\lambda$}}


\pretolerance=10000
\tolerance=10000
\font\sy=cmsy10


\begin{document}

\label{firstpage}
\maketitle


%\input{epsf}



\thispagestyle{empty}

\vspace{1.5cm}
\begin{abstract}
En las pr\'oximas p\'aginas se plantea una introducci\'on a la
implementaci\'on del {\em model--checking} en {\bf Coq} cuando el conjunto
de estados del sistema a verificar es, previsiblemente, infinito. Para ello,
deberemos estudiar en qu\'e consiste, para qu\'e se usa, qu\'e formalismos
permiten describirlo, qu\'e l\'ogica es suficientemente amplia como para
poder abarcarlo sin perder consistencia, qu\'e  inconvenientes sint\'acticos
presenta y c\'omo poder sortearlos, qu\'e  sem\'antica describe con
correcci\'on el comportamiento de estos sistemas y,  por \'ultimo, c\'omo
encaja ello con los  recientes estudios de la  {\em matem\'atica inversa},
herramienta creada por Harvey Friedmann para  describir el conjunto
m\' {\i}nimo de axiomas que permiten obtener un  teorema determinado (o un
conjunto de ellos).

La  pretensi\'on de  automatizar el proceso utilizando el demostrador de
teoremas {\bf Coq}, herramienta creada en el INRIA para modelizar el
C\'alculo de Construcciones Inductivas, impone analizar  \'este con
profundidad y rigor.

\end{abstract}


\section{Introducci\'on}

Es bien sabido que los m\'etodos formales son \cite{tremblay}
{\em t\'ecnicas basadas en las matem\'aticas  usadas para describir las
propiedades de los sistemas de computaci\'on. Se utilizan para especificar,
desarrollar y verificar tales sistemas de una forma rigurosa y sistem\'atica.}

Los elementos claves de  un m\'etodo formal son:
\begin{enumerate}
\item un lenguaje formal para escribir las especificaciones;
\item reglas para chequear la calidad de las especificaciones;
\item estrategias y reglas para  refinar y verificar las especificaciones.
\end{enumerate}

Precisamos, pues, aclarar qu\'e entendemos por un lenguaje formal
de especificaciones. Por una parte, el lenguaje formal conlleva la existencia
de una sintaxis y una sem\'antica bien definidas. Ya que una especificaci\'on
 describe el qu\'e y no el c\'omo, el lenguaje de especificaci\'on debe
 hacer una descripci\'on del comportamiento externo de las componentes
del software. Para ello, debe describir sus principales propiedades de un modo
abstracto  y, adem\'as,  sin hacer indicaciones de c\'omo va a ser
implementado.

Las principales ventajas que aportan las especificaciones y los m\'etodos
formales es  que las primeras son m\'as expl\' {\i}citas y precisas, con
menor ambig\"{u}edad; adem\'as, el esfuerzo de formalizaci\'on ayuda a detectar
errores y problemas en una etapa temprana. Aportan, tambi\'en, una mejor
fundamentaci\'on de cara al trabajo de implementaci\'on. Y, por \'ultimo,
proveen de una base para hacer verificaci\'on formal.

Estamos interesados en sistemas reactivos, es decir, con una
interacci\'on constante con el entorno y con un comportamiento dirigido a
eventos, y concurrentes, o sea, aquellos donde el comportamiento est\'a
determinado por la interacci\'on de m\'ultiples procesadores (cada uno,
posiblemente, ejecutando una tarea diferente) que cooperan e intercambian
informaci\'on.

Para modelizar el comportamiento de un  sistema reactivo su comportamiento
se pueden describir las acciones que puede ejecutar. Ya que la computaci\'on
de  tal sistema es, posiblemente, infinita, usaremos sistemas de transinci\'on
etiquetados. La modelizaci\'on de sistemas concurrentes se realiza por medio
de la denominada sem\'antica {\em interleaving}, es decir, las acciones
concurrentes pueden suceder en cualquier orden y las acciones sincr\'onicas
son acciones efectuadas simult\'aneamente por dos o m\'a agentes.

Hay diferentes aproximaciones a la especificaci\'on de las propiedades:
\begin{enumerate}
\item l\'ogica modal: las propiedades locales de los estados ;
\item l\'ogica temporal: propiedades de la ejecuci\'on:
\begin{enumerate}
\item l\'ogica de tiempo lineal;
\item l\'ogica de tiempo ramificado.
\end{enumerate}
\end{enumerate}

Nosotros vamos a centrarnos en el $\mu$--c\'alculo modal, una l\'ogica
temporal modal que nos permite expresar las propiedades locales de los
estados. La parte modal nos la aportan dos construcciones:
\begin{enumerate}
\item posibilidad: $<$a$>\phi$ indicando que es posible realizar la acci\'on
a y alcanzar un estado que satisfaga $\phi;$
\item necesidad: [a]$\phi$ indicando que cuando se realiza la acci\'on a el
estado resultante satisface $\phi.$
\end{enumerate}

La parte temporal nos permite expresar los caminos de la ejecuci\'on y
describir cualitativamente la ocurrencia de sucesos en el tiempo. Dos
constructores surgen en este contexto:
\begin{enumerate}
\item Siempre: s  $\models$ AG $\phi$, indicando que $\phi$ se verifica en todos los
estados alcanzables desde el estado s;

\item Posiblemente: s  $\models$ EF $\phi$, expresando que, desde s, existe un camino donde,
posiblemente, $\phi$ se satisfar\'a.
\end{enumerate}
El $\mu$--c\'alculo modal es, entonces, tal como ha quedado indicado, una
l\'ogica temporal modal con operadores expl\' {\i}citos de punto fijo,
$\mu X.\phi, \; \nu X.\phi.$

Los constructores temporales Siempre y Posiblemente se expresan utilizando
estos operadores de punto fijo junto a la conjunci\'on y la disyunci\'on:
$$Siempre(\phi)=\nu X.\phi \wedge [-]X;$$
$$Posiblemente(\phi)=\mu X.\phi \vee <->X.$$

El {\em model--checking} es una t\'ecnica que trata de construir un modelo
(finito o infinito) de un sistema y chequear que una propiedad se satisface en ese modelo.
Es decir, es una t\'ecnica autom\'atica para verificar propiedades de
sistemas de estados posiblemente infinitos.

Debemos, pues, construir un modelo (M) del comportamiento del sistema,
especificar la propiedad ($\phi$) que \'este debe satisfacer (expresada, en
nuestro caso,  en el lenguaje del $\mu$--c\'alculo) y chequear que M satisface
$\phi$ o, en caso contrario, producir un contraejemplo.

El model--checking tiene, obviamente, ventajas e inconvenientes. Entre las
primeras cabe rese\~nar que la verificaci\'on est\'a complemante automatizada
y que puede producir contraejemplos que representan errores; entre los
segundos caba la posibilidad de explosi\'on del tama\~no de los estados.

Debemos distinguir entre el model--checking global y el local:
en el primero dados un modelo M y una f\'ormulo $\phi$ se ha de determinar
el conjunto de estados en M que satisfacen $\phi;$ en el segundo, dados un
modelo M, una f\'ormula $\phi$ y un estado s en M, se ha de determinar si
s satisface $\phi.$

\section{El C\'alculo de Construcciones Inductivas y Coinductivas}
El C\'alculo de Construcciones (CC a partir de ahora) es un metalenguaje
con las siguientes caracter\' {\i}sticas:
\begin{enumerate}
\item es de orden superior, es decir, permite  que definamos funciones que
tienen como argumentos otras funciones. Por ejemplo, el punto fijo del
$\mu$--c\'alculo tiene como tipo $(MuCalculo \r MuCalculo) \r MuCalculo$;
a partir de un endomorfismo en el $\mu$--c\'alculo nos devuelve un valor
de \'este;
\item posibilita la definici\'on de funciones con polimorfismo
param\'etrico por medio de la abstracci\'on de tipos. As\' {\i}, la
funci\'on identidad, $\lambda x.x,$ tiene como tipo $\Pi \alpha.\alpha \r
\alpha$ siendo $\alpha$ una variable de tipo que puede ser instanciada por
cualquier tipo concreto;
\item permite declarar tipos dependientes, o sea, tipos que dependen no s\'olo
de otros tipos sino tambi\'en de objetos de alg\'un  tipo. Por ejemplo, cuando
se desea multiplicar dos matrices es preciso que el n\'umero de columnas de
la primera matriz coincida con el n\'umero de filas de la segunda, siendo el
resultado del producto de una matriz $M_{n \times k}$ por una matriz
$M_{k \times m}$ una matriz de tipo $M_{n \times m}.$ Es en este caso donde
encaja la dependencia en los  tipos al permitir definir el tipo de las
matrices de n filas y m columnas, \verb"Matrix n m" siendo \verb"n, m"
n\'umeros naturales.
\end{enumerate}
Cuando a\~nadimos la  posibilidad de definir tipos inductivos (en cierto
sentido, tipos iniciales) tenemos el  C\'alculo de Construcciones Inductivas
(CCI); por \'ultimo, si definimos tambi\'en tipos coinductivos (tipos
terminales) tenemos el C\'alculo de Construcciones Inductivas y CoInductivas
(CCI$^{\infty}$).

Contamos en el CC con dos tipos $Set$ y $Prop$ que son impredicativos,
es decir, el t\'ermino $(P:\Sigma)P \r P$ (representando por $\Sigma$ tanto a
$Set$ como a $Prop$), tiene tambi\'en tipo $\Sigma.$ Por contra, hay un tipo
predicativo $Type$, indicado (aunque esos \' {\i}ndices no son visualizables)
de  forma que el tipo de $Type_i$ es $Type_{i+1}.$ Por consiguiente, el
tipo de $(X:Type_i)X \r X$ es $Type_{i+1}.$

La sintaxis del C\'alculo de Construcciones, es, por lo que acabamos de decir:
$$T ::= Set \mid Prop \mid Type$$
\[ \begin{array}{ll}
\mid x & \mbox{Variables}  \\
\mid (T \; T) & \mbox{Aplicaci\'on} \\
\mid [x:T]T & \mbox{Abstracci\'on} \\
\mid (x:T)T & \mbox{Producto} \\
\mid T \r T & \mbox{Tipo de las funciones}
\end{array} \]
El tipo de  las funciones, $A \r B,$ es una abreviatura de $(x:A)B$ cuando
$x$ no ocurre libre en $B.$ El hecho de que una expresi\'on tenga un tipo
garantiza que no puede haber computaciones infinitas. Es decir, si dado un
t\'ermino $e$ existe un tipo $\alpha$ tal que $\Gamma \vdash e:\alpha,$
 entonces $e$ es $\beta \eta$--normalizable (toda  cadena de reducciones termina
en una forma normal).


\section{La sintaxis del $\mu$--c\'alculo}
Sea {\em Atom}=\verb"{"p,q,r,...\verb"}"$\bigcup$
\verb"{"$\perp,\top $\verb"}" un conjunto de  \'atomos,
{\em Var}=\verb"{"X,Y,..\verb"}" un conjunto de variables y
{\em Act}=\verb"{"a,b,..\verb"}" un conjunto de acciones. Las f\'ormulas del
$\mu$--c\'alculo vienen expresadas, en nomenclatura BNF, como sigue:
$$\phi::=\perp \mid \top \mid X \mid p \mid \neg \phi \mid
\phi_1 \wedge \phi_2 \mid \phi_1 \vee \phi_2 \mid [a]\phi \mid <a>\phi
\mid \mu X.\phi \mid \nu X.\phi$$

Requeriremos en un momento dado (y explicaremos por qu\'e)  que cualquier variable libre en la f\'ormula
$\phi$ dentro del alcance de un operador de punto fijo ($\mu, \; \nu$) sea
{\em positiva}, es decir, est\'e precedida por un n\'umero par de negaciones. 

Surge, a la hora de la implementaci\'on en {\bf Coq} (o en cualquier
probador de teoremas basado en el C\'alculo de Construcciones Inductivas),
un problema: cuando queremos  declarar  el tipo $MuCalculo$ debemos aportar
los constructores  correspondientes a los puntos fijos, cuyos tipos son
 $$(MuCalculo \r MuCalculo) \r MuCalculo.$$

Pero tal formalizaci\'on no es  aceptada por {\bf Coq} puesto que vulnera
la cl\'ausula de positividad de la declaraci\'on inductiva de los tipos.
\'Esta restringe tal construcci\'on a tipos donde, en su llamada recursiva,
 no aparezcan en posici\'on impar (con respecto al s\' {\i}mbolo de
 funci\'on $\r).$ La raz\'on de tal restricci\'on radica en
 que el uso de  sintaxis de orden superior {\bf (HOAS)} conlleva la
 posibilidad  de construir valores {\em ex\'oticos} \cite{miculan}. Es decir, podemos
 declarar t\'erminos que no representen a ning\'un objeto del lenguaje que
 queremos determinar. Es m\'as, los t\'erminos ex\'oticos surgen cuando un
 tipo tiene un constructor de orden superior sobre un tipo inductivo. Es
 necesario, para precaverse contra estos t\'erminos espurios,  establecer
 reglas por medio de asignaciones de validez auxiliares.

\subsection{Una introducci\'on a la sintaxis de orden superior {\bf (HOAS)}}

La sintaxis abstracta de orden superior {\bf (HOAS)} es una t\'ecnica de
representaci\'on b\'asica  en muchas  herramientas deductivas, es decir, es
el metalenguaje dise\~nado para para la formalizaci\'on de sistemas deductivos.
La idea  que subyace a  esta t\'ecnica es representar las variables del
lenguaje objeto por medio de variables en el metalenguaje. Por consiguiente,
los constructores del lenguaje objeto que acotan  variables deben ser
representadas por constructores del metalenguaje que acotan las correspondientes
variables.

La codificaci\'on de sistemas l\'ogicos usando esta idea suele ser concisa
y elegante ya que  conceptos y  operaciones como pueden ser la acotaci\'on de
variables, su renombramiento, la sustituci\'on evitando la captura son
directamente soportadas por la herramienta y no es preciso codificarlas
separadamente en cada aplicaci\'on \cite{pfenning}.

En la pr\'actica, la sintaxis abstracta de orden superior explota la potencia
expresiva del $\lambda$--c\'alculo tipado para la representaci\'on de un
lenguaje objeto donde la $\lambda$--abstracci\'on proporciona el mecanismo
para representar las acotaciones. Analizamos, a continuaci\'on, un ejemplo
donde nos limitamos a tipos simples, sin polimorfismo ni dependencias.

Entonces, el metalenguaje simplemente tipado es el est\'andar:
$$Tipos \; puros: \; B::=a \mid B_1 \r B_2$$
$$Objetos: \; M::=c \mid x \mid \lambda x:B.M \mid M_1 \; M_2$$
$$Contexto: \; \psi::= \cdot \mid \psi ,x:B$$
$$Signatura: \; \Sigma::= \cdot \mid \Sigma ,a:type \mid \Sigma,c:B$$
donde $a$ representa un tipo constante, $c$ es un t\'ermino constante  y $x$
es una variable.

La asignaci\'on de tipos es, tambi\'en, est\'andar:
\[ \frac{\psi(x)=B}{\psi \vdash x:B} \]

\[ \frac{\psi(c)=B}{\psi \vdash c:B} \]

\[ \frac{\psi,x:B_1 \vdash M:B_2}{\psi \vdash \lambda x:B_1.M:B_1 \r B_2} \]

\[ \frac{\psi \vdash M_1:B_2 \r B_1 \; \; \psi \vdash M_2:B_2}{\psi \vdash M_1 \; M_2:B_1} \]

Las $\lambda$--expresiones no tipadas ilustran claramente la idea de sintaxis
abstracta de orden superior: las variables del lenguaje objeto se representan
como variables del metalenguaje:

Siendo las expresiones del $\lambda$--c\'alculo no tipado
$$e ::=x \mid lambda \; x.e \mid e_1 \odot e_2$$
y siendo $exp:type, \; lam:(exp \r exp) \r exp, \; app:exp \r (exp \r exp),$
las interpretamos como sigue
$$ \lceil lambda \; x.e \rceil=lam(\lambda x:exp. \lceil e \rceil)$$
$$ \lceil e_1 \odot e_2 \rceil=app \lceil e_1 \rceil \lceil e_2 \rceil$$
$$ \lceil x \rceil=x$$


Pero cuando se quiere implementar el $\lambda$--c\'alculo en el
C\'alculo de Construcciones Inductivas usando esta sintaxis se encuentra
uno con un obst\'aculo: el constructor correspondiente a la
 abstracci\'on $$(\lambda x.M)$$ tiene como tipo
 $$(Lambda \r Lambda) \r Lambda.$$
 Entonces, la abstracci\'on en el lenguaje objeto se expresa usando
 $\lambda$--abstracci\'on en el metalenguaje. Como  resultado, las variables
 acotadas en el lenguaje objeto se identifican con variables acotadas en el
 metalenguaje. Pero la aparici\'on negativa del tipo $Lambda$ en la anterior
 expresi\'on no es factible. Necesitamos, entonces, introducir un tipo
 separado de variables $(Var)$ de forma que la abstracci\'on tiene tipo
 $$(Var \r Lambda) \r Lambda.$$
 Este uso limitado de la sintaxis de orden superior todav\' {\i}a permite
 definir la abstracci\'on usando la $\lambda$--abstracci\'on en {\bf Coq} y
 los t\'erminos $\alpha$--convertibles en nuestro lenguaje objeto se
 corresponden con t\'erminos $\alpha$--convertibles en {\bf Coq}. Pero impide
 usar la $\beta$--reducci\'on de {\bf Coq} para definir la sustituci\'on a nivel
 de objeto.

Otro problema (ya mencionado anteriormente en el caso del $\mu$--c\'alculo) es
que al definir las $\lambda$--expresiones en {\bf Coq} como un tipo inductivo
(con los constructores de  aplicaci\'on,  abstracci\'on y  variables) se
genera un conjunto de t\'erminos mayor  que los posibles en el lenguaje
objeto original. Es necesario introducir predicados indicando cu\'ales de estas
expresiones son v\'alidas como $\lambda$--t\'erminos.

Un primer ejemplo de esta clase de expresiones es el siguiente t\'ermino de
$Lambda$ (donde hemos acotado $var$ a $nat,$ conjunto de los naturales):
$$Abs( \; \lambda x.Case \;  x \; of \; O \; \Rightarrow (Var \; O)
\mid (S \; n) =>(Var \; (S \; n)) \; end).$$

Esta expresi\'on es, extensionalmente, igual al $\lambda$--t\'ermino
$$Abs \; (\lambda x.(Var \; x))$$ por lo cual no resulta excesivamente
problem\'atico. S\' {\i} lo es, por contra, la expresi\'on
$$Abs( \; \lambda f.(Abs \; \lambda x.(\lambda f.\lambda x.
(Case \;  x \; of \; O \; \Rightarrow (Var \; O)$$
$$\mid (S \; n) =>(App \; (Var \; f) \; (Var \; n)) \; end) f \; x)))$$
ya que no representa, en absoluto, a ninguna $\lambda$--expresi\'on.

La teor\' {\i}a de la sintaxis abstracta de orden superior est\'a ligada a la
{\em teor\' {\i}a  de contextos.}

\subsubsection{La teor\' {\i}a  de contextos \cite{honsell}}
Un contexto es un $\lambda$--t\'ermino  con agujeros. Consta,
entonces, de un conjunto de axiomas que reflejan, en un nivel te\'orico,
algunas propiedades fundamentales de la noci\'on intuitiva de contexto y
aparici\'on de una variable. Informalmente,  su significaci\'on  es la
siguiente:
\begin{enumerate}
\item {\bf No saturaci\'on de las variables}: ning\'un t\'ermino puede
contener todas  las variables (posibilidad, pues, de disponer siempre de
variables de  refresco);
\item {\bf Extensionalidad de los contextos}: dos contextos son iguales si
coinciden sobre cualquier variable fresca; es  decir, si $M[x]=N[x]$ y
$x \not \in M, \; x \not \in N$ entonces $M=N;$
\item {\bf $\beta$--expansi\'on}: dado un t\'ermino $M$ y una variable $x$ hay
un contexto $N[\cdot]$ tal que $N[x]=M$ y $x$ no ocurre en $N[\cdot].$
\end{enumerate}

Los axiomas que rigen esta teor\' {\i}a son :
\begin{enumerate}
\item {\bf Decidibilidad de la igualdad}: $\forall x,y.x=y \vee x \neq y$
\item {\bf Decidibilidad de la pertenencia}:
$\forall x,M.x \in M \vee x \not \in M$

\item {\bf Insaturaci\'on}:$\forall M. \exists x.x \not \in fv(M)$
\item {\bf Monoton\'  {\i}a de $\not \in$}: $\forall x,y,M.x \not \in M[y]
\Rightarrow x  \not \in M[\cdot]$
\item {\bf $\beta$--expansi\'on}: $\forall M,x.\exists N[\cdot].x \not \in
fv(N[\cdot]) \wedge M=N[x]$
\item {\bf Extensionalidad}: $\forall M[\cdot],N[\cdot],x.x \not \in
fv(M[\cdot]) \cup fv(N[\cdot]) \Rightarrow M[x]=N[x] \Rightarrow M[\cdot]=
NM[\cdot]$
\end{enumerate}
El hecho de la introducci\'on de axiomas presenta serios problemas como pueden
ser los relacionados con su coherencia. Una rama de los fundamentos de las
 matem\'aticas que en los \'ultimos a\~nos se ha planteado analizar qu\'e
 conjunto m\' {\i}nimo de axiomas es necesario para demostrar un determinado
 teorema es la matem\'atica inversa ({\bf reverse mathematics} en la
 bibliograf\' {\i}a inglesa). Ha dado proficuos resultados en determinadas
 \'areas de las matem\'aticas (de hecho se ha convocado un congreso
 relacion\'andola con  cuestiones de verificaci\'on). Mencionaremos m\'as
 adelante algo relativo a  este t\'opico fundamentalmente en la subteor\' {\i}a
 que permite desarrollar matem\'atica constructiva, denominada $RCA_0.$

\section{Implementaci\'on del $\mu$--c\'alculo en {\bf Coq}}
\subsection{Sintaxis}
Usando, pues, la sintaxis abstracta de orden superior, implementamos en 
{\bf Coq} la sintaxis del $\mu$--c\'alculo. Notemos que las declaraciones
son convencionales  salvo en el caso de los puntos fijos puesto que, como
ya hemos visto, no cabe la  posibilidad  de definir constructores donde
el tipo no aparezca positivamente.
Introducimos como par\'ametros los conjuntos de los \'atomos, las acciones
 y las variables (de hecho, como tambi\'en hemos indicado, no cabe la
 posibilidad de declarar este \'ultimo conjunto inductivamente por el riesgo
  de generar t\'erminos ex\'oticos.
  Introducimos un par\'ametro \verb"N" que nos facilite negar las
  variables (necesario, como veremos, para establecer una sintaxis m\'as
  c\'omoda donde  prescindamos de  la negaci\'on sobre $\mu$--t\'erminos
  relegando \'esta \'unicamente a las variables  y a los \a'tomos
  \cite{igor}.

  Dada la condici\'on de puntos fijos de los  constructores \verb"Mu, Nu"
  estos deben  verificar  $\psi$\verb"(Mu("$\psi$\verb"))=Mu("$\psi$\verb")",
   $\psi$\verb"(Nu("$\psi$\verb"))=Nu("$\psi$\verb")". Ello implica que
   $\psi$ debe ser una funci\'on de tipo  \verb"PreMuForm->PreMuForm"
   de donde el tipo de \verb"Mu" (y, obviamente, el de \verb"Nu") debe ser
   \verb"(PreMuForm->PreMuForm)->PreMuForm" que, como ya queda indicado
   no es viable  en el C\'alculo de Construcciones Inductivas. Es  por ello que
   definimos los constructores \verb"Mu, Nu" con tipo
   \verb"(Var -> PreMuForm) -> PreMuForm". Analizaremos, posteriormente, desde
   un punto  de vista  sem\'antico de qu\'e funcional son, entonces,
   puntos fijos (ya que sint\'acticamente carece de sentido tal hip\'otesis).


\begin{verbatim}
Variable Atom, Var, Act:Set.

Parameter bot,top:Atom.
Parameter N:Var->Var.

Inductive PreMuForm:Set := 
  V  :Var -> PreMuForm
 |At :Atom    -> PreMuForm
 |Neg  :PreMuForm    -> PreMuForm
 |A  :PreMuForm -> PreMuForm -> PreMuForm
 |Or   :PreMuForm -> PreMuForm -> PreMuForm
 |Dia  :Act -> PreMuForm -> PreMuForm
 |Box  :Act -> PreMuForm -> PreMuForm
 |Mu : (Var -> PreMuForm) -> PreMuForm
 |Nu : (Var -> PreMuForm) -> PreMuForm
.

Coercion V:Var>->PreMuForm.
\end{verbatim}
La coerci\'on encaja el conjunto de las variables dentro de las
$\mu$--expresiones, por lo cual no ser\'a necesario precederlas del
constructor \verb"V", \'util para nosotros cuando queramos utilizar
la negaci\'on de una variable.

El porqu\'e de construir el tipo \verb"PreMuForm" en lugar de \verb"MuForm"
directamente radica en que no todas las expresiones as\' {\i} generadas dan
lugar a t\'erminos del $\mu$--c\'alculo {\em aceptables} por nosotros. Para
definir su  sem\'antica por medio de sistemas de transici\'on etiquetados de
tal forma que el comportamiento de los puntos fijos sea correcto (en cuanto
a ciertas condiciones de monoton\' {\i}a) ser\'a preciso que las
 variables libres en las f\'ormulas acotadas por estos
puntos fijos sean positivas (es decir, est\'en precedidas por un n\'umero
par de negaciones).
 Para establcer esta restricci\'on  es necesario indicar cu\'ando una variable
 aparece en  una $\mu$--expresi\'on, cu\'ando es libre y, por \'ultimo,
 cuando  es  positiva (indicando, de paso, cu\'ando no est\'a o cuando
 es negativa).
 \begin{verbatim}
Fixpoint  isin [x: Var;phi: PreMuForm] : Prop :=
  <Prop>Cases phi of
  (V y) => x=y 
| (At p) => False
| (Neg phi) => (isin x phi)
| (A phi psi) => (isin x phi) \/ (isin x phi)
| (Or phi psi) => (isin x phi) \/ (isin x phi)
| (Dia _ phi) => (isin x phi)
| (Box _ phi) => (isin x phi)
| (Mu F) => (y:Var)(isin x (F y))
| (Nu F) => (y:Var)(isin x (F y))
end.

Fixpoint notin [x:Var;phi:PreMuForm] : Prop :=
   <Prop>Cases phi of
     (V y) => ~(x=y)
   | (At p)     => True
   | (Neg phi) => (notin x phi)
   | (A phi psi) => (notin x phi) /\ (notin x psi)
   | (Or phi psi) => (notin x phi) /\ (notin x psi)
   | (Dia _ phi)   => (notin x phi)
   | (Box _ phi)   => (notin x phi)
   | (Mu F)      => (y:Var)~(x=y)->(notin x (F y))
   | (Nu F)      => (y:Var)~(x=y)->(notin x (F y))
   end.


Fixpoint posin [x:Var;phi:PreMuForm] : Prop :=
   <Prop>Cases phi of
     (V y) => True
   | (At p) => True
   | (Neg phi) => (negin x phi)   
   | (A phi psi) => (posin x phi) /\ (posin x psi)
   | (Or phi psi) => (posin x phi) /\ (posin x psi)
   | (Dia _ phi) => (posin x phi)
   | (Box _ phi) => (posin x phi)
   | (Mu F)  => (y:Var)~(x=y)->(posin x (F y))
   | (Nu F)  => (y:Var)~(x=y)->(posin x (F y))
   end
with negin [x:Var;phi:PreMuForm] : Prop :=
   <Prop>Cases phi of
     (V y)    => ~(x=y)
   | (At p) => True
   | (Neg phi) => (posin x phi)
   | (A phi psi) => (negin x phi) /\ (negin x psi)
   | (Or phi psi) => (negin x phi) /\ (negin x psi)
   | (Dia _ phi) => (negin x phi)
   | (Box _ phi) => (negin x phi)
   | (Mu F)  => (y:Var)~(x=y)->(negin x (F y))
   | (Nu F)  => (y:Var)~(x=y)->(negin x (F y))
   end.
 \end{verbatim}
 Es necesario establecer que siempre tendremos variables frescas (es decir,
 que \verb"Var" es un conjunto  infinito) y poder determinar cuando dos
 variables  son diferentes. Lo primero lo resolvemos por medio de un
 axioma indicando un morfismo sobreyectivo entre el conjunto de los n\'umeros
 naturales y \verb"Var". Lo segundo es el lema de separaci\'on que nos dice que,
 si tenemos dos variables y una aparece  en una f\'rmula y la otra no, entonces,
 son diferentes.
 \begin{verbatim}
Axiom Var_nat : (Ex [srj:Var->nat](n:nat)(Ex [x:Var](srj x)=n)).

Lemma separation: (x,y:Var; phi:PreMuForm)(notin x phi)->(isin y phi)
->~x=y.
 \end{verbatim}
Podemos, entonces,  indicar ya cu\'ando una $\mu$--expresi\'on es una
f\'ormula del $\mu$--c\'alculo (las apariciones de las variables libres son
positivas) y, por consiguiente, definir el tipo de las $\mu$--f\'ormulas,
\verb"MuForm", a saber, las $\mu$--expresiones bien formadas:
\begin{verbatim}
Fixpoint iswf [phi:PreMuForm]:Prop :=
   <Prop>Cases phi of
   (V _) => True
  |(At _) => True
  |(Neg phi) => (iswf phi)
  |(A phi psi) => (iswf phi) /\ (iswf psi)
  | (Or phi psi) => (iswf phi) /\ (iswf psi)
  | (Dia _ phi) => (iswf phi)
  | (Box _ phi) => (iswf phi)
  | (Mu F) => (x:Var)(iswf (F x))/\((notin x (Mu F)) -> (posin x (F x)))
  | (Nu F) => (x:Var)(iswf (F x))/\((notin x (Nu F)) -> (posin x (F x)))
 end.
 

Inductive MuForm: Set := 
muform :(phi:PreMuForm)(iswf phi)->MuForm.

\end{verbatim}

\subsection{Sem\'antica}
La sem\'antica de las expresiones del $\mu$--c\'alculo se obtiene usando
los sistemas de transici\'on o modelos de Kripke.

\begin{definition}
Un sistema de transici\'on es una terna $M=(S,R,\rho)$ donde:
\begin{enumerate}
\item $S$ es un conjunto no vac\' {\i}o que representa el conjunto de estados;
\item $R$ es una funci\'on que a cada acci\'on le asocia una relaci\'on binaria
en $S$, es decir, $R:Act \r 2^{S \times S}$;
\item $\rho$ asocia a cada \'atomo un conjunto de estados, $rho:Atom \r 2^S.$
\end{enumerate}
\end{definition}
Cuando tenemos un modelo $M$ y una  valoraci\'on $Val:Var \r 2^S$, denotamos
por medio de $Val[X \r T]$ la valoraci\'on que a la variable $X$ le  asigna
  $T$  y a una variable  $Y$ diferente de $X$ le asigna  $Val(Y).$

\begin{definition}
La sem\'antica (o sea, el significado) de una f\'ormula $\alpha$ es el conjunto
de estados en los que es verdadera respecto del modelo $M$ y la valoraci\'on
$Val$.
\end{definition}
Entonces, la sem\'antica (denotada por $\parallel \cdot \parallel$, donde se
sobreentienden  el modelo y la valoraci\'on) de las $\mu$--expresiones es la
siguiente:
$$\parallel X \parallel=Val(X);$$
$$\parallel p \parallel=\rho(p);$$
$$\parallel \neg \alpha \parallel=S-\parallel \alpha \parallel;$$
$$\parallel  \alpha \vee \beta \parallel=\parallel \alpha \parallel
\cup \parallel \beta \parallel;$$
$$\parallel  \alpha \wedge \beta \parallel=\parallel \alpha \parallel
\cap \parallel \beta \parallel;$$
$$\parallel  <a>\alpha \parallel= \{ s \in St \mid \exists s' \in St.
(s,s') \in R(a) \wedge s' \in \parallel  \alpha \parallel \};$$

$$\parallel  [a]\alpha \parallel= \{ s \in St \mid \forall s' \in St.
(s,s') \in R(a) \Rightarrow s' \in \parallel  \alpha \parallel \};$$

$$\parallel  \mu(X).\alpha(X) \parallel=\bigcap \{ T \subset St \mid
 \parallel  \alpha \parallel_{Val[X \r T]} \in T \} ;$$

$$\parallel  \nu(X).\alpha(X) \parallel=\bigcup \{ T \subset St \mid
T \in \parallel  \alpha \parallel_{Val[X \r T]} \}.$$


Al igual que hicimos con la sintaxis, comenzamos estableciendo la sem\'antica
de las $\mu$--expresiones para, posteriormente, definirla para las
$\mu$--f\'ormulas bien formadas.
\begin{verbatim}
Variable St:Set.

Variable R:Act->St->St->Prop.


Variable Rho:Atomo -> (Ensemble St). 

Definition complementario:=Complement.

Definition instance := [Val:Var->(Ensemble St)] [x:Var][T:(Ensemble St)]
[y:Var]Cases y of 
x => T
|y0 => (Val y0)
end.


Fixpoint PreSem [phi:PreMuForm]:(Var->(Ensemble St))->(Ensemble St):=
	Cases phi of 
  (V y) => [Val:(Var->(Ensemble St))](Val y)  
| (At p) => [Val:(Var->(Ensemble St))](Rho p)
| (Neg psi) => [Val:(Var->(Ensemble St))]
                (complementario St (PreSem  psi Val))
| (A psi psi') => [Val:(Var->(Ensemble St))]
                (Intersection St (PreSem psi Val) (PreSem psi' Val))
| (Or psi psi') => [Val:(Var->(Ensemble St))]
                (Union St (PreSem psi Val) (PreSem psi' Val))
| (Dia ct psi) => [Val:(Var->(Ensemble St))]
                [s:St](EX t:St|(R ct s t)/\(In St (PreSem psi Val) t))
| (Box ct psi) => [Val:(Var->(Ensemble St))]
                [s:St](t:St)(R ct s t)->(In St (PreSem psi Val) t)
| (Mu alpha) => [Val:(Var->(Ensemble St))]
                [s:St](Y:(Ensemble St))(x:Var)(Included St (PreSem (alpha x)
                (instance Val x Y)) Y)->(In St Y s)
|(Nu alpha) => [Val:(Var->(Ensemble St))]
                [s:St] (EXT Y:(Ensemble St)| (x:Var)(Included St Y
                (PreSem (alpha x) (instance Val x Y)) )/\(In St Y s))
end.


Definition Semantic  := 
[phi:MuForm ]
Cases phi  of
(muform psi caract) => (PreSem psi)
end.

\end{verbatim}

Cuando $\alpha$ es una $\mu$--f\'ormula y $X$ es una variable libre en
$\alpha$, podemos construir la funci\'on $f_{\alpha}:2^{S} \r 2^{S}$ definida
por $$f_{\alpha}(T)=\parallel \alpha \parallel_{Val[X \r T]}.$$
\begin{proposition}
Si la variable $X$ aparece s\'olo positivamente en $\alpha$ entonces
la funci\'on $f_{\alpha}$ es mon\'otona.
\end{proposition}
Lo enunciamos y probamos en {\bf Coq}:
\begin{verbatim}
Fixpoint  isfree [x: Var;phi:PreMuForm] : Prop :=
  <Prop>Cases phi of
  (V y) => x=y 
| (At p) => False
| (Neg p) => False
| (A phi psi) => (isfree x phi) /\(isfree x psi)
| (Or phi psi) => (isfree x phi) /\(isfree x psi)
| (Dia _ phi) => (isfree x phi)
| (Box _ phi) => (isfree x phi)
| (Mu F) => (y:Var)(~(x=y)->(isfree x (F y)))
| (Nu F) => (y:Var)(~(x=y)->(isfree x (F y)))
end.

Definition falpha := [x:Var][alpha:(PreMuForm )][Val:Var->(Ensemble St)]
[T:(Ensemble St)](PreSem alpha (instance Val x T)).


Lemma monotonia : (x:Var)(alpha:(PreMuForm ))(Val:Var->(Ensemble St))
(posin  x alpha)->(isfree x alpha)->(U,V:(Ensemble St))(Included St U V)
->(Included St (falpha x alpha Val U) (falpha x alpha Val V)).


\end{verbatim}
Al ser mon\'otona podemos aplicar el teorema de Tarski por lo cual
$f_{\alpha}$ tendr\'a un menor y un mayor  punto  fijo que, como parece
obvio despu\'es del desarrollo hasta aqu\' {\i} establecido, ser\'an los
que nosotros hemos identificado con los constructores $Mu$ y $Nu:$
\begin{verbatim}
Lemma menor_punto_fijo : (x:Var)(alpha:Var->(PreMuForm ))
(Val:Var->(Ensemble St))(posin  x (alpha x))->
(isfree x (alpha x))->(PreSem (Mu  alpha) Val)
==(falpha x  (Mu  alpha) Val (PreSem (Mu  alpha) Val)).


Lemma Mayor_Punto_Fijo : (x:Var)(alpha:Var->(PreMuForm ))
(Val:Var->(Ensemble St))(posin  x (alpha x))->
(isfree x (alpha x))->(PreSem (Nu  alpha) Val)
==(falpha x  (Nu  alpha) Val (PreSem (Nu  alpha) Val)).

\end{verbatim}
En el camino que nos permitir\'a construir las expresiones del $\mu$--c\'alculo
sin negaciones establecemos  resultados que relacionan
el operador diamante con el oeprador cuadrado. Notemos que, al introducir
como dominio sem\'antico el conjunto $2^S$ hemos entrado  en el campo de la
l\'ogica cl\'asica, de donde, de cara a las pruebas que hemos de llevar a
cabo, precisamos relaciones en esa l\'ogica que para expresar la
negaci\'on de forma acorde a nuestras intenciones:
\begin{verbatim}
Lemma imply_to_not_and : (P,Q:Prop)~(P->~Q)->P/\Q.

Lemma Not_and_to_imply : (P,Q:Prop)~(P/\~Q)->P->Q.
\end{verbatim}
Con esos dos lemas podemos probar las siguientes propiedades correspondientes
a la complementariedad de conjuntos:

\begin{verbatim}
Lemma Prev1:(ct:Act)(psi:PreMuForm)(Val:Var->(Ensemble St))(x:St)
(complementario St [s:St](t:St)(R ct s t)->
(In St (complementario St (PreSem psi Val)) t) x)
==([s:St]~(t:St)(R ct s t)->
(In St (complementario St (PreSem psi Val)) t) x).



Lemma Prev2: (ct:Act)(psi:PreMuForm)(Val:Var->(Ensemble St))(x:St)
(EX t:St|~((R ct x t)->(complementario St (PreSem psi Val) t)))
->(EX t:St|(R ct x t)/\(PreSem psi Val t)).


Lemma Prev3:(ct:Act)(psi:(PreMuForm ))(Val:Var->(Ensemble St))
(x:St)(complementario St [s:St]
(EX t:St|(R ct s t)/\(complementario St (PreSem psi Val) t)) x)
==([s:St]~(EX t:St|
(R ct s t)/\(complementario St (PreSem psi Val) t)) x).



Theorem no_box_dia : (ct:Act)(psi:(PreMuForm ))(Val:Var->(Ensemble St))
(PreSem (Neg  (Box  ct (Neg  psi) ) )Val)
==(PreSem (Dia  ct psi) Val). 




Theorem no_dia_box : (ct:Act)(psi:(PreMuForm ))(Val:Var->(Ensemble St))
(PreSem (Neg  (Dia  ct (Neg  psi) ) )Val)
==(PreSem (Box  ct psi) Val). 
\end{verbatim}

Para poder expresar de forma similar la relaci\'on entre las interpretaciones
de los constructores $Mu$ y $Nu$
\begin{verbatim}
 Theorem Mu_no_Nu : (alpha:Var->PreMuForm)(Val:Var->(Ensemble St))
(PreSem (Neg (Mu alpha)) Val)==(PreSem (Nu [X:Var](Neg (alpha (N X)))) Val).


Theorem Nu_no_Mu : (alpha:Var->PreMuForm)(Val:Var->(Ensemble St))
(PreSem (Neg (Nu alpha)) Val)==(PreSem (Mu [X:Var](Neg (alpha X)) ) Val).
\end{verbatim}
hemos de indicar cu\'al es la interpretaci\'on
de  $ (\neg (\alpha ( \neg X))).$ \'Esta no podemos inferirla de la
interpretaci\'on sem\'antica puesto que la negaci\'on de la variable la
hemos definida como una coerci\'on, por lo cual no tenemos ninguna regla
para ella. As\' {\i}, debemos introducirla como un axioma:
\begin{verbatim}
Axiom Semantica_no_var:(alpha:Var->PreMuForm)(Val:Var->(Ensemble St))
(Y:(Ensemble St))(X:Var)
(PreSem (alpha (N X)) (instance Val (N X) Y))==
(complementario St (PreSem (alpha X) (instance Val X (complementario St Y)))).

\end{verbatim}




\begin{definition}
Sean $M=(S,R,\rho)$ un modelo del $\mu$--c\'alculo y $Val:Var \r 2^S$ una
valoraci\'on sobre \'el. Diremos que una f\'ormula $\alpha$ se satisface en
un estado $s \in S$ bajo la valoraci\'on $Val$ (y lo escribirimos
$\{M,s,Val \} \vdash \alpha$) si se verifica que $$s \in
\parallel \alpha {\parallel_{Val}}^M.$$
\end{definition}
\begin{definition}
Una f\'ormula $\alpha$ es v\'alida ($\vdash \alpha$) si y s\'olo si
lo es para cualesquiera modelo, estado y valoraci\'on, es decir,
$$\forall M.\forall s.\forall Val.\{ M,s,Val \} \vdash \alpha.$$
\end{definition}
Tras haber cerrado al secci\'on podemos proceder a la declaraci\'on en
{\bf Coq} de esta definici\'on:
\begin{verbatim}

Definition Valid := [alpha:(PreMuForm Atom Var Act)][S:Set]
[R:Act->S->S->Prop][rho:Atom->(Ensemble S)][s:S][Val:Var->(Ensemble  S)]
(In S (PreSem Atom  Var Act S R rho alpha Val) s).
\end{verbatim}

 \section{Matem\'atica Inversa }
En la \'ultima fase de la implementaci\'on anterior hemos hecho uso
de un axioma que, indefectiblente, precis\'abamos para poder llegar  a las
conclusiones deseadas y que no pod\' {\i}a ser obtenido de otra forma
al involucrar t\'erminos que no aparec\' {\i}an de forma natural en el
lenguaje.

En efecto, tal como hemos indicado, cuando queremos probar la equivalencia
sem\'antica entre $\mu(X).F(X)$ y $\neg \nu(x).\neg(F (\neg X))$ y al haber
incorporado la negaci\'on sobre las variables como una coerci\'on externa y
no como una posibilidad de los constructores del $\mu$--c\'alculo, debemos
asumir como algo verdadero el axioma que hemos denominado
\verb"Semantica_no_var" para poder seguir avanzando.

Algo an\'alogo sucede cuando queremos saber qu\'e axiomas (en forma de
constructores)  debemos usar para determinar  una  relaci\'on
bien fundada sobre, por ejemplo, un tipo dependiente polim\'orfico.

Partamos de un caso singular:
\begin{verbatim}
Variable A:Set.

Inductive tipo :nat->Set :=
nil:(tipo O)
|cons:(n:nat)A->(tipo n)->(tipo (S n)).
\end{verbatim}

Deseamos obtener el resultado 
\begin{verbatim}
Variable B:(n:nat)(tipo n)->Set.

Variable Phi:(m:nat)(x: (tipo m))((n:nat)(y:(tipo n))
(R n y m x)->(B n y))->(B m x).

Theorem hh:(m:nat)(x:(tipo m))(n:nat)(y:(tipo n))(R n y m x)->(B n y).

Theorem HH:(n:nat;a:A;x:(tipo n))(B n x)->(B (S n) (cons n a x)).

Theorem tipo_rec_gen : (n:nat)(o:(tipo n))(B  n o).
\end{verbatim}
que establezca que, bajo la hip\'otesos $\phi$, se verifica el
principio de inducci\'on bien fundada (es decir, que la relaci\'on $R$ sobre
 $tipo$ es bien fundada). El problema que tenemos es, pues, triple:
\begin{enumerate}
\item definir la relaci\'on $R$ de forma que sea bien fundada;
\item construirla de tal forma que se corresponda con un orden estructural
(grosso modo, que dado un valor $v$ de $tipo$, es menor (en el sentido de estar
 relacionado) que el valor $cons \dots v \dots);$

\item determinarla de la forma m\'as general posible para que el m\'etodo
de demostraci\'on de la buena fundaci\'on sea "casi" autom\'atico (es decir,
poder disponer de la capacidad de trasladar las t\'acticas de la demostraci\'on
a cualquier otro tipo simplemente amold\'andolas a los constructores
adecuados).
\end{enumerate}
Hemos visto que la derivaci\'on de esa relaci\'on no es una cuesti\'on
tan obvia. La primera que a uno se le ocurre con $tipo$ es, siguiendo la
norma estructural indicado en el segundo \' {\i}tem anterior
\begin{verbatim}
Inductive R [n:nat]:(tipo n)->(tipo (S n))->Prop :=  
Rax:(a:A)(x:(tipo n))(R n x (cons1 n a x)).
\end{verbatim}
Pero tiene serias carencias ya que no nos otorga esa capacidad de
automatizaci\'on (es tan simple que al intentar extrapolarla a un tipo m\'as
complejo como puede ser el de los ordinales de Brouwer nos deja sin
alternativas de actuaci\'on).

Es el hecho de trabajar con ambos tipos (el dependiente y el de los ordinales)
lo que nos permite englobar una definici\'on para esa relaci\'on:
\begin{verbatim}
Inductive R [n:nat]:(tipo n)->(m:nat)(tipo m)->Prop :=  
Rax:(x:(tipo n))((m:nat)(y:(tipo m))(R n x m y)->
(a:A)(R n x (S m) (cons m a y))).
\end{verbatim}
para $tipo$ y
\begin{verbatim}
Inductive ord:Set:=
Ord0:ord
|OrdS:ord->ord
|lim:(nat->ord)->ord.

Inductive R   :ord->ord->Prop :=  
R1 : (o1,o2:ord)(R o1 o2)->(R o1 (OrdS o2))
|R2:(f:nat->ord)(n:nat)(o:ord)(R o (f n))->(R o (lim f)).
\end{verbatim}
para los ordinales.

Es sabido que al final del siglo XIX y en los inicios del XX hubo serios
intentos de  hallar una fundamentaci\'on precisa para las matem\'aticas.
De ese estudio nacieron ramas de \'estas como son la teor\' {\i}a de modelos,
la teor\' {\i}a de la computabilidad y la teor\' {\i}a de las pruebas. Pero
desde entonces el an\'alisis de estas cuestiones hab\' {\i}a declinado
sobremanera hasta principios de los a\~nos en que Harvey Friedmann las retom\'o
estableciendo un programa de b\'suqueda de esos fundamentos denominado
{\bf matem\'atica inversa} (Reverse Mathematics en la bibliograf\' {\i}a
al uso).

En el a\~no  1982 da Simpson una charla  donde, dentro de la aritm\'etica de
segundo orden, aisla los cinco  grandes sistemas de que  \'esta se
compone: $RCA_0, \; WKL_0, \; ACA_0, \;  ATR_0, \;  {\Pi_1}^1-CA_0.$

 La cuesti\'on b\'asica que pretende estudiar la matem\'atica inversa es,
 entonces,  cu\'ales son los axiomas de existencia necesarios para probar los
 teoremas conocidos de las  matem\'aticas.

 Aunque resulte  sorprendente, si dado un teorema $\tau$ de la matem\'atica
 ordinaria, uno se cuestiona cu\'al es el subsistema de $Z_2$ (aritm\'etica
 de segundo orden)  m\'as d\'ebil en el cual $\tau$ es demostrable, resulta que,
 para una  buena cantidad de  estos teoremas  esta pregunta puede ser
 contestada. De  hecho, en la  mayor\' {\i}a  de los  casos, ese sistema
 (denot\'emoslo por $S(\tau)$) ser\'a uno de los  cinco previamente
 mencionados.

(Aunque no he encontrado aplicaciones a temas concretos en el \'area de
 la computaci\'on, he de reconocer que en los dos problemas anteriores
 (tal vez un poco menos en el primero puesto que el axioma es obvio) s\' {\i}
 me  ha sido de  ayuda ese paso atr\'as a que obliga el estudio de la
 matem\'atica  inversa para no cernirse sobre un hecho concreto sino intentar
 englobarlo en  una estructura (paso del  tipo dependiente a los ordinales y
 posterior  generalizaci\'on) donde la concreci\'on del resultado quede,
 quiz\'a, enmascarado por el contexto menos definido pero las necesidades
 de la automatizaci\'on s\' {\i} son  m\'as claramente perceptibles.)


 Fundamentalmente, el campo de actuaci\'on de la matem\'atica inversa es
  el lenguaje de la aritm\'etica de  segundo  orden ($L_2$), ya que
  \cite{simpson}  {\em ese lenguaje es el m\'as d\'ebil y suficientemente rico
  para expresar   y desarrollar el grueso del n\'ucleo matem\'atico.}
 Este  sistema consta de dos clases:
 \begin{enumerate}
\item Variables de n\'umeros: m, n,... que recorren el conjunto de los
naturales $w=\{ 0,1,2,3, \dots \}$;
\item Variables de conjunto: X, Y,.. recorriendo subconjuntos de $w.$
Sobre $w$ tenemos las operaciones $+, \; \times, \; =$ adem\'as de una
relaci\'on de pertenencia $\in= \{ (n,X) \mid n \in X \}  \in w \times P(w).$
\end{enumerate}

Es sumamente interesante saber que cada uno de esos modelos de la matem\'atica
inversa conduce a buenos resultados  en determinadas ramas de la matem\'atica.
De hecho, los especialistas en matem\'atica inversa clasifican los teoremas
matem\'atiocs de acuerdo con el subsistema de $Z_2$ en que son demostrables.

Por ejemplo,  el constructivismo se analiza dentro del sistema $RCA_0$ mientras
que el reduccionismo finitista de Hilbert es estudiado dentro del sistema
$WKL_0$ (el sistema $RCA_0$ al que se le ha a\~nadido el lema d\'ebil de
K\"{onig} que establece lo siguiente:

cualquier \'arbol infinito de sucesiones binarias contiene un camino infinito.

La metodolog\' {\i}a de la matem\'atica inversa se basa en tres componentes:
\begin{enumerate}
\item Una teor\' {\i}a base $B$ (que ser\'a alg\'un subsistema de $Z_2;$
\item una sucesi\'on $S_1,\; S_2,\dots$ de axiomas de existencia de longitud
creciente;
\item alg\'un teorema matem\'atico.
\end{enumerate}
Entonces la pretensi\'on de la matem\'atica inversa es establecer un metateorema
de la forma $B \vdash \phi \leftrightarrow S_i.$ Los resultados de esta forma
establecen no s\'olo que el teorema $\phi$ puede ser probado en el sistema
$B cup S_i$ sino tambi\'en que el axioma $S_i$ puede ser deducido del teorema
$\phi.$ $S_i$ es el axioma m\'as d\'ebil de forma que $\phi$ puede ser
demostrado.

Los axiomas en los que se fundamenta el sistema $RCA_0$ (denominado de
{\em recursi\'on comprensiva}) son los de la aritm\'etica b\'asica a los
que se a\~nade el esquema de inducci\'on completo de segundo orden
$$\psi(0) \wedge \forall n.(\psi(n) \r \psi(n+1)) \r \forall n.\psi(n)$$
y el esquema de comprehensi\'on completo de segundo orden, o sea,
$$\exists X \mid \forall n.(n \in X \leftrightarrow \phi(n)$$
siendo $\phi(n)$ una f\'ormula de $Z_2$ en la cual $X$ no ocurre libremente.

$S \subset P(\omega)$ es un $w$--modelo del sistema $RCA_0$ si y s\'olo si:
\begin{enumerate}
\item $S \neq \emptyset;$
\item $A \in S$ y $B \in S$ implica que $A \oplus B \in S;$
\item $A \in S$ y $B \leq_{T} A$ implica que $B \in S.$
\end{enumerate}

De hecho, $RCA_0$ tiene un $\omega$--modelo m\' {\i}nimo,
$$REC= \{A \in P(\omega) \mid A \; is \; recursive \},$$
donde  que el conjunto $A$ sea recursivo en los conjuntos
$B_1,B_2,\dots,B_n$ significa que la funci\'on caracter\' {\i}stica de
$A$ es computable a partir de las  computaciones de las respectivas funciones
caracter\' {\i}sticas asociadas a $B_1,B_2,\dots,B_n.$

Hay una buena cantidad de matem\'aticas que pueden probarse usando este
sistema (que, como se ve en sus presupuestos axiom\'aticos, es sumamente
d\'ebil). Por ejemplo, el teorema de la categor\' {\i}a de Baire, el teorema
del valor intermedio, los lemas de Urysohn  y el de extensi\'on de Tietze e,
 incluso, el teorema de completitud de G\"{o}del. En cambio, en este sistema
 no es demostrable el teorema de Bolzano--Weierstrass (cualquier sucesi\'on
 acotada de  n\'umeros reales tiene una subsucesi\'on convergente).

En lo que a  nosotros nos  concierne, el desarrollo formal de la matem\'atica
ordinaria dentro de $RCA_0$ es muy similar al constructivismo al estilo
de Bishop aunque difiere en la interpretaci\'on cl\'asica que este sistema
conlleva (incluido el principio del tercio excluso).
.

\begin{thebibliography}{}

\bibitem[Despeyroux et al 1995]{felty}{J. Despeyroux, A. Felty, A. Hirschowitz,
Higher--order abstract syntax in {\bf Coq}.}
{\it Proceedings of the ICTLCA. LNCS 902 }(1995)

\bibitem[Honsell et  al 2002]{honsell}{F. Honsell, M. Miculan, I. Scagnetto, 
The Theory of Contexts for First Order and Higher Orden Abstract Syntax.}
{\it Elsevier Science B.V. } (2002)



\bibitem[Pfenning et al 1996]{pfenning}{J. Despeyroux, F. Pfenning,
C. Sch\"urmann, Primitive Recursion for Higher--Order Abstract Syntax.}
{\it Technical Report CMU--CS--96--172. Carnegie Mellon University } (1996)


\bibitem[Miculan 1999]{miculan}{M. Miculan, On the Formalization of the modal
$\mu$--calculus in the Calculus of Inductive Constructions.}
{\it Proceedings of ICALP'99 }(1999)

\bibitem[Miculan el at 2003]{miculan2}{M. Miculan, I. Scagnetto, A Framework for
Types HOAS and Semantics. } {\it Proceedings of PPDP'03 }(2003)

\bibitem[Simpson 2001]{simpson}{S. G. Simpson, Reverse Mathematics: an
Overview. } {\it Proceedings of the Association for Symbolic Logic  }(2001)


\bibitem[Tremblay 2002]{tremblay}{G. Tremblay, An introduction to model checking.}
{\it Technical Report. University of Alberta }(2002)

\bibitem[Walukiewicz 1995]{igor}{I. Walukiewicz, Notes on the Propositional
$\mu$--calculus: Completeness and Related Results.}
{\it Technical Report. University of Aarhus }(1995)

\end{thebibliography}
\end{document}
