La relación de subsunción

La letra a en el nombre está relacionada con la regla a del lambda cálculo ya que en esta regla también realizábamos un renombramiento de variables.

El conjunto cociente de a-equivalencias

A partir de ahora es fácil definir

[$$ M < N \Leftrightarrow M \le N \wedge M \not\approx N $$]

Y las relaciones simétricas >, =, etc.

Como la a-congruencia es una relación de equivalencia, notaremos [M] por la clase de equivalencia del término M (o clase de congruencia ya que estamos trabajando con congruencias).

Realmente el conjunto cociente T(A,V)/≈ agrupa en una misma clase los términos que son iguales excepto renombramientos de variables.

[$$ \left[ f(x) \right] = \left\{ f(x), f(y), f(z), ...\right\} $$]
[$$ \left[ g(h(1,z),y) \right] = \left\{ g(h(1,x),y), g(h(1,y),x), g(h(1,x),z), ...\right\} $$]

Es importante recordar que un renombramiento de variables no puede fusionar variables y por lo tanto el término g(h(1,x),x) no pertenece a la clase de equivalencia anterior. Esto es así porque no existe ninguna sustitución que pueda obtener el término original g(h(1,z),y) y por tanto no sería a-congruente.

La subsunción inducida

Si ignoramos los renombramientos de variables, la subsunción se convierte en un orden parcial. Esto es obvio ya que la antisimetría nos lleva directamente a la definición de a-congruencia y, dado que estamos trabajando en el conjunto cociente de esta relación, ambas clases de equivalencia van a ser la misma.

Formalmente esto lo haríamos extendiendo la subsunción al conjunto cociente obtenido por a-conversión. Esta nueva relación se denomina subsunción inducida en el conjunto cociente.

[$$ \left( \le, T(A,V)/\approx \right) $$]

Usaremos el mismo símbolo = para ambas relaciones ya que usualmente trabajaremos con la inducida en el conjunto cociente.

Es realmente importante ver que, dado que los términos son finitos, la subsunción inducida es Noetheriana. Es decir, no existe una cadena infinita

[$$ M_1 > M_2 > \cdots $$]

Esto significa que la subsunción inducida forma una semiretículo inferior Noetheriano y, por ciertos teoremas, debe ser también un semiretículo superior y un retículo completo.

El menor elemento del retículo es [x] ya que lo podemos sustituir por cualquier otro elemento y el superior es [O] que no puede ser sustituido más que por él mismo. Esta era una de las razones por las que nos interesaba introducir un elemento indefinido.

Supremo e ínfimo

Siempre que hablamos de retículos podemos aproximarnos a ellos desde dos perspectivas. Desde una relación de orden y desde las operaciones constituyentes de supremo e ínfimo (con las propiedades asociativa, conmutativa y absorción).

En el caso del retículo de la subsunción inducida el supremo (lo notaremos como una unión de conjuntos) es una unificación con variables disjuntas.

[$$ f(x,g(y)) \cup f(g(y), z) = f(g(w), g(v)) $$]

Probablemente explique algo de unificación más adelante. La idea de la unificación es buscar una sustitución que, aplicada a ambos términos, nos proporcione un mismo término final. En el caso especial de usar variables disjuntas, antes de realizar esta unificación hay que renombrar las variables para que sean todas distintas unas a otras.

El ínfimo (que notaremos como la intersección) es la antiunificación.

[$$ f(x,g(y)) \cap f(g(y),z) = f(x,y) $$]

Lo interesante de todas estas ideas es que, a partir de una definición muy simple de términos y sustituciones, obtenemos una estructura algebraica con unas propiedades bastante bien estudiadas como son los retículos completos.