Un algorithme d'unification entre types
Une substitution s'écrit [
a
1
:
t
1
,...,
a
n
:
t
n
]. Connaissant la substitution
S
1
, l'unification de
t
1
et
t
2
produit la nouvelle substitution
S
2
. On le note:
S
1
|-
t
1
º
t
2
:
S
2
Avec les règles:
S
|-
t
º
t
:
S
S
|-
t
1
º
t
'
1
:
S
1
S
1
|-
t
2
º
t
'
2
:
S
2
S
|-
t
1
®
t
2
º
t
'
1
®
t
'
2
:
S
2
S
|-
t
1
º
t
'
1
:
S
1
S
1
|-
t
2
º
t
'
2
:
S
2
S
|-
t
1
*
t
2
º
t
'
1
*
t
'
2
:
S
2
S
|-
t
1
º
t
2
:
S
2
S
(
a
) =
t
1
S
|-
a
º
t
2
:
S
2
a
Ï
Dom
(
S
)
a
Ï
Vars
(
S
(
t
))
S
|-
a
º
t
:
S
[
a
:
S
(
t
)]
