Tipus de dades algebraic

En matemàtiques discretes és usual introduir definicions d'estructures recursives donant els casos de definició i un axioma de clausura indicant que cap altra cosa forma part del definit.

Per exemple, els arbres amb informació en els nodes poden definir-se com segueix: Siga T un conjunt. Els arbres amb informació en els nodes són tots els valors que es poden construir amb les regles següents.

L'arbre buit és un arbre i és representat amb la constant ABuit.
Si $t_{1}$ i $t_{2}$ són arbres, i x és un element de T, llavors Node( $t_{1}$ ,x, $t_{2}$ ) és un arbre.

Els arbres són únicament els valors que es construeixen utilitzant les regles 1 i 2.

La construcció corresponent en els llenguatges de programació es diu Tipus de dades algebraic. Les seues regles de tipus polimòrfiques van ser introduïdes per Robin Milner juntament amb la definició del llenguatge Standard ML i han estat adoptades des de llavors en diversos llenguatges de programació, sobretot en els llenguatges de programació funcionals. Per exemple, la definició del tipus arbre binari amb informació en els nodes de tipus T s'escriu en Ocaml com seguix:

 type 'T Arbol = AVacio | Nodo of ('T Arbol * 'T * 'T Arbol)

i en sintaxi d'Haskell:

 data Arbol T = AVacio | Nodo (Arbol T) T (Arbol T)

Els constructors del tipus Arbre són ABuit i Node els quals, al rebre els arguments necessaris produeixen un valor del tipus arbre. Per exemple, en Ocaml, ABuit és un arbre igual que Node (ABuit,5,ABuit).

Les operacions sobre els tipus recursius generalment s'escriuen utilitzant la construcció de cridada per patrons. Per exemple, en Haskell, el nombre de nivells d'un arbre de defineix com:

 nivells :: Arbre T -> Int
 nivells AVacio = 0
 nivells (Nodo i n d) = 1 + max (nivells i) (nivells d)

en Standard ML la mateixa funció s'escriu

 fun nivells AVacio = 0
 | nivells Nodo(i,n,d) = 1 + max (nivells i) (nivells d)

Correcció de programes

A cada tipus de dades algebraic correspon l'ordre ben fonamentat de subtermes i un esquema d'inducció estructural sobre la base de la definició del tipus. En el cas dels arbres aquests són els següents:

$t_{1}<Nodo(t_{1},n,t_{2})~~~~~~t_{2}<Nodo(t_{1},n,t_{2})$

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

Per a demostrar la terminació de la funció anivelles aplicant aquest esquema d'inducció

estructural, s'ha de demostrar, utilitzant les regles semàntiques del llenguatge, que l'expressió (nivells ABuit) acaba i que si (nivells i) i (nivells d) acaben llavors (nivells (Node (i, n, d)) acaba també.

L'operació anomenada per patrons és una operació complexa que pot definir-se amb ajuda de dues primitives, L'operador *is permet identificar el cas particular d'una definició i la definició estructurada de variables permet obtenir els components d'un cas ja identificat:

En l'exemple d'arbres, el predicat i is ABuit és cert quan l'arbre i és efectivament un arbre buit i i is Node és cert quan i és un node. Una definició del tipus let Node (o, x, v) = i ..., que només té sentit quan i is Node és cert, permet associar a les variables o, x, v els components del node.

Enllaços externs

FOLDOC (Algebraic data type) Arxivat 2005-04-14 a Wayback Machine.