Diferencia entre revisiones de «Tipo de dato algebraico»
Contenido eliminado Contenido añadido
Deshecha la edición 30695444 de 190.21.204.27 (disc.)Revirtiendo vandalismo |
|||
Línea 36:
| niveles Nodo(i,n,d) = 1 + max (niveles i) (niveles d)
</code>
== Corrección de programas ==
A cada tipo de datos algebraico corresponde el [[orden bien fundamentado]] de subtérminos y un esquema de [[inducción estructural]] sobre la base de la definición del tipo. En el caso de los árboles éstos son los siguientes:
<center>
<math> t_1 < Nodo(t_1,n,t_2)~~~ ~~~t_2 < Nodo(t_1,n,
<math>\frac{P(AVacio) \wedge (\forall i,n,d:i,d\in Arbol(T): P(i) \wedge P(d) \Rightarrow P(Nodo(i,n,d)))}{(\forall x:x\in Arbol(T):P(x))}</math>
Línea 49 ⟶ 50:
La llamada por patrones es una operación compleja que puede definirse con ayuda de dos primitivas, El operador ''is'' permite identificar el caso particular de una definición y la definición estructurada de variables permite obtener los componentes de un caso ya identificado:
En el ejemplo de árboles, el predicado ''e is AVacio'' es cierto cuando el árbol ''e'' es efectivamente un árbol vacío y ''e is Nodo'' es cierto cuando ''e'' es un nodo. Una definición del tipo ''let Nodo (
== Enlaces externos ==
| |||