Sustitución de variables

En esta práctica vamos a construir un par de predicados en Prolog para realizar la sustitución de variables libres por términos en fórmulas de Lógica de Primer Orden de cualquier tipo.

Para representar una fórmula lógica, definiremos los siguientes operadores en Prolog:

:- op(1060, yfx, <->). % doble implicación :- op(1050, yfx, <-). % implicación hacia la izquierda :- op(600, yfx, v). % disyunción :- op(400, yfx, &). % conjunción :- op(200, fx, forall). % universal :- op(200, fx, exists). % existencial :- op(300, xfy, ::). % separador para cuantificadores

Además, permitiremos los operadores '-' y '->' para representar la negación ¬ y la implicación →, respectivamente. Esos dos operadores ya están predefinidos en Prolog, del siguiente modo:

?- current_op(P,T,-).
P = 200,
T = fy .

?- current_op(P,T,->).
P = 1050,
T = xfy.

El operador :: se usará para construir fórmulas cuantificadas de la siguiente manera: forall x :: formula o bien exists x :: formula. Por ejemplo, la siguiente fórmula en cálculo de predicados:

∀x (P(x) → ∃y (¬Q(x,y) ∧ R(y)) )

sería representada como el término Prolog

forall x :: ( p(x) -> exists y :: (-q(x,y) & r(y) ) )

Nótese que, en una fórmula concreta de Lógica de Primer Orden, no usaremos mayúsculas. Los nombres con mayúsculas los reservamos para variables en Prolog.

Predicados que hay que definir

El programa Prolog deberá contener la definición de los predicados subs/3 y subs_list/3 que definimos a continuación

1. Predicado subs(X/T, F ,G)

Realizará la sustitución de toda aparición libre de la variable X reemplazándola por el término T en la fórmula de entrada F devolviendo como resultado la fórmula G. Estos son algunos ejemplos de consultas con ese predicado:

?- subs(x/4, p(f(x),y), G).
G = p(f(4), y).

?- subs(x/f(a), exists y :: q(y,x) & forall x :: p(x), G).
G = exists y::q(y, f(a))&forall x::p(x).

Por simplicidad, supondremos que la fórmula que nos pasan está bien construida (no es necesario comprobarlo). Por ejemplo, no necesitamos comprobar que nos pasen expresiones mal construidas como subs(x/4, 3 :: [x]+5 , G) donde está claro que la expresión "3 :: [x]+5" no es una fórmula bien formada, a pesar de ser un término Prolog.

También supondremos que el término T no contiene ninguna variable ya cuantificada en la fórmula F. De lo contrario, algunas sustituciones serían incorrectas. Por ejemplo, esta sustitución:

?- subs(x/y, q(x) & exists y :: p(x,y), G).
G = q(y)&exists y::p(y, y).

es incorrecta en lógica, porque la variable y que introducimos de primer parámetro del predicado p debería quedar libre, y no ligada al cuantificador exists, como ocurre en el resultado arriba mostrado.

Ejercicio opcional: reforzar el predicado subs/2 para que compruebe estas situaciones, de modo que si tenemos cualquier identificador atómico a en T que luego aparezca nombrado como una variable cuantificada en F, el predicado devuelve false y muestre un mensaje:

?- subs(x/y, q(x) & exists y :: p(x,y), G).
Error: no se puede cambiar x/y porque y está cuantificada en exists y :: p(x,y)
false

2. Predicado subs_list(L, F ,G)

Realizará la secuencia de sustituciones X/T contenidas en la lista L de forma acumulada, una tras otra, sobre la fórmula F para devolver la fórmula final G. Cada sustitución realizará una llamada al predicado subs/3 del paso anterior. Ejemplo de consulta:

?- subs_list([x/f(y), y/g(z), z/0], exists w :: (p(w,y) & -q(h(x),w)), G  ).
G = exists w::(p(w, g(0))& -q(h(f(g(0))), w)).

Entrega y evaluación