Introdução

Unificação é um processo utilizado em lógica que consiste em atribuir valores para variáveis de diferentes expressões para testar se uma expressão pode ser substituída em outra. Isto é, se existe uma substituição atuando em um conjunto finito de termos tal que , onde é um conjunto unitário.

Em uma expressão unificável $P$ existe duas expressões e , tal que exista e que possuam equivalência. Por exemplo, para unificarmos as expressões e , precisamos de e . Desta maneira, ambos termos são , sendo esta última expressão a forma mais reduzida, uma vez que impossível de se unificar e .

Para verificar se uma expressão é unificável, nosso programa verifica a relação de tipos entre sub-expressões, obedecendo as seguintes definições:

  1. Termos são expressões construídas a partir de constantes, variáveis e símbolos funcionais de aridade finita:
<center>
  <tt>$$t ::= c~|~x~|~f(t_1, t_2, \ldots,t_n) $$</tt>
</center>
  1. Uma substituição é um conjunto , onde cada variável é distinta das outras e cada é um termo distinto de . Chamamos de ligação da substituição .
  2. Para dois conjuntos distintos de substituições
<center>
  $$\theta = \{u_1/s_1, \ldots, u_m/s_m\} $$
</center>


  
e
      
<center>
  $$\sigma = \{v_1/t_1, \ldots, v_n/t_n\} $$
</center>


  
uma composição $$\theta\sigma $$ é a substituição obtida do conjunto $$\{u\_1/s\_1\sigma, \ldots, u\_m/s\_m\sigma, v\_1/t\_1, \ldots, v\_n/t\_n\} $$ eliminando qualquer ligação $$u\_i/s\_i\sigma $$ , para qual $$u\_i = s\_i\sigma $$ e qualquer ligação $$v\_j/t\_j $$ para qual $$v\_j \in \{u\_1, \ldots, u_m\} $$ .    4. Seja $$S $$ um conjunto finito de termos. Uma substituição $$\theta $$ é denominada um unificador de $$S $$ se $$S\theta $$ for um **conjunto unitário**.    5. Um unificador $$\theta $$ para um conjunto finito $$S $$ de termos é denominado um **unificador mais geral** de $$S $$ se $$\forall $$ unificador de $$\sigma $$ de $$S $$ $$\exists $$ uma substituição $$\gamma $$ tal que $$\sigma = \theta\gamma $$ .    6. Seja $$S $$ um conjunto finito de termos. O conjunto de conflitos de $$S $$ consiste dos sub-termos mais a esquerda dos termos de $$S $$ que se diferenciam.

 

Algoritmo

A existência das definições anteriores são verificadas pelo seguinte algoritmo:

Inicio

Enquanto repita:

Seja o conjunto de conflitos de

Se com variavel, termos sem ocorrencias de Entao

Senão

reporte que não unificável e saia

retorna , o unificador de

Fim

 

Implementação

Os tipos

Para representarmos uma expressão qualquer, precisamos definir um tipo abstrato. No nosso programa, definimos três tipos:

type id    = string;;
type term' = Var' of id | Term' of term' * term';;
type term  = Var of id | Term of id * term list;;

onde

  • é o tipo fundamental da menor sub-expressão possível. Este tipo pode ser visto como valores de variáveis.
  • é o tipo que representa uma expressão. No caso, este expressão pode ser uma variável</p>
    • é associado com valores do tipo “id”, ou então uma sub-expressão composta por dois sub-termos deste tipo.
  • é um tipo que foi definido apenas para receber uma entrada de expressões contendo a interface proposta para este trabalho.

Podemos notar que o tipo é definido recursivamente e gerará uma árvore binária com nós não-marcados. Isso serve para o programa armazenar nas folhas os termos mais simples, que serão as variáveis. Desta maneira, podemos comparar em cada sub-árvore as regras necessárias para haver unificação.

 

As exceções

Nosso programa prevê dois possíveis erros durante a execução:

  • Erro na unificação: Quando avalia uma sub-expressão e ela não obedece aos requisitos para unificação.
  • Erro de conformidade: Quando uma expressão de entrada é mal-formada. Ou seja, ela não corresponde à uma expressão avaliável.

Tais exceções são definidas em Ocaml como:

exception UnificationError of string;;
exception MatchError of string;;

</p>

 

Conversão de tipos

Para este trabalho, foi proposto que a entrada de uma expressão deveria ser composta de um termo composto por uma string e uma lista formada por uma variável e um sub-termo com a mesma definição. Por exemplo:


$$Term(“f”, [Var “x”; Term(“g”, [Var “y”])])$$

Embora esta notação seja simples, ela não pode ser utilizada diretamente em nossa implementação, uma vez que a abordagem escolhida para avaliação consiste em comparar sub-expressões de tipo iguais. Sendo assim, a expressão válida para as funções do nosso programa precisariam ser escritas da forma


$$Term'(Var’ “f”, Term'(Var’ “x”, Term'(Var’ “g”, Term'(Var’ “y”))))$$

que é menos conveniente para leitura do ser humano.

Sendo assim, segue abaixo a função que faz a conversão da primeira forma para a segunda:

let rec conv v =
  match v with
    | Var x               -> Var' x
    | Term(x, [])         -> Var' x
    | Term(a, [Var b])    -> Term'(Var' a, Var' b)
    | Term(a, [Var h; t]) -> Term'(Var' a, Term'(Var' h, conv t))
    | _                   -> raise (MatchError "bad format expression");;

Nesta função podemos notar que o tipo básico de ambos os casos (variáveis) possuem equivalência em qualquer uma das formas.

Além disso, as constantes — denotadas por — são tratadas como variáveis pelas funções relacionadas à unificação.

Os demais termos são definidos e convertidos recursivamente ou geram um erro se forem expressões mal-formadas.

 

Busca de ocorrências

Antes de reavaliar uma unificação de sub-termos, nosso programa verifica se ocorre situações de conflitos entre elas. O primeiro destes conflitos ocorre quando termos uma expressão e outra expressão . A substituição não é unificável por gerar um conflito conhecido como dependência cíclica ou circularidade.

Assim, para uma variável e uma expressão qualquer , o programa busca se esta variável ocorre em alguma sub-expressão de através da seguinte função:

let rec occurrences a v =
  match v with
    | Var' b -> (Var' b = Var' a)
    | Term'(f, subexpr) -> (occurrences a f) || (occurrences a subexpr);;

A expressão é sempre formada por uma variável ou por composições de — e . Assim, a chamada recursiva presente na última linha garante que todos sub-termos da expressão original serão verificados. Ainda nessa linha, observamos que a operação lógica ou retornará verdadeiro se houver ao menos uma ocorrência da variável testada. Assim, a função retorna verdadeiro sempre que houver uma condição de dependência circular nas expressões unificadas.

 

Substituição

A função de substituição procura a ocorrência de um termo na expressão e troca este termo por outro. Como o unificador só existe se houver uma substituição que transforme o conjunto de termos, esta função é fundamental para o funcionamento do programa.

A substituição é implementada de forma a procurar a ocorrência da variável em uma sub-expressão . Para isso, utilizamos a função , que retorna o valor associado à chave em uma lista associativa. Caso não haja ocorrência desta variável na expressão, ela é retornada pela função. Tal função é apresentada abaixo:

let rec substitute tm1 tm2 =
  match tm2 with
    | (Var' a) as alpha -> (try List.assoc a tm1 with Not_found -> alpha)
    | Term'(t1, t2)     -> Term'(substitute tm1 t1, substitute tm1 t2);;

O comportamento explicado anteriormente é repetido recursivamente, substituindo-se os termos mais simples nas expressões compostas, como observamos pela última linha.

 

Acoplamento

A primeira parte do algoritmo de unificação é implementada na função chamada . Este função recebe uma dupla de expressões e faz os seguintes testes:

  1. Verifica se duas expressões são idênticas. Caso sejam, retorna uma lista vazia, uma vez que não há unificação de uma expressão por ela mesmo.
  2. Verifica ocorrências de uma variável em uma expressão . Se este caso aparece, então ocorre circularidade e não ocorre unificação (primeiro ).
  3. Se os casos acima não ocorrerem, então ambas expressões são formadas por termos compostos por mais de uma simples variável. Para esta situação, a função tenta substituir a primeira na segunda e fazer as verificações anteriores recursivamente.

Segue a implementação dos passos descritos:

let rec coupling expr =
  match expr with
    | (exp1, exp2) when exp1 = exp2 -> []
    | (Var' a, exp) -> 
        if occurrences a exp then
          raise (UnificationError "not unifiable: circularity")
        else
          [a, exp]
    | (exp, Var' a) -> coupling (Var' a, exp)
    | (Term'(s1 ,s2), Term'(t1 ,t2)) ->
        let s = coupling (s1 ,t1) in
        let m1 = coupling (substitute s s2 , substitute s t2) in
        let tail_subs (a, exp) = (a, substitute m1 exp) in
          List.append (List.map tail_subs s) m1;;

 

Unificação

A função consiste apenas em:

  1. receber duas expressões distintas e ,
  2. convertê-las para o formato utilizado pelas outras funções,
  3. verificar o resultado do acoplamento entre elas,
  4. e decidir se há uma substituição possível de uma expressão em outra. Caso isso não ocorra, então a unificação não é possível (segundo ).

Esta função é implementada como

let unif e1 e2 =
  let exp1 = conv e1 and
      exp2 = conv e2 in
  let l = coupling (exp1, exp2) in
    match l with
      | [(c, Var' y)] -> [(c, Var' y)] 
      | _ -> raise (UnificationError "not unifiable: head symbol conflict");;

 

Resultados

A implementação foi testada para os três casos: duas expressões válidas e unificáveis, para o caso trivial de circularidade e para duas expressões não unificáveis.

Para funções unificáveis:

`# unif (Term(“f”,[Var “x”; Term(“g”,[Var “y”])]))
(Term(“f”,[Var “x”; Term(“g”,[Var “x”])]));;

  • : (id * term’) list = [(“y”, Var’ “x”)]
    `

Para funções não-unificáveis:

`# unif (Term(“f”,[Var “x”; Term(“g”,[Var “y”])]))
(Term(“f”,[Var “x”; Term(“f”,[Var “x”])]));;</p>

Exception: UnificationError "not unifiable: head symbol conflict".` Para condições de circularidade: > `# unif (Var "x") (Term("f", [Var "x"]));;

Exception: UnificationError "not unifiable: circularity".`   ## Conclusão Esta implementação utiliza uma abordagem elegante e eficiente, consistindo em um conjunto pequeno de funções para abranger todos os casos possíveis do algoritmo de Robson. Como trabalho futuro, podemos modificá-la para utilizar apenas uma estrutura de dados na representação dos termos. Se fizermos isto sem aumentar o tamanho das funções, podemos ter um código ainda mais conciso e eficiente.   ## Código Completo 

(*
 * Another unification algorithm.
 *
 * Author: Pedro Garcia Freitas [sawp@sawp.com.br]
 *         http://www.sawp.com.br
 *
 *)

(*
 * Exception
 *)
exception UnificationError of string;;
exception ListError of string;;
exception MatchError of string;;

(*
 * Abstract types
 *)
type id = string;;
type term' = Var' of id | Term' of term' * term';;
type term = Var of id | Term of id * term list;;

(*
 * Perform Substitution
 *)

let rec substitute tm1 tm2 =
  match tm2 with
    | (Var' a) as alpha -> (try List.assoc a tm1 with Not_found -> alpha)
    | Term'(t1 ,t2) -> Term'(substitute tm1 t1, substitute tm1 t2);;

(*
 * Check Occurrences of a variable in a expression
 *)
let rec occurrences a v =
  match v with
    | Var' b -> (Var' b = Var' a)
    | Term'(f, subexpr) -> (occurrences a f) || (occurrences a subexpr);;

(*
 * Convert the term to term'
 *)
let rec conv v =
  match v with
    | Var x               -> Var' x
    | Term(x, [])         -> Var' x
    | Term(a,[Var b])     -> Term'(Var' a, Var' b)
    | Term(a, [Var h; t]) -> Term'(Var' a, Term'(Var' h, conv t))
    | _                   -> raise (MatchError "bad format expression");;

(*
 * Verify coupling variables and sub-expression from one to another
 *)
let rec coupling expr =
  match expr with
    | (exp1, exp2) when exp1 = exp2 -> []
    | (Var' a, exp) -> 
        if occurrences a exp then
          raise (UnificationError "not unifiable: circularity")
        else
          [a, exp]
    | (exp, Var' a) -> coupling (Var' a, exp)
    | (Term'(s1 ,s2), Term'(t1 ,t2)) ->
        let s = coupling(s1 ,t1) in
        let m1 = coupling(substitute s s2 , substitute s t2) in
        let tail_subs (a,exp) = (a,substitute m1 exp) in
          List.append (List.map tail_subs s) m1;;

(*
 * Unify using coupling
 *)
let unif e1 e2 =
  let exp1 = conv e1 and
      exp2 = conv e2 in
  let l = coupling (exp1, exp2) in
    match l with
      | [(c, Var' y)] -> [(c, Var' y)] 
      | _ -> raise (UnificationError "not unifiable: head symbol conflict");;
Disponível em http://sawp.com.br/code/general/unif.ml

Referências