For faster navigation, this Iframe is preloading the Wikiwand page for Tipus de dades algebraic.

Tipus de dades algebraic

De Viquipèdia

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.

  1. L'arbre buit és un arbre i és representat amb la constant ABuit.
  2. Si i són arbres, i x és un element de T, llavors Node(,x,) és un arbre.
  1. 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:

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

{{bottomLinkPreText}} {{bottomLinkText}}
Tipus de dades algebraic
Listen to this article

This browser is not supported by Wikiwand :(
Wikiwand requires a browser with modern capabilities in order to provide you with the best reading experience.
Please download and use one of the following browsers:

This article was just edited, click to reload
This article has been deleted on Wikipedia (Why?)

Back to homepage

Please click Add in the dialog above
Please click Allow in the top-left corner,
then click Install Now in the dialog
Please click Open in the download dialog,
then click Install
Please click the "Downloads" icon in the Safari toolbar, open the first download in the list,
then click Install
{{::$root.activation.text}}

Install Wikiwand

Install on Chrome Install on Firefox
Don't forget to rate us

Tell your friends about Wikiwand!

Gmail Facebook Twitter Link

Enjoying Wikiwand?

Tell your friends and spread the love:
Share on Gmail Share on Facebook Share on Twitter Share on Buffer

Our magic isn't perfect

You can help our automatic cover photo selection by reporting an unsuitable photo.

This photo is visually disturbing This photo is not a good choice

Thank you for helping!


Your input will affect cover photo selection, along with input from other users.