´n Departamento de Computacio Facultad de Ciencias Exactas y Naturales Universidad de Buenos Aires

Tesis de Licenciatura en Ciencias de la Computaci´on λσgc: Un c´alculo basado en λσ con Garbage Collection

Luis Francisco Ziliani - [email protected] - L.U. 356/01 Director: Alejandro R´ıos Julio de 2009

Resumen Desde hace unos 20 a˜ nos que distintos c´alculos de sustituciones expl´ıcitas han dado diferentes resultados en la forma de imitar al λ-c´alculo. Uno de los primeros, λσ, ha sido inspiraci´ on para muchos de ellos por su forma de componer sustituciones y por su forma de trabajar los ´ındices de de Bruijn. Sin embargo, ning´ un c´ alculo derivado de ´este logra combinar satisfactoriamente todas las buenas propiedades que se esperan de un c´alculo de sustituciones expl´ıcitas: preservaci´ on de la normalizaci´on fuerte (PSN), simulaci´on del λ-c´alculo (Sim), metaconfluencia (MC), etc. En un reciente trabajo de D. Kesner se presenta un c´alculo derivado de λx que tiene todas estas propiedades. Parte fundamental de este c´alculo es la eliminaci´ on de “basura” -sustituciones que no modifican el t´ermino a sustituir, que al componerse con otras sustituciones terminan generando m´as basura, resultando en t´erminos con derivaciones infinitas que en el λ-c´alculo tradicional son fuertemente normalizantes. En este trabajo presentamos λσgc , un c´alculo basado en λσ, que resulta de agregar una regla que elimina sustituciones “basura”, y evita la composici´on y distribuci´ on de esta basura. Demostramos que este nuevo c´alculo presenta las mismas propiedades que λσ. Adem´as, demostramos que λσgc consigue incluir al t´ermino de M`ellies en el conjunto de t´erminos fuertemente normalizantes, aunque PSN para este c´ alculo sigue siendo una pregunta abierta. En el estudio de algunas propiedades del nuevo c´alculo hemos desarrollado herramientas l´ ogicas originales, que pueden servir a futuras extensiones de λσ, y hemos abierto y desarrollado la discusi´on sobre c´omo evitar la basura en c´alculos derivados de dicho c´ alculo.

Abstract For the last 20 years different calculi with explicit substitutions have been developed in order to imitate the λ-calculus, with diverse results. One of them, λσ, has been an inspiration to many of them, because of the way it composes substitutions, and the way it handles de Bruijn indices. However, no calculus derived from it is known to achieve all the good properties expected from a calculus with explicit substitutions: preservation of strong normalization (PSN), simulation of λ-calculus (Sim), metaconfluence (MC), etc. In a recent work, D. Kesner presents a new calculus obtained from λx with all these properties. To achieve this result, it does “garbage collection” -throw away substitutions that are not going to modify the term to substitute, whose composition with other substitutions ends up in the generation of more garbage, creating infinite derivations in terms which are strongly normalizing in traditional λ-calculus. In this work we present λσgc , a calculus based on λσ that performs garbage collection, avoids the distribution of garbage through the terms, and does not allow for the composition of garbage. We prove that this new calculus has the same properties as λσ. Moreover, we prove that λσgc includes the M`ellies term in the set of strongly normalizing terms. But PSN for this calculus remains an open question. In the study of some of the properties of the new calculus, we have developed some original logic tools. Future extensions of λσ can benefit from these ideas. Also, we have opened and advanced the discussion about how garbage can be avoided in calculi derived form λσ.

A Maril´ı y Rody, mis padres.

Agradecimientos Esta tesis es el producto de una serie infinita de eventos, en los que participaron diversas personas, muchas de las cuales no me conocen ni las conozco. Como nombrar a todas es una tarea imposible, voy a robar una frase que un compa˜ nero de militancia, Guido de Caso, puso en su tesis: agradezco a todos los que, desde su fundaci´ on, lucharon por una universidad p´ ublica, gratuita, aut´ onoma y laica. En concreto, en orden m´ as o menos cronol´ogico: A mis padres, a quienes dedico este trabajo, mi reconocimiento a todo el saber que nunca dejaron de transmitirnos a m´ı y a mis hermanos, sin el cual posiblemente no podr´ıa estar presentando este trabajo. A Ceci, mi novia, le debo nada menos que mi cambio de carrera, junto con la infinita paciencia que me tuvo ante cada instancia de presentaci´on de trabajos, elecciones de centro de estudiantes, etc. Adem´as, todas sus ense˜ nanzas, ya sean acad´emicas, polt´ıcias, o cotidianas. A ella, todo mi amor. A mis compa˜ neros de cursada, Alexis, Edu, Elvis, Gast´on, gracias por el rock! A mis compa˜ neros de La Mella, les debo lo que lamentablemente no se ense˜ na en las aulas, pero se vive en toda intereacci´on humana: la pol´ıtica. A todos y cada uno de ellos, un abrazo lleno de esperanza. A Alejandro R´ıos, le agradezco su gu´ıa paciente y sabia. A Nicol´ as di Tada, Director de Manas Technology Solutions, la empresa de la que formo parte desde hace casi 5 a˜ nos, un profundo agradecimiento por haber sido sponsor de este trabajo. Espero que este ejemplo de ayudar a la investigaci´ on universitaria sin condicionarla sea imitado por quienes intentan llevar “agua para su molino”, consumiendo los recursos del estado, es decir, del pueblo. Finalmente, y pido disculpas si ofendo a alguien, a la estampita de Sai Baba, c´ abala oficial de toda mi carrera.

´Indice general Introducci´ on

1

1 Presentaci´ on de formalismos 1.1 Introducci´ on a la teor´ıa de la reescritura . . . . . . . . . . . . 1.1.1 Sistemas de Reducci´on Abstractos (ARS) . . . . . . . 1.1.2 Sistemas de Reescritura de T´erminos (TRS) . . . . . . 1.2 C´ alculo λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.1 λ-c´ alculo simplemente tipado . . . . . . . . . . . . . . 1.3 C´ alculo λDB . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 C´ alculo λσ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4.1 C´ alculo λσ simplemente tipado . . . . . . . . . . . . . 1.4.2 Propiedades de los c´alculos de sustituciones expl´ıcitas 1.4.3 Definiciones . . . . . . . . . . . . . . . . . . . . . . . . 1.5 C´ alculo λx . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.6 C´ alculo λes . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . .

. . . . . . . . . . . .

3 3 3 6 9 10 11 12 13 15 16 19 19

2 C´ alculo λσgc 21 2.1 Afectar o no afectar un t´ermino . . . . . . . . . . . . . . . . . . . 21 2.2 Relaci´ on entre GC y λσ . . . . . . . . . . . . . . . . . . . . . . . 23 2.3 C´ alculo λσgc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3 Normalizaci´ on fuerte de σgc 3.1 Presentaci´ on de σgc0 . . . . . . 3.2 SN de σgc0 implica SN de σgc . 3.3 Presentaci´ on del c´ alculo AMAs 3.4 AMAs es SN . . . . . . . . . . 4 Lemas u ´ tiles

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

29 30 30 33 33 37

5 Confluencia de σgc 61 5.1 Confluencia local de σgc . . . . . . . . . . . . . . . . . . . . . . . 61 5.2 Confluencia de σgc . . . . . . . . . . . . . . . . . . . . . . . . . . 75 6 Confluencia de λσgc 79 6.1 Simulaci´ on . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 6.2 Correcci´ on y confluencia de λσgc . . . . . . . . . . . . . . . . . . 84 7 El c´ alculo λσgc tipado

93

i

8 λσgc y PSN 97 8.1 λσgc resuelve el contraejemplo de Melli`es . . . . . . . . . . . . . . 97 8.2

?

?

Problema abierto: SN λσ ⊂ SN λσgc ⊃ SN λ . . . . . . . . . . . .

9 Conclusiones 9.1 Generalizaci´ on de lemas a λσ . . 9.2 Confluencia en t´erminos puros . . 9.3 Acercamiento a λes . . . . . . . . 9.4 λsgc : Garbage collection para λs

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

98 101 101 101 102 102

A Demostraciones para λσ

103

B Programa int´ erprete de λσ en Prolog

107

C Programa int´ erprete de λσgc en Java

109

ii

Introducci´ on La implementaci´ on del λ-c´alculo ha presentado varios desaf´ıos desde sus primeros intentos, ya sea en el estudio y creaci´on de lenguajes funcionales, como en demostradores de teoremas. As´ı es como de Bruijn concibe en el a˜ no 1972 lo que actualmente se conoce como c´alculo con ´ındices de de Bruijn. La finalidad de este c´ alculo era eliminar los problemas de trabajar m´ odulo α-congruencia, definiendo un u ´nico t´ermino para cada clase de equivalencia. En el a˜ no 1990, Abadi et al. crean el c´alculo λσ, un c´ alculo de sustituciones expl´ıcitas (SE) basado en Categorical Combinatory Logic ([Cur94], [CC87], [Har92]). Estos c´ alculos internalizan la metaoperaci´on de sustituci´on como pasos at´ omicos propios del c´ alculo. Pero, como lo muestran Abadi et al., el c´alculo λσ no es metaconfluente (MC), es decir, confluente en los t´erminos con metavariables, propiedad necesaria para representar pruebas incompletas en demostradores de teoremas basados en tipos. Adem´as, en el a˜ no 1995 Melli`es muestra otro inconveniente en la teor´ıa de este c´alculo: no todo t´ermino fuertemente normalizante del λ-c´ alculo lo es en λσ. Esta propiedad, deseable en todo c´alculo con SE, es denominada preservaci´ on de la normalizaci´ on fuerte (PSN). Desde entonces, han proliferado distintos tipos de c´alculos de sustituciones expl´ıcitas en la b´ usqueda de uno que satisfaga MC, PSN, y adem´as simule la β-reducci´ on (Sim). Una extensi´ on de λσ estudiada por R´ıos en [Rio93], λσSP , consigue MC de t´erminos semiabiertos, es decir, con metavariables en los t´erminos y no en las sustituciones. Otra variante presentada por Curien et al. en [CHL96], el λσ⇑ , consigue MC y Sim, pero pierde PSN. Lescanne en [Les94] presenta λυ, variante que conserva PSN y Sim, pero no MC, y Mu˜ noz en [Mun96] consigue con λζ PSN y MC, pero no Sim. En el a˜ no 1995, Kamareddine y R´ıos presentan en [KR95] al c´alculo λs, que incluye dos familias de operadores para simular la sustituci´on y la actualizaci´on de de Bruijn. Si bien cumple PSN y Sim, no consigue MC. Dos a˜ nos m´as tarde (en [KR97]), los mismos autores lo extienden con el fin de lograr MC. Esta extensi´ on, denominada λse , consigue Sim y MC, pero no cumple PSN. La b´ usqueda de un c´ alculo que preservara MC, PSN, y Sim parec´ıa infructuosa, pero en el 2001, David y Guillaume presentan en [DG01] al c´alculo λws, que logra esas tres propiedades con una signatura infinita, marcada por labels. Hasta aqu´ı hemos mencionado todos c´alculos que utilizan ´ındices para referir a las variables. En el conjunto de c´alculos de SE y variables nombradas, λx ([Ros93]) fue el pionero, aunque no consigue MC. Kesner en [Kes07] presenta λes, un c´ alculo que posee MC, PSN, Sim, entre otras buenas propiedades. En el presente trabajo hemos tomado algunas ideas del c´alculo λes para llevarlas al terreno de los ´ındices de de Bruijn, modificando al c´alculo λσ res1

Introducci´on

tringiendo la composici´ on.

Plan En el cap´ıtulo 1 presentaremos las nociones b´asicas de la teor´ıa de la reescritura. Introduciremos el λ-c´ alculo en la versi´on tradicional y `a la de Bruijn. Luego, nos concentraremos en λσ, por ser la base del c´alculo presentado en el cap´ıtulo 2. Finalizaremos el cap´ıtulo con una breve presentaci´on de los c´alculos λx y λes, el segundo por ser inspirador del presente trabajo, el primero por ser antecesor de λes. Dedicaremos el cap´ıtulo 2 a definir el concepto de basura para el c´alculo λσ, concepto que nos permitir´ a definir una variante de λσ con garbage collection: λσgc . En el cap´ıtulo 3 demostraremos que vale la normalizaci´on fuerte para el c´ alculo asociado de sustituciones, σgc . Daremos una demostraci´on detallada utilizando la t´ecnica de Distribution elimination utilizada por Zantema para demostrar la misma propiedad para el c´alculo σ. A lo largo del cap´ıtulo 4 demostraremos varios lemas, con el fin de obtener un conjunto de herramientas te´oricas para los siguientes cap´ıtulos. En el cap´ıtulo 5 analizaremos todos los pares cr´ıticos de σgc para concluir su confluencia d´ebil, y luego su confluencia, necesaria para la demostraci´on de confluencia del c´ alculo λσgc del siguiente cap´ıtulo. Dedicaremos el cap´ıtulo 6 a demostrar la confluencia del c´alculo λσgc , para lo cual ser´ a necesario primero establecer que se cumplen dos propiedades: Simulaci´ on y Correcci´ on. Demostraremos estas propiedades extendiendo las pruebas realizadas por R´ıos para λσ. Finalmente, estableceremos la confluencia de λσgc utilizando el lema de interpretaci´on. Brevemente introduciremos en el cap´ıtulo 7 una versi´on tipada de λσgc , que se corresponder´ a con la versi´ on tipada de λσ. En el cap´ıtulo 8 mostraremos que el contraejemplo de M`ellies pertenece al conjunto de t´erminos fuertemente normalizantes de λσgc , y comenzaremos la discusi´ on acerca de la relaci´ on entre los t´erminos fuertemente normalizantes de los c´ alculos λ, λσ, y λσgc . Para terminar, presentaremos distintos problemas que consideramos interesantes para continuar este trabajo. Por u ´ltimo, en los anexos mostraremos int´erpretes para λσ y λσgc que ser´an utilizados en demostraciones que requieren un an´alisis exhaustivo de todas las posibles derivaciones de un t´ermino.

2

Cap´ıtulo 1

Presentaci´ on de formalismos En este cap´ıtulo se introducir´an algunos de los formalismos utilizados o referenciados en el presente trabajo. La secci´ on 1.1 estar´ a dedicada a presentar algunas definiciones y resultados de la teor´ıa de la reescritura, enfocada en las herramientas utilizadas en el estudio de las propiedades del c´alculo λσgc . En la secci´on 1.2 se presentar´a el c´ alculo que ha inspirado gran parte de los trabajos aqu´ı mencionados: el λ-c´alculo. Luego, en 1.2.1 se mostrar´ a una versi´on tipada del mismo, que ser´a u ´til para comprender las versiones tipadas de λσ y λσgc . En la secci´on 1.3 se explicar´a un refinamiento del λ-c´ alculo que evita la α-congruencia, λDB . En la secci´on 1.4 se detallar´ a una variante de λDB que explicita la sustituci´on y admite composici´on de sustituciones: el c´ alculo λσ, base del presente trabajo. En la secci´on 1.4.1 se describir´ a la versi´ on tipada de este c´alculo. Finalmente, en la secci´on 1.5 se retomar´ an los c´ alculos de sustituciones con variables nombradas para introducir λx, el c´ alculo base de λes (secci´on 1.6), que ha inspirado el presente trabajo.

1.1

Introducci´ on a la teor´ıa de la reescritura

Aqu´ı ser´ an presentados los elementos b´asicos de la teor´ıa de la reescritura. Dada la vastedad de este tema, nos centraremos estrictamente en lo requerido para la comprensi´ on del presente trabajo. Para una profundizaci´on en el tema, el lector puede encontrar mayor informaci´on en [BN98] y en [Ter03].

1.1.1

Sistemas de Reducci´ on Abstractos (ARS)

Sea A un conjunto y R una relaci´on binaria sobre A. Notaremos a →R b para (a, b) ∈ R. Llamaremos reducci´ on a esta relaci´on, y ARS al par (A, R). Adem´ as, notaremos +

• R+ o →R a la clausura transitiva de R. • R∗ o R a la clausura reflexiva transitiva de R.

3

1.1 Introducci´ on a la teor´ıa de la reescritura

Presentaci´on de formalismos

n

• a R b a la reducci´ on de a en n pasos a b, es decir, a →R a1 →R . . . →R an = b Tambi´en llamaremos derivaci´ on a una reducci´on (posiblemente infinita) a1 →R a2 →R . . . Un ejemplo sencillo de ARS puede ser (N, sobre los naturales, obtenemos que 0 es la u ´nica forma normal. A continuaci´ on presentaremos las definiciones relacionadas con este concepto. Definici´ on 3. Sea (A, R) un ARS, decimos que

4

1.1 Introducci´ on a la teor´ıa de la reescritura

Presentaci´on de formalismos

• a ∈ A es una R-forma normal (o R-f.n.) si (@b ∈ A) a →R b. • a ∈ A es una forma normal de b si es una R-f.n. y b R a. • R es d´ebilmente normalizante o WN (weakly normalizing) si todo elemento de A tiene al menos una forma normal. • R es fuertemente normalizante o SN (strongly normalizing), si no hay derivaciones infinitas. • SN R es el subconjunto de A cuyos elementos no tienen derivaciones infinitas en R. • a ∈ A es SN si a ∈ SN R . Lema 4. Si R es SN, entonces R es WN. Demostraci´ on. Si R no fuera WN, entonces existe un elemento a0 que no tiene forma normal, con lo que existe un elemento a1 tal que a0 →R a1 , pero nuevamente a1 no tiene forma normal, con lo que existe a2 tal que a1 →R a2 ... y as´ı se construye una derivaci´ on infinita, absurdo. Los siguientes lemas nos permiten relacionar los conceptos hasta aqu´ı mencionados: Lema 5 (Newman). Toda relaci´on R fuertemente normalizante y localmente confluente es confluente. Demostraci´ on. Ver [BN98], lema 2.7.2. Lema 6. Sea (A, R) un ARS, tal que R es SN y WCR, entonces todo elemento de A tiene una u ´nica forma normal. En este caso, notaremos R(a) a la R-f.n. de a. Demostraci´ on. Por SN y lema 4 se tiene que todo elemento tiene una R-f.n. Si la forma normal no fuera u ´nica, entonces R no ser´ıa confluente, pero Newman nos lo asegura. Presentamos ahora un lema que permite relacionar la confluencia entre dos ARS distintos. Este lema es utilizado en el cap´ıtulo 6 para demostrar confluencia del c´ alculo presentado en este trabajo. Lema 7 (Lema de interpretaci´on). Sea R1 una reducci´on que cumple CR y SN, R2 una relaci´ on cualquiera. Sea R = R1 ∪ R2 , y R0 una relaci´on en las R1 -f.n. tal que R0 ⊆ R∗ y a →R2 b =⇒ R1 (a) R0 R1 (b) Entonces, R0 es CR ⇐⇒ R es CR. Demostraci´ on. Ver [CHL96], lema 1.1.

5

1.1 Introducci´ on a la teor´ıa de la reescritura

1.1.2

Presentaci´on de formalismos

Sistemas de Reescritura de T´ erminos (TRS)

Mientras en los ARS se reescriben objetos arbitrarios, en los TRS se reescriben t´erminos de primer orden. Para ello, se definen las reglas de reescritura que especifican como reemplazar parte de un t´ermino por otro. C´omo ejemplo, una definici´ on de los n´ umeros naturales y la operaci´on de suma se puede definir como x+0 x + S(y)

−→ −→

x S(x) + y

donde 0 representa el cero, S(0) el uno, etc. Las variables x e y pueden ser reemplazadas por cualquier t´ermino del sistema. Para computar la suma de (0 + 1) + 2 se puede realizar (0 + S(0)) + S(S(0)) → (S(0) + 0) + S(S(0)) → S(S(0) + 0) + S(0) → S(S(0)) + S(0) → S(S(S(0))) + 0 → S(S(S(0))) A continuaci´ on presentaremos formalmente el concepto de TRS, para el cual necesitaremos primero las siguientes definiciones: Definici´ on 8. • Una signatura es un conjunto de s´ımbolos de funciones. Usualmente se la nota Σ. Un s´ımbolo de funci´on f de aridad n es notado f (n) , pero si por contexto puede deducirse la aridad, ´esta se puede obviar. • Un conjunto de t´erminos TΣ (V ) (tambi´en llamados Σ-t´erminos), con V un conjunto de variables y Σ una signatura, se define induct´ıvamente como – V ⊆ TΣ (V ) – (∀n ≥ 0) (∀f (n) ∈ Σ) (∀t1 , . . . , tn ∈ TΣ (V )) f (t1 , . . . , tn ) ∈ TΣ (V ) En el ejemplo: x, y ∈ V , 0(0) , S (1) , +(2) ∈ Σ , y 0, S(0), 0+S(0) ∈ TΣ (V ). • Un contexto (denotado C) es un t´ermino que contiene exactamente una ocurrencia de un s´ımbolo especial . Notaremos C[t] al reemplazo de  por t en C. • Una sustituci´ on σ es una funci´on V → TΣ (V ) de variables a t´erminos. Notaremos σ(t) al reemplazo de toda variable x en t por σ(x). Dadas dos sustituciones σ y τ , notaremos σ ≤ τ si existe una sustituci´on ρ tal que τ = σ ◦ ρ (◦ es la composici´on de funciones). • La sustituci´ on σ unifica dos t´erminos s y t si σ(s) = σ(t). Si existe tal sustituci´ on, decimos que s y t son unificables. • La sustituci´ on τ es el Unificador M´ as General (umg) de dos t´erminos unificables s y t si para toda sustituci´on σ que unifica a s y t, τ ≤ σ. Dados dos t´erminos unificables, siempre se puede computar su umg (por ejemplo, ver el cap´ıtulo 2 de [Ter03]).

6

1.1 Introducci´ on a la teor´ıa de la reescritura

Presentaci´on de formalismos

• Una regla de reescritura r es un par (s, t) donde s, t ∈ TΣ (V ), y 1. s 6∈ V 2. V (t) ⊆ V (s) donde V (t) son las variables que aparecen en t. Notamos s →r t a dicha regla. Ahora s´ı podemos definir TRS: Definici´ on 9. Un Sistema de Reescritura de T´erminos (TRS ) es un par (TΣ (V ), R), donde R es un conjunto de reglas de reescritura. La reducci´ on R creada por R se define como s →R t sii existen (u, v) ∈ R, σ una sustituci´on, C un contexto, tales que ∧

s = C[σ(u)]

t = C[σ(v)]

Par Cr´ıtico Para el estudio de la confluencia d´ebil, resulta necesario estudiar la interacci´ on entre las reglas. Por ejemplo, en el TRS (1) (2) (3)

−→ −→ −→

x+0 x + S(y) 0+x

x S(x) + y x

desde el t´ermino 0 + S(0) existen dos posibles derivaciones a S(0): S(0) + 0 0 + S(0)

1

S(0)

2

3

S(0)

En este ejemplo, ambos casos reducen al mismo resultado, pero esto podr´ıa no ser as´ı. Definici´ on 10 (Par cr´ıtico). Sean s → t y u → v dos reglas de reescritura. Sea w un subt´ermino de u que no es una variable, y que unifica con s. Sea σ el umg de w y s, y sea C el contexto tal que u = C[w]. El t´ermino σ(u) puede entonces reducirse de dos maneras: σ(u) = σ(C[w]) → σ(C[t])

y σ(u) → σ(v)

El par (σ(C[t]), σ(v)) se llama par cr´ıtico (CP) resultante de la superposici´on de las reglas s → t y u → v. Si s = u y t = v, se pide que s sea unificable con un subt´ermino propio de u. En el ejemplo, el par (S(0) + 0, S(0)) es el par cr´ıtico resultante de la superposici´ on de las reglas 2 y 3. Para m´ as detalles, ver [BN98] cap. 6 o [Ter03] cap. 2. 7

1.1 Introducci´ on a la teor´ıa de la reescritura

Presentaci´on de formalismos

Lema 11 (Critical Pair Lemma). Un TRS es WCR sii todos sus pares cr´ıticos convergen, es decir, para todo par de reglas r, t que forman un par cr´ıtico (b, c), existe d tal que bdc Demostraci´ on. Ver [BN98], teorema 6.2.4. Terminaci´ on Total Presentaremos en esta subsecci´on un concepto de terminaci´on que nos va a permitir en el cap´ıtulo 3 determinar SN de un c´alculo. Este concepto se encuentra desarrollado de [Ter03] secci´on 6.3.2. Definici´ on 12 (Σ-´ algebra mon´otona bien fundada). 1. Una Σ-´ algebra definida sobre la signatura Σ est´a compuesta de un conjunto base A y una interpretaci´on fA : An → A para cada s´ımbolo de funci´on f ∈ Σ de aridad n. 2. Se define una Σ-´ algebra mon´ otona bien fundada (A, >) como una Σ-´algebra cuyo conjunto base A est´a provisto de un orden bien fundado1 > y para todo f ∈ Σ de aridad n, y todos los a1 , . . . , an , b1 , . . . , bn ∈ A en los cuales ai > bi para alg´ un i, y aj = bj para todo j 6= i, se tiene fA (a1 , . . . , an ) > fA (b1 , . . . , bn ) 3. Decimos que una Σ-´ algebra mon´otona bien fundada y no vac´ıa (A, >) es compatible con un TRS si lA > rA para todas las reglas l → r del TRS, donde tA es la interpretaci´on del t´ermino t. Definici´ on 13. Un TRS es totalmente terminante (TT) si admite una Σ-´algebra mon´ otona y bien fundada (A, >) compatible con ´el, en el cual > es total en A. Los teoremas presentados a continuaci´on nos permitir´an deducir cu´ando un c´ alculo es SN a partir de TT. Teorema 14. Si un TRS es TT, entonces es SN. Demostraci´ on. Ver [Zan00] proposici´on 29, o [Ter03] secci´on 6.3.2. Definici´ on 15. Se define el TRS Emb(Σ) para una signatura Σ como aqu´el que tiene el conjunto de reglas f (x1 , . . . , xn ) → xi

(∀f ∈ Σ)(∀i ∈ [1, n])

Teorema 16. Un TRS R es totalmente terminante sii R∪Emb(R) es totalmente terminante. Demostraci´ on. Ver [Zan94], proposici´on 8. 1 Que

no admite cadenas infinitas decrecientes a1 > a2 > . . .

8

1.2 C´ alculo λ

Presentaci´on de formalismos

“Distribution Elimination” Esta subsecci´ on estar´ a dedicada a una t´ecnica presentada por Zantema en [Zan94], que permite simplificar un TRS sin perder la terminaci´on total. Definici´ on 17. Sea l → r una regla de reescritura. Se dice que es una regla distribuidora del s´ımbolo f de aridad n si existe un contexto no trivial C tal que l = C[f (x1 , . . . , xn )] r = f (C[x1 ], . . . , C[xn ]) y f no ocurre en C. Definici´ on 18. Dado un conjunto de t´erminos TΣ (V ), se define la funci´on2 Erasef : TΣ (V ) → P(TΣ (V )), para f ∈ Σ, como = {x} = {g(u Sn 1 , . . . , uk )|(∀i) ui ∈ Erasef (ti )} = i=1 Erasef (ti )

Erasef (x) Erasef (g(t1 , . . . , tk )) Erasef (f (t1 , . . . , tn ))

(∀x ∈ V ) (∀g ∈ Σ, g 6= f )

Definici´ on 19. Sea R un TRS tal que toda regla es o una regla distribuidora de f o una regla donde f no aparece en el lado izquierdo. Erasef (R) es el TRS definido a partir del conjunto de reglas {l → u|l → r ∈ R no es una regla distribuidora de f y u ∈ Erasef (r)} Teorema 20 (Distribution Elimination). Sea R un TRS tal que toda regla es o una regla distribuidora de f o una regla donde f no aparece en el lado izquierdo. Entonces Erasef (R) es totalmente terminante sii R es totalmente terminante. Demostraci´ on. Ver [Zan94], teorema 12.

1.2

C´ alculo λ

El c´ alculo λ fue creado por Alonzo Church en la d´ecada de 1930. Nosotros utilizaremos la versi´ on presentada en [Bar84]. El conjunto de t´erminos del λ c´alculo Λ se encuentra definido para un conjunto de variables V por t ::= x | t t0 | (λx.t)

(x ∈ V )

Definici´ on 21. Se define para un t´ermino t ∈ Λ el conjunto de variables libres de t como FV(x)

=

x

FV(t u)

=

FV(t) ∪ FV(u)

FV(λx.t)

=

FV(t) − {x}

Definici´ on 22. Para t, u ∈ Λ y x ∈ V , definimos t[[x/u]] como la sustituci´on en t de la variable x por u: x[[x/u]] y[[x/u]] (t1 t2 )[[x/u]] (λx.t)[[x/u]] (λy.t)[[x/u]] (λy.t)[[x/u]] 2 Donde

= = = = = =

u y t1 [[x/u]] t2 [[x/u]] λx.t λy.(t[[x/u]]) λz.(t[[y/z]][[x/u]])

(x 6= y)

(y = 6 x ∧ (y 6∈ FV(u) ∨ x 6∈ FV(t))) (y = 6 x ∧ y ∈ FV(u) ∧ x ∈ FV(t))

P es el conjunto de partes

9

1.2 C´ alculo λ

Presentaci´on de formalismos

En el u ´tlimo caso, z es una variable “fresca” (que no figura libre en t ni en u). Definici´ on 23 (≡α ). Sea t = C[λx.u], y sea y 6∈ FV(u). Se dice que t0 se obtiene a partir de t por un cambio de variable ligada si t0 = C[λy.u[[x/y]]]. Decimos que t y t0 son α-congruentes, notado t ≡α t0 , si t0 puede obtenerse por una serie de cambios de variables ligadas. Definici´ on 24 (β-reducci´ on). Se define la relaci´on denominada β-reducci´on entre t´erminos, notada →β , como t →β u sii existe un contexto C y t´erminos v, w tales que t = C[(λx.v) w] u = C[v[[x/w]]] Definici´ on 25. El λ-c´ alculo es el sistema de reducci´on (Λ/ ≡α , β) Observaci´ on 26. El λ-c´ alculo no es SN. Demostraci´ on. Se muestra un contraejemplo. Sea el t´ermino Ω = (λx.x x) (λx.x x) notar que Ω →β Ω. Teorema 27. El λ-c´ alculo es CR. Demostraci´ on. Hay varias pruebas en la literatura. Por ejemplo, [Bar84], secci´on 11.1

1.2.1

λ-c´ alculo simplemente tipado

Presentamos aqu´ı una versi´on expl´ıcitamente tipada del c´alculo. El conjunto de tipos de primer orden T se encuentra definido para un conjunto de variables de tipos VT como T ::= v | T → T (v ∈ VT ) Los t´erminos son modificados para indicar el tipo de las variables en las abstracciones: t ::= x | t t0 | (λx : T.t) (x ∈ V ) Las siguientes definiciones nos permitir´an establecer el tipo de un t´ermino: Definici´ on 28. • Dados un t´ermino M y un tipo σ, una aserci´ on se nota como M : σ, y se lee “el t´ermino M tiene tipo σ”. • Se define base (usualmente notado Γ) a un conjunto de aserciones cuyos t´erminos son variables disjuntas.

10

1.3 C´ alculo λDB

Presentaci´on de formalismos

• Una aserci´ on M : σ se infiere o deriva de una base Γ, notado Γ ` M : σ, si se obtiene de los siguientes axiomas y reglas: Γ ` x:σ

si (x : σ) ∈ Γ

Γ ` M :σ→τ Γ ` N :σ Γ ` M N :τ Γ ∪ {x : σ} ` M : τ Γ ` λx : σ.M : σ → τ El siguiente teorema asegura la perservaci´on del tipo de un t´ermino bajo β-reducciones. Teorema 29 (Subject Reduction). Sean M , N t´erminos, y Γ una base, M →β N

entonces

Γ ` M : σ =⇒ Γ ` N : σ

Demostraci´ on. Ver [Bar92] proposici´on 3.2.11. Teorema 30. Todo t´ermino que puede tiparse dadas las reglas de inferencia de tipos es SN. Demostraci´ on. Existen varias pruebas en la literatura, por ejemplo [GTL89] cap. 6.

1.3

C´ alculo λDB

Nicolaas Govert de Bruijn introduce en [dB72] un c´alculo basado en el λc´ alculo, en el cual reemplaza el conjunto de variables por un conjunto de “´ındices” naturales. Informalmente, cada ´ındice i hace referencia a la cantidad de λ’s que se deben cruzar para encontrar el λ que lo abstrae. A continuaci´on mostramos algunos ejemplos, traduciendo los t´erminos desde el λ-c´alculo: λx.x

se traduce como λ1

λz.z

se traduce como λ1

λy.(λx.y) λx.(λy.x y)

se traduce como λλ2 se traduce como λλ(2 1)

Al realizar esta traducci´ on debe considerarse un caso especial: cuando el λ-t´ermino tiene variables libres. En ese caso se deben realizar algunos pasos adicionales. Primero, se debe establecer un orden entre las variables. Luego se debe cerrar el t´ermino, agregando λ’s abstrayendo las variables libres en el orden establecido. Finalmente se realiza la traducci´on y se quitan los λ’s agregados. C´ omo ejemplo, traduciremos el t´ermino λu.z. 1. Establecemos el orden de variables como x, y, z, u, . . .. 2. Cerramos el t´ermino: λz.λy.λx.(λu.z). 11

1.4 C´ alculo λσ

Presentaci´on de formalismos

(β)

−→

(λa) b

j{i ← b}

=

(a b){i ← c} (λa){i ← b}

= =

Ukj (i)

=

Ukj (a b) Ukj (λa)

= =

a{1 ← b}   j−1 j >i Ui (b) j = i  0 j jj Ukj (a) Ukj (b) Ukj+1 (a)

Figura 1.1: C´alculo λDB 3. Traducimos: λλλλ4. 4. Quitamos los λ’s agregados: λ4. Haciendo este reemplazo de variables por ´ındices se tiene que t´erminos αcongruentes resultan id´enticos en λDB . A continuaci´ on presentaremos la notaci´on utilizada actualmente para describir este c´ alculo. Los t´erminos de λDB se definen como: a ::= i | a a | λa (i ∈ N>0 ) El c´ alculo se encuentra conformado por la regla de reducci´on β y la metasustituci´ on definida en la figura 1.1. Una consecuencia de esta forma de indicar las variables, es que cada vez que se elimina un λ al aplicar la regla β, las variables deben ser actualizadas para reflejar este cambio. Esto explica la complejidad de la sustituci´on. A modo de ejemplo, mostramos una derivaci´on en λ-c´alculo, y su traducci´on en λDB :

1.4

λ

:

(λu.(λw.u) y) z →β (λw.z) y →β z

λDB

:

(λ(λ2) 3) 3 →β (λ4) 2 →β 3

C´ alculo λσ

En el λ-c´ alculo y en λDB , la sustituci´on es una metaoperaci´on del sistema. En [ACCL91] se presenta un c´alculo novedoso que utiliza indices de de Bruijn, en el cual las sustituciones son tratadas de forma expl´ıcita dentro del c´ alculo. Este c´ alculo, denominado λσ, adem´as permite la composici´ on de sustituciones, es decir, dos o m´ as sustituciones pueden ser compuestas en una u ´nica sustituci´ on.

12

1.4 C´ alculo λσ

Presentaci´on de formalismos

(Beta) (VarId) (VarCons) (App) (Abs) (Clos) (IdL) (ShiftId) (ShiftCons) (Map) (Ass)

−→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→

(λa) b 1[id] 1[a · s] (a b)[s] (λa)[s] a[s][t] id ◦ s ↑ ◦id ↑ ◦(a · s) (a · s) ◦ t (s ◦ t) ◦ u

a[b · id] 1 a a[s]b[s] λ(a[1 · (s◦ ↑)]) a[s ◦ t] s ↑ s a[t] · (s ◦ t) s ◦ (t ◦ u)

Figura 1.2: C´alculo λσ Presentamos primero el c´ alculo, para dar luego una breve introducci´on informal de su funcionamiento. En λσ los t´erminos est´ an definidos por dos conjuntos o sorts: el sort de t´erminos propiamente dichos, y el sort de sustituciones. Λσ t { Λσ s {

a ::= 1 | a a | λa | a[s] s ::= id | ↑ | a · s | s ◦ s

El c´ alculo se encuentra definido por las reglas mostradas en la figura 1.2. Se llama σ al c´ alculo de sustituciones asociado, es decir, λσ − Beta. Definici´ on 31. Se define la composici´on n-´esima de una sustituci´on s como s0

=

id

1

s

=

s

i+1

=

s ◦ si

s

Informalmente, un ´ındice de de Bruijn i es notado en este c´alculo como 1[↑i−1 ]. Luego, una sustituci´ on de la forma a1 · a2 · . . . · am · ↑n sustituye las variables de un t´ermino reemplazando 1 por a1 , la variable 2 por a2 , ..., la variable m por am , y el resto de las variables son incrementadas por la diferencia de n − m (que puede ser negativa). La sustituci´on id es interpretada como la sustituci´ on 1 · 2 · 3 · . . ., es decir, la que reemplaza cada variable por s´ı misma. La sustituci´ on ↑ es interpretada como la sustituci´on 2 · 3 · 4 · . . ., es decir, la que reemplaza cada variable i por i + 1.

1.4.1

C´ alculo λσ simplemente tipado

En [ACCL91] se presenta una versi´on simplemente tipada del c´alculo. Una base va a ser simplemente una lista de tipos, permitiendo asignar el i-´esimo tipo a la i-´esima variable. Los t´erminos son modificados para permitir anotaciones de tipo: 13

1.4 C´ alculo λσ

Presentaci´on de formalismos

Tipos Bases T´ erminos Sustituciones

A ::= E ::= a ::= s ::=

K |A→B nil | A, E 1 | a a | λA. a | a[s] id | ↑ | a : A · s | s ◦ s

El c´ alculo λσ simplemente tipado consta de las mismas reglas que el original, con excepci´ on de Beta, VarCons, Abs, ShiftCons, Map que se reemplazan por (Beta) (VarCons) (Abs) (ShiftCons) (Map)

(λA. a) b 1[a : A · s] (λA. a)[s] ↑ ◦(a : A · s) (a : A · s) ◦ t

−→ −→ −→ −→ −→

a[b : A · id] a λA. (a[1 : A · (s◦ ↑)]) s a[t] : A · (s ◦ t)

Definici´ on 32. En base a las reglas de inferencia mostradas abajo, se definen: 1. Un t´ermino a tiene tipo A, seg´ un una base E, notado E ` a : A 2. Una sustituci´ on s actualiza una base E, resultando en la base E 0 , notado E ` s B E0

var lambda app clos id shift cons comp

A, E ` 1 : A A, E ` b : B E ` λA. b : A → B E ` a : B→A E ` b : B E ` ab : A E ` s B E0 E0 ` a : A E ` a[s] : A E ` id B E A, E E ` E E `

`↑B E a : A E ` s B E0 ` (a : A · s) B A, E 0 s00 B E 00 E 00 ` s0 B E 0 E ` s0 ◦ s00 B E 0

En este c´ alculo se cumple que el tipo de un t´ermino se mantiene por reducci´ on: Teorema 33 (Subject Reduction). Sean a y b t´erminos, s y t sustituciones, E y E 0 bases, a →λσ b entonces s →λσ t entonces

E ` a : A =⇒ E ` b : A E ` s B E 0 =⇒ E ` t B E 0

Demostraci´ on. La demostraci´ on en [ACCL91] analiza todas las reglas del c´alculo confirmando que se preserva el tipo para todas ellas.

14

1.4 C´ alculo λσ

1.4.2

Presentaci´on de formalismos

Propiedades de los c´ alculos de sustituciones expl´ıcitas

A la hora de estudiar c´ alculos con sustituciones expl´ıcitas resulta u ´til estudiar las siguientes propiedades: Sea λZ un c´ alculo de sustituciones expl´ıcitas, Z su c´alculo de sustituciones asociado, y toZ una funci´ on que traduce un λ-t´ermino en un λZ -t´ermino, (CRZ ) El c´ alculo Z es confluente. (SNZ ) El c´ alculo Z es fuertemente normalizante. (CR) La relaci´ on →λZ es confluente (en t´erminos cerrados). (MC) La relaci´ on →λZ es confluente en t´erminos abiertos (t´erminos con metavariables). (PSN) La relaci´ on →λZ preserva la normalizaci´ on fuerte de la β-reducci´on: si t ∈ SN λ , entonces toZ (t) ∈ SN λZ (SNt) La relaci´ on →λZ es fuertemente normalizante para todos los t´erminos tipados de λZ . (Sim) La relaci´ on →λZ simula la β-reducci´on: si t →β t0 , entonces toZ (t) λZ 0 toZ (t ). En [ACCL91] se muestra que λσ cumple CRσ , SNσ , CR, Sim. Una prueba directa de SNσ se encuentra en [Zan94], y ser´a presentada en el cap´ıtulo 3. Sin embargo, λσ no cumple con MC, SNt, PSN: Observaci´ on 34. El c´ alculo λσ no es metaconfluente, i.e. confluente en los t´erminos extendidos con metavariables: a ::= X | 1 | a a | λa | a[s] s ::= x | id | ↑ | a · s | s ◦ s Demostraci´ on. Contraejemplo: a[b[s] · s]  ((λa) b)[s]  a[b[s] · (s ◦ id)] Si a = X, b = Y, s = x se tienen dos formas normales distintas. Teorema 35. En el c´ alculo λσ no todo t´ermino tipable es fuertemente normalizante. Adem´ as, λσ no preserva la normalizaci´on fuerte. Demostraci´ on. En [Mel95], Melli`es demuestra que el t´ermino T = (λx.(λy.y) ((λz.z) x)) ((λv.v) w) es tipable en λ c´ alculo (que por el teorema 30 no tiene derivaciones infinitas), y sin embargo su traducci´ on a λσ tambi´en es tipable, pero acepta una derivaci´on infinita.

15

1.4 C´ alculo λσ

1.4.3

Presentaci´on de formalismos

Definiciones

En esta subsecci´ on se presentar´an algunas definiciones y propiedades que permitir´ an el estudio en detalle de λσ y λσgc . Notaci´ on (σ-forma normal de un t´ermino λσ). Dado un t´ermino t de λσ, nos referimos como σ(t) a la u ´nica σ-forma normal del t´ermino. Es u ´nica por ser σ SN y CR (ver subsecci´ on 1.4.2), y por lema 6.

Lema 36 (Caracterizaci´ on de las formas normales). Las σ-f.n. est´an dadas por a ::= 1 | 1[↑n ] | a a | λa s ::= id | ↑n | a · s Demostraci´ on. La prueba se encuentra en [Rio93], y una variaci´on de la prueba se utiliza para demostrar el lema 62. Peso de una sustituci´ on Para caracterizar a las sustituciones, nos va a ser u ´til la presente definici´on de peso de una sustituci´ on, obtenida de [ACCL91] : | · | : Sustituci´on −→ (N × N) |id| |↑| |a · s| |s ◦ t| |s ◦ t|

= = = = =

(0, 0) (0, 1) (m + 1, n) con |s| = (m, n) (m + p − n, q) con |s| = (m, n), |t| = (p, q), p ≥ n (m, q + n − p) con |s| = (m, n), |t| = (p, q), p < n

La idea intuitiva de la definici´on de peso se aprecia por este lema: Lema 37. Sea s una sustituci´on, |s| = (m, n) sii existen t´erminos a1 , . . . , am tales que σ(s) = a1 · a2 · . . . · am · ↑n Demostraci´ on. Por inducci´ on en s. Esta prueba es muy similar a la prueba del lema 68, que sostiene la misma propiedad para el c´alculo σgc . El siguiente lema permite mostrar que la σ-reducci´on no modifica el peso de una sustituci´ on: Lema 38 (Preservaci´ on del peso por reducci´on). Para dos sustituciones s y t, s λσ t =⇒ |s| = |t| Demostraci´ on. Por inducci´ on en la longitud de la derivaci´on, y para el caso base por inducci´ on en s. Esta prueba es muy similar a la prueba del corolario 64, que sostiene la misma propiedad para el c´alculo σgc

16

1.4 C´ alculo λσ

Presentaci´on de formalismos

Variables libres de un t´ ermino No hemos encontrado en la literatura una definici´on formal de variables libres de un t´ermino λσ, por lo que aqu´ı presentamos nuestra definici´on. En la misma, hacemos uso de la siguiente notaci´on para un conjunto de naturales C, un natural n, y un entero m: C>n C +m

= {i | i ∈ C ∧ i > n} = {i + m | i ∈ C ∧ i + m > 0}

Observaci´ on 39. Para C un conjunto de naturales y m, n dos naturales, 1. (C + m) − n = C + (m − n) 2. Para m − n ≥ 0, (C + n)>m = C>m−n + n Demostraci´ on. 1. Se demuestra de forma directa (C + m) − n =

{i + m | i ∈ C ∧ i + m > 0} − n

=

{j − n | j ∈ {i + m | i ∈ C ∧ i + m > 0} ∧ j − n > 0}

=

{(i + m) − n | i ∈ C ∧ i + m > 0 ∧ (i + m) − n > 0}

=

{(i + m) − n | i ∈ C ∧ (i + m) − n > 0}

=

{i + (m − n) | i ∈ C ∧ i + (m − n) > 0}

=

C + (m − n)

2. Tambi´en se demuestra de forma directa (C + n)>m

= {i + n | i ∈ C}>m = {j | j ∈ {i + n | i ∈ C ∧ i + n > 0} ∧ j > m} = {i + n | i ∈ C ∧ i + n > m} = {i + n | i ∈ C ∧ i > m − n} = {i + n | i ∈ C>m−n } = C>m−n + n

Definici´ on 40 (Variables libres de un t´ermino). FV(1) FV(a b) FV(λa) FV(a[s]) FV(id) FV(↑) FV(a · s) FV(s ◦ t)

= = = = = = = =

{1} FV(a) ∪ FV(b) FV(a) − 1 (FV(a)>m + n − m) ∪ FV(s) con |s| = (m, n) ∅ ∅ FV(a) ∪ FV(s) (FV(s)>m + n − m) ∪ FV(t) con |t| = (m, n)

Lema 41 (Preservaci´ on de las variables libres por reducci´on). Sean a y b dos t´erminos, a λσ b =⇒ FV(b) ⊆ FV(a) 17

1.4 C´ alculo λσ

Presentaci´on de formalismos

Demostraci´ on. Por inducci´ on en la cantidad de reducciones, y en el caso base en el t´ermino a. Esta prueba es muy similar a la prueba del corolario 66, que sostiene la misma propiedad para el c´alculo σgc . Observaci´ on 42. Sean a un t´ermino, s y t sustituciones. Entonces, FV(a[s][t]) = FV(a[s ◦ t]) Demostraci´ on. Sean |s| = (m, n) y |t| = (p, q)

FV(a[s][t])

=

(FV(a[s])>p + q − p) ∪ FV(t)

=

(((FV(a)>m + n − m) ∪ FV(s))>p + q − p) ∪ FV(t)

=

((FV(a)>m + n − m)>p + q − p) ∪ ∪(FV(s)>p + q − p) ∪ FV(t)

Dividimos en casos: • p ≥ n: |s ◦ t| = (m + p − n, q) FV(a[s][t])

((FV(a)>m + n − m)>p + q − p) ∪

=

∪(FV(s)>p + q − p) ∪ FV(t) =Obs 39

((FV(a)>m )>p−n+m + q − p + n − m) ∪ ∪(FV(s)>p + q − p) ∪ FV(t) (FV(a)>p−n+m + q − p + n − m) ∪

=

∪(FV(s)>p + q − p) ∪ FV(t) FV(a[s ◦ t])

(FV(a)>m+p−n + q − (m + p − n)) ∪

=

∪FV(s ◦ t) (FV(a)>p−n+m + q − p + n − m) ∪

=

∪(FV(s)>p + q − p) ∪ FV(t) • p < n: |s ◦ t| = (m, q + n − p) FV(a[s][t])

=

((FV(a)>m + n − m)>p + q − p) ∪ ∪(FV(s)>p + q − p) ∪ FV(t)

=

(FV(a)>m + n − m + q − p) ∪ ∪(FV(s)>p + q − p) ∪ FV(t)

FV(a[s ◦ t])

=

(FV(a)>m + q + n − p − m) ∪

=

((FV(a)>m + n − m + q − p) ∪

∪FV(s ◦ t) ∪(FV(s)>p + q − p) ∪ FV(t) En ambos casos se concluye que FV(a[s][t]) = FV(a[s ◦ t]).

18

1.5 C´ alculo λx

Presentaci´on de formalismos

(B)

(λx.t) u x[x/u] y[x/u] (t u)[x/v] (λy.t)[x/v]

−→ −→ −→ −→ −→

t[x/u] u y t[x/v] u[x/v] λy.t[x/v]

(x 6= y)

Figura 1.3: C´alculo λx

1.5

C´ alculo λx

En [Ros93] se presenta λx, el λ-c´alculo con sustituciones expl´ıcitas m´as simple que se puede definir, puesto que introduce la sustituci´on por reglas id´enticas a la del c´ alculo tradicional. La figura 1.3 muestra dicho c´alculo. Este c´ alculo cumple todas las propiedades mencionadas en 1.4.2, excepto metaconfluencia, como lo demuestra el siguiente contraejemplo: t[y/v][x/u[y/v]]  ((λx.t) u)[y/v]  t[x/u][y/v]

1.6

C´ alculo λes

En [Kes07], la autora presenta un c´alculo lambda con sustituciones expl´ıcitas y variables nombradas denominado λes. Dicho c´alculo posee todas las propiedades mencionadas en 1.4.2 Los t´erminos de λes son los mismos que los de λx: t ::= x | t t0 | λx | t[x/t0 ] donde x pertenece a un conjunto enumerable de variables. El c´ alculo se encuentra resumido en la figura 1.4. En ´el podemos apreciar una regla denominada Gc (Garbage Collection), es decir, “recolectora de basura”. Esto es interpretado de la siguiente forma: si la sustituci´on x/u no va a modificar el t´ermino t, entonces es basura y debe ser eliminada. En este caso se cumple cuando x no aparece libre en t. Esta regla fue originalmente concebida para el c´ alculo λxgc[BR95]. Para el c´ alculo λes, el motivo de esta “limpieza” es para evitar que futuras composiciones (ver reglas Comp1 y Comp2 ) no compongan elementos inecesarios, que puedan provocar p´erdidas en las propiedades mencionadas. Este tipo de tratamiento diferencial en las sustituciones cuyas variables a sustituir no aparecen en la variables libres de los t´erminos a sustituir se aprecia tambi´en en el c´ alculo λlxr [KL05], quiz´ as un precursor de λes. Otra particularidad del c´ alculo es la regla de equivalencia C, con lo que la relaci´ on t →λes t0 es interpretada en el conjunto de t´erminos m´ odulo C. Como la aplicaci´ on de las reglas se encuentra condicionada al conocimiento de las variables libres del t´ermino, la metaconfluencia se consigue para metavariables anotadas con un conjunto de variables libres, es decir, para X una metavarible, y ∆ un conjunto de variables, FV(X∆ ) = ∆.

19

(C)

t[x/u][y/v]

=

(B) (Var) (Gc) (App1 ) (App2 ) (App3 ) (Lamb) (Comp1 ) (Comp2 )

(λx.t) u x[x/u] t[x/u] (t u)[x/v] (t u)[x/v] (t u)[x/v] (λy.t)[x/v] t[x/u][y/v] t[x/u][y/v]

−→ −→ −→ −→ −→ −→ −→ −→ −→

t[y/v][x/u] t[x/u] u t t[x/v] u[x/v] t u[x/v] t[x/v] u λy.t[x/v] t[y/v][x/u[y/v]] t[x/u[y/v]]

Figura 1.4: C´alculo λes

(y 6∈ FV(u) ∧ x 6∈ FV(v))

(x 6∈ FV(t)) (x ∈ FV(t) ∧ x ∈ FV(u)) (x 6∈ FV(t) ∧ x ∈ FV(u)) (x ∈ FV(t) ∧ x 6∈ FV(u)) (y ∈ FV(u) ∧ y ∈ FV(t)) (y ∈ FV(u) ∧ y 6∈ FV(t))

Cap´ıtulo 2

C´ alculo λσgc En este cap´ıtulo presentaremos un c´alculo que intenta ser un puente entre los c´ alculos λes y λσ. Primero, en la secci´on 2.1, discutiremos c´omo definir la “basura” en el c´ alculo λσ, y daremos una definici´on. Luego, en la secci´on 2.2 mostraremos c´ omo esta definici´on interact´ ua con el c´alculo λσ. Finalmente, en la secci´ on 2.3 presentaremos al c´alculo λσgc .

2.1

Afectar o no afectar un t´ ermino

En esta secci´ on veremos los elementos a tener en cuenta a la hora de definir “basura” en un c´ alculo como λσ. Recordemos la regla Gc para λes: (GC)

t[x/u]

−→

t

(x 6∈ FV(t))

Nosotros queremos una regla similar en λσ: (GC)

a[s]

−→

a

(condici´ on)

Como se mostr´ o en la secci´on 1.4, en λσ una sustituci´on s con peso (m, n) reemplaza los primeros m ´ındices por los m t´erminos de la sustituci´on. Por ello, es necesario condicionar la regla a que no haya variables libres en a que sean menores o igual a m. Dicho de otra manera, (∀i ∈ FV(a)) i > m. Adem´as, vamos a necesitar que ninguna variable sea actualizada, es decir, m deber´a ser igual a n. Cuando estas condiciones ocurren, decimos que: Definici´ on 43. Una sustituci´on s no afecta a un t´ermino a si (|s| = (m, m) ∧ (∀p ∈ FV(a)) p > m) ∨ FV(a) = ∅ En ese caso, notamos s p\. a. Para el caso contrario, decimos que: Definici´ on 44. Se dice que una sustituci´on s afecta a un t´ermino a si |s| = (m, n) ∧ (m 6= n ∨ (∃p ∈ FV(a)) p ≤ m) ∧ FV(a) 6= ∅ En ese caso, notamos s p. a. 21

2.1 Afectar o no afectar un t´ermino

C´alculo λσgc

Notar que 1· ↑ p. 1. La idea intuitiva es que, aunque la sustituci´on 1· ↑ simule la sustituci´ on id, est´ a reemplazando la variable 1 por otro 1. Definimos entonces la regla GC para λσ como (GC)

−→

a[s]

a

(s p\. a)

Esta definici´ on de “basura” es, en efecto, muy restrictiva, en tanto que no siempre que se aplica GC en λes se puede aplicar GC en λσ, como se puede apreciar en la reducci´ on del t´ermino t del siguiente ejemplo: →Beta(λes)

t = (λu.(λv.y)) x

(λv.y)[u/x]

→GC(λes)

(λv.y)

En λσ, ordenando las variables como x, y, z, u, v, . . ., t se traduce (λλ4) 1

→Beta(λDB )

1

como

(λ4)[1 · id]

que se encuentra en GC (λσ)-forma normal. El inconveniente radica, como se mencion´ o previamente, en que la variable libre del t´ermino (λ4) debe ser decrementada, puesto que las sustituciones provienen de una Beta-reducci´on (con la correspondiente elminaci´ on de un λ). En [Rio93] y en [VARK07] aparece el problema de la actualizaci´on de ´ındices, al tratar con la regla η. Esta regla, en el λ-c´alculo, se define como (η)

λx.M x

=

M

(x 6∈ FV(M ))

Para λσ, en [Rio93] esto se traduce como (Eta)

λ(a 1)

−→

b

(σ(a) = σ(b[↑]))

Es decir, el resultado de aplicar la regla debe computarse como reducir en 1 todos los ´ındices libres de a, aunque no se encuentra explicitado c´omo se debe realizar. En [VARK07] se comentan varios inconvenientes surgidos por esta falta de explicitaci´ on (por ejemplo, la versi´on tipada pierde la propiedad Subject Reduction), y como soluci´ on, sugieren una versi´on constructiva de la regla. Esta versi´ on incluye un subc´ alculo (ηλσ ) cuya finalidad es realizar la actualizaci´on y verificar que la variable 1 no se encuentre libre en a. Para ello se introduce el operador ηji . Luego, la regla queda como (Eta)

λ(a 1)

−→

ηλσ (a[η11 ])

(si ηλσ (a[η11 ]) es un t´ermino λσ)

Esta misma idea podr´ıa aplicarse para hacer m´as general la regla GC. Para ello se podr´ıa definir un subc´ alculo θ que en base a un operador θji actualice en i − j las variables libres mayores a j del t´ermino al que se aplica. Luego, la regla GC quedar´ıa como (GC)

a[s]

−→

n θ(a[θm ])

(si |s| = (m, n) ∧ (∀i ∈ FV(a)) i > m)

A´ un as´ı, la definici´ on de “basura” no es equivalente a la de λes, como lo muestra el siguiente ejemplo: el t´ermino a = x[y/b] se traduce (siguiendo el orden lexicogr´ afico de las variables) a a0 = 1[1 · b0 · ↑] para b0 la traducci´on del t´ermino b. Si bien en a se puede aplicar la regla GC, en a0 no se puede aplicar. 1 Para

este ejemplo, nos basta con traducir primero de λ a λDB , y luego utilizar la convenci´ on i = 1[↑i−1 ] para cada ´ındice i. La traducci´ on de los t´ erminos de λes a λσ es compleja y no ser´ a tratada en este trabajo.

22

2.2 Relaci´ on entre GC y λσ

C´alculo λσgc

Una forma de evitar esto es generalizando la restricci´on (∀i ∈ FV(a)) i > m como (∀i ∈ FV(a)) i > m ∨ (i ≤ m ∧ i[s] σ i) Cada evaluaci´ on de una posible aplicaci´on de la regla debe calcular el valor σ(i[s]) para cada variable libre i, lo que hace que esta opci´on sea costosa desde el punto de vista pr´ actico. Nosotros vamos a estudiar en este trabajo la primer definici´on, dejando para el futuro el estudio de las otras alternativas.

2.2

Relaci´ on entre GC y λσ

En esta secci´ on mostraremos cu´al es la relaci´on entre los t´erminos a[s] y a cuando s p\. a en λσ. Para ello, primero vamos a demostrar un lema que ser´a utilizado frecuentemente durante este trabajo: Lema 45. Sean a, b t´erminos y s una sustituci´on. Entonces, s p\. a ∧ s p\. b ⇐⇒ s p\. (a b) Demostraci´ on. Sea |s| = (m, n). Por definici´on de FV, FV(a b) = FV(a)∪FV(b). ⇒) Tenemos que FV(a) = ∅ ∨ m = n ∧ (∀i ∈ FV(a)) i > m FV(b) = ∅ ∨ m = n ∧ (∀i ∈ FV(b)) i > m Queremos ver que FV(a b) = ∅ ∨ m = n ∧ (∀i ∈ FV(a b)) i > m Separamos en los cuatro casos: (a) FV(a) = ∅ ∧ FV(b) = ∅: FV(a b) = ∅. (b) FV(a) = ∅ ∧ FV(b) 6= ∅: (∀i ∈ FV(b)) i > m

⇐⇒

(∀i ∈ FV(a) ∪ FV(b)) i > m

⇐⇒

(∀i ∈ FV(a b)) i > m

ym=n (c) FV(a) 6= ∅ ∧ FV(b) = ∅: Idem anterior. (d) FV(a) 6= ∅ ∧ FV(b) 6= ∅: (∀i ∈ FV(a)) i > m ∧ (∀i ∈ FV(b)) i > m =⇒ (∀i ∈ FV(a b)) i > m ym=n

23

2.2 Relaci´ on entre GC y λσ

C´alculo λσgc

⇐) Tenemos que FV(a b) = ∅ ∨ m = n ∧ (∀i ∈ FV(a b)) i > m Queremos ver que FV(a) = ∅ ∨ m = n ∧ (∀i ∈ FV(a)) i > m FV(b) = ∅ ∨ m = n ∧ (∀i ∈ FV(b)) i > m Separamos en los dos casos: (a) FV(a b) = ∅ ⇐⇒ FV(a) ∪ FV(b) = ∅ =⇒ FV(a) = ∅ ∧ FV(b) = ∅ (b) FV(a b) 6= ∅: Luego m = n y (∀i ∈ FV(a b)) i > m

⇐⇒

(∀i ∈ FV(a) ∪ FV(b)) i > m

⇐⇒

(∀i ∈ FV(a)) i > m ∧ (∀i ∈ FV(b)) i > m

Observaci´ on 46. s p. a ∨ s p. b ⇐⇒ s p. (a b). El siguiente lema establece que, bajo σ-forma normal, una sustituci´on que no afecta a un t´ermino efectivamente reduce al mismo t´ermino. Lema 47. Sean a un t´ermino en σ-forma normal, y s una sustituci´on tal que s p\. a. Entonces, a[s]  a Demostraci´ on. Por inducci´ on en la forma normal a: • a = 1: s s´ olo puede ser id (notar que para cualquier sustituci´on t, 1·t p. 1), luego a[id] →VarId a. • a = 1[↑n ]: S´ olo puede suceder que |s| = (m, m) con m ≤ n. Por lemas 38, y 37, existen t´erminos b1 , . . . , bm tales que σ(s) = b1 · . . . · bm · ↑m Luego, 1[↑n ][s]

σ

1[↑n ][b1 · . . . · bm · ↑m ]

→Clos

1[↑n ◦(b1 · . . . · bm · ↑m )]

→Assn

1[(↑ ◦(↑ ◦ . . . (↑ ◦(b1 · . . . · bm · ↑m )) . . .))]

→ShiftConsm

1[(↑ ◦ . . . (↑ ◦ ↑m ) . . .)]

=

1[↑n−m+m ]

=

1[↑n ]

Notar que se pueden realizar m pasos de ShiftCons por ser n ≥ m. Con esto se eliminan m ↑’s, que se recuperan de los m ↑’s de s, con lo que efectivamente quedan n.

24

2.3 C´ alculo λσgc

C´alculo λσgc

• a = b c: Por lema 45, s p\. b y s p\. c, luego (b c)[s] →App b[s] c[s] h.i. b c • a = λb: No siempre puede aplicarse la hip´otesis inductiva, con lo que debe utilizarse otra t´ecnica. La demostraci´on de este caso es el resultado principal del ap´endice A.

A continuaci´ on presentamos el resultado principal de esta secci´on, que permite mostrar la relaci´ on existente entre un t´ermino a y una sustituci´on s cuando s no afecta a a. Corolario 48 (Garbage Collection). Si s p\. a, entonces a[s]  a Demostraci´ on. Por lema 41, s p\. a =⇒ s p\. σ(a). Luego, a[s]

σ

σ(a)[s]

L 47

σ(a)

σ

a

Nota 1. No es cierto en general que si s p\. a, entonces a[s]  a. Demostraci´ on. Tomar a = 3[2·id] y s = 1· ↑. Es f´acil notar que |s| = (1, 1), y que las variables libres de a son {2}, con lo que s p\. a. En el ap´endice B se muestra un programa que busca ocurrencias de a en todas las posibles derivaciones del t´ermino a[s], sin encontrarlas, demostrando que efectivamente a[s] 6 a.

2.3

C´ alculo λσgc

En esta secci´ on se muestra el c´alculo que ser´a estudiado en este trabajo, λσgc . Este c´ alculo incluye a GC como una regla de reescritura dentro del c´alculo, y evita la distribuci´ on de la “basura”. Los t´erminos del c´ alculo son los mismos que los de λσ: t T´ erminos Λσgc { a ::= 1 | a a | λa | a[s] s Sustituciones Λσgc { s ::= id | ↑ | a · s | s ◦ s El λσgc -c´ alculo es el TRS conformado por las reglas mostradas en la figura 2.1. Notar que, a diferencia del c´alculo λσ, este TRS tiene infinitas reglas. Por ejemplo, la regla GC es en realidad una regla-esquema, que define una regla para cada a y s que cumplan la condici´on s p\. a. Cabe aclarar que en este trabajo s´ olo se trabajar´ a con t´erminos cerrados, es decir, sin metavariables. Esta definici´ on de TRS con condiciones es diferente a la mencionada en la literatura como “Conditional TRS” (por ejemplo, [BK86]), donde las condiciones se encuentran definidas en t´erminos del propio sistema de reescritura, como en el siguiente ejemplo ([BK86]):

25

2.3 C´ alculo λσgc

(Beta) (GC) (VarCons) (App1 ) (App2 ) (App3 ) (Abs) (Clos) (ClosGC) (IdL) (ShiftId) (ShiftCons) (Map) (MapGC) (Ass)

C´alculo λσgc

(λa) b a[s] 1[a · s] (a b)[s] (a b)[s] (a b)[s] (λa)[s] a[s][t] a[s][t] id ◦ s ↑ ◦id ↑ ◦(a · s) (a · s) ◦ t (a · s) ◦ t (s ◦ t) ◦ u

−→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→ −→

a[b · id] a a a[s] b[s] a[s] b a b[s] λ(a[1 · (s◦ ↑)]) a[s ◦ t] a s ↑ s a[t] · (s ◦ t) a · (s ◦ t) s ◦ (t ◦ u)

(si s p\. a) (si (si (si (si (si (si

s p. a y s p. a y s p\. a y s p. λa) s p. a y s p. a y

s p. b) s p\. b) s p. b) t p. a[s] y s ◦ t p. a) t p. a[s] y s ◦ t p\. a)

(si t p. a) (si t p\. a)

Figura 2.1: C´alculo λσgc Sxyz K xy I x

−→ −→ −→

x z (y z) x x

(si x  I ∧ y  I ∧ z  I) (si x  I ∧ y  I) (si x  I)

Salvo indicaci´ on contraria, no se har´a distinci´on entre regla y regla-esquema. Se llama σgc al c´ alculo de sustituciones asociado, es decir, λσgc − {Beta}. Discusi´ on acerca de las reglas de λσgc El c´ alculo λσgc tiene como principal objetivo evitar la propagaci´on y generaci´ on de “basura”, por ser motivo de p´erdida de la propiedad PSN. 1. La regla GC generaliza a la regla VarId de λσ. 2. La regla Map de λσ se divide en Map y MapGC, con el objetivo de evitar que la “basura” sea distribuida. 3. Lo mismo ocurre para la regla App, que se divide en las tres posibilidades de distribuci´ on a los t´erminos a y b. Notar que la opci´on de no distribuir ni a a ni a b es llevada a cabo por la regla GC. 4. La regla Abs no se aplica a “basura”. En el caso de tener basura, de debe aplicar la regla GC. 5. La regla Clos no permite componer “basura”. Si alguna de las sustituciones es basura, deber´ a ser eliminada por la regla GC. Adem´as, se evita la generaci´ on de basura, como lo muestra el siguiente ejemplo: Sea b = 2, s = 1 · id, t =↑. Es claro que s p. b y t p. b[s]. Pero s ◦ t p\. b, pues |s ◦ t| = |(1 · id)◦ ↑ | = (1, 1), y FV(b) = 2. Por ello se define la regla ClosGC, que elimina la basura producto de la composici´on.

26

2.3 C´ alculo λσgc

C´alculo λσgc

Otras opciones pueden estudiarse para las reglas, como la eliminaci´on de la regla ClosGC (que no figura en λes). Cabe aclarar que en ese caso las demostraciones de los siguientes cap´ıtulos deben ser replanteadas (esto ser´a se˜ nalado en el momento que corresponda).

27

Cap´ıtulo 3

Normalizaci´ on fuerte de σgc En [Rio93] y [CHR92] se demuestra la normalizaci´on fuerte del c´alculo σ utilizando un c´ alculo intermedio (σ0 ), en el cual SN de este c´alculo implica SN de σ. En estos trabajos la prueba de SN de σ0 es compleja. Hans Zantema en [Zan94] presenta una prueba sencilla, mediante la t´ecnica de Distribution Elimination. Nosotros reproducimos esta prueba aqu´ı para demostrar que σgc0 , una variante de σgc , es SN. Zantema presenta otra prueba de terminaci´on fuerte de σ0 en [Ter03] y en [Zan00], mediante la t´ecnica de Semantic Labelling. Esta prueba tambi´en puede ser adaptada para demostar terminaci´on de σgc0 . Los pasos de la demostraci´on ser´an: 1. En 3.1 presentamos σgc0 , una variante simplificada de σgc . 2. En 3.2 mostramos que SN de σgc0 implica SN de σgc . 3. En 3.3 presentamos al c´alculo AMAs, una variante simplificada de σgc0 . En esta secci´ on mostramos que SN de AMAs implica SN de σgc0 . 4. En 3.4 mostramos que AMAs es SN, concluyendo que σgc es SN. Presentamos una definici´ on y un lema que permiten relacionar la terminaci´on de dos c´ alculos: Definici´ on 49. Sean ψ y ω dos c´alculos cuyos t´erminos se encuentran definidos por los conjuntos Ψ y Ω, respectivamente. Sea F una funci´on de Ψ a Ω, decimos que F es estricta 1 sii + s →ψ t =⇒ F (s) →ω F (t) Lema 50. Sean ψ y ω dos c´alculos y F una funci´on estricta del primero al segundo. Entonces ω es SN =⇒ ψ es SN 1 Esta

definici´ on es distinta de la presentada en [Rio93], donde un paso de ψ se traduce a exactamente un paso de ω.

29

3.1 Presentaci´ on de σgc0

Normalizaci´on fuerte de σgc

s◦t 1 ◦ (s · t) (λs) ◦ t id ◦ s ↑ ◦id ↑ ◦(s · t) (s · t) ◦ u (s ◦ t) ◦ u

(K) (VarCons) (Abs) (IdL) (ShiftId) (ShiftCons) (Map) (Ass)

−→ −→ −→ −→ −→ −→ −→ −→

s s λ(s ◦ (1 · (t◦ ↑))) s ↑ t (s ◦ u) · (t ◦ u) s ◦ (t ◦ u)

Figura 3.1: El c´alculo σgc0 Demostraci´ on. Suponemos que no. Entonces, existe una derivaci´on infinita en ψ, tal que s0 →ψ s1 →ψ s2 →ψ . . . Pero por definici´ on de estricta, +

+

+

F (s0 ) →ω F (s1 ) →ω F (s2 ) →ω . . . con lo que se gener´ o una derivaci´on infinita en ω, lo que es absurdo. El absurdo provino de suponer la existencia de una derivaci´on infinita en ψ, luego ψ es SN.

3.1

Presentaci´ on de σgc0

Vamos a extender el c´ alculo presentado en [Rio93] como σ0 , agregando la regla K (similar a la regla GC pero sin condici´on) y quitando la regla VarId. Este nuevo c´ alculo, denominado σgc0 , no distingue t´erminos de sustituciones, generalizando la sustituci´ on y la composici´on en una misma operaci´on. Los t´erminos se encuentran definidos como Λσgc0 {

s ::= 1 | id | ↑ | λs | s ◦ t | s · t

Las reglas se encuentran definidas en la figura 3.1.

3.2

SN de σgc0 implica SN de σgc

Definici´ on 51. Sea F : Λσgc → Λσgc0 la misma funci´on que la presentada en [Rio93]: F (1) F (a b) F (λa) F (a[s])

= = = =

1 F (a) · F (b) λF (a) F (a) ◦ F (s)

F (id) = F (↑) = F (a · s) = F (s ◦ t) =

id ↑ F (a) · F (s) F (s) ◦ F (t)

Lema 52. La funci´ on F es estricta. Demostraci´ on. Sea v →σgc w, vamos a mostrar por inducci´on en la longitud de +

v que F (v) →σgc0 F (w): 30

3.2 SN de σgc0 implica SN de σgc

Normalizaci´on fuerte de σgc

• v ∈ {1, id, ↑}. No hay reducci´on posible. • v = a b: Pueden darse dos casos: +

– w = a0 b, con a →σgc a0 : Por h.i., F (a) →σgc0 F (a0 ), luego +

F (a b) = F (a) · F (b) →σgc0 F (a0 ) · F (b) = F (a0 b) +

– w = a b0 , con a →σgc a0 : Por h.i., F (b) →σgc0 F (b0 ), luego +

F (a b) = F (a) · F (b) →σgc0 F (a) · F (b0 ) = F (a b0 ) +

• v = λa: w = λa0 , con a →σgc a0 . Por h.i., F (a) →σgc0 F (a0 ), luego +

F (λa) = λF (a) →σgc0 λF (a0 ) = F (λa0 ) • v = a[s]: Si la reducci´ on no ocurre en la ra´ız, tenemos los siguientes dos casos: +

– w = a0 [s], con a →σgc a0 : Por h.i., F (a) →σgc0 F (a0 ), luego +

F (a[s]) = F (a) ◦ F (s) →σgc0 F (a0 ) ◦ F (s) = F (a0 [s]) +

– w = a[s0 ], con s →σgc s0 : Por h.i., F (s) →σgc0 F (s0 ), luego +

F (a[s]) = F (a) ◦ F (s) →σgc0 F (a) ◦ F (s0 ) = F (a[s0 ]) Si la reducci´ on ocurre en la ra´ız, hay que considerar todas las posibles reglas: – w = a, y s p\. a: F (a[s]) = F (a) ◦ F (s) →K F (a) – v = 1[b · s],

w = b:

F (1[b · s]) = F (1) ◦ (F (b) · F (s)) →V arCons F (b) – v = (b c)[s],

w = b[s] c[s], con s p. b y s p. c:

F ((b c)[s])

(F (b) · F (c)) ◦ F (s)

= →M ap =

– v = (b c)[s],

(F (b) ◦ F (s)) · (F (c) ◦ F (s)) F (b[s] c[s])

w = b[s] c, con s p. b y s p\. c:

F ((b c)[s])

(F (b) · F (c)) ◦ F (s)

= →M ap →K

(F (b) ◦ F (s)) · (F (c) ◦ F (s)) (F (b) ◦ F (s)) · F (c)

=

F (b[s] c) 31

3.2 SN de σgc0 implica SN de σgc

Normalizaci´on fuerte de σgc

– v = (b c)[s],

w = b c[s], con s p\. b y s p. c: An´alogo al anterior.

– v = (λb)[s],

w = λb[1 · (s◦ ↑)], con s p. λb: F ((λb)[s])

(λF (b)) ◦ F (s)

= →Abs

λ(F (b) ◦ (1 · (F (s)◦ ↑))) F (λb[1 · (s◦ ↑)])

= – v = b[t][s],

w = b[t ◦ s], con t p. b, s p. b[t] y t ◦ s p. b: F (b[t][s])

=

(F (b) ◦ F (t)) ◦ F (s)

→Ass

F (b) ◦ (F (t) ◦ F (s)) F (b[t ◦ s])

= – v = b[t][s],

w = b, con t p. b, s p. b[t] y t ◦ s p\. b: F (b[t][s])

=

(F (b) ◦ F (t)) ◦ F (s)

→Ass

F (b) ◦ (F (t) ◦ F (s))

→K

F (b)

• v = b · s: Pueden darse dos casos: +

– w = b0 · s, con b →σgc b0 : Por h.i., F (b) →σgc0 F (b0 ), luego +

F (b · s) = F (b) · F (s) →σgc0 F (b0 ) · F (s) = F (b0 · s) +

– w = b · s0 , con s →σgc s0 : Por h.i., F (s) →σgc0 F (s0 ), luego +

F (b · s) = F (b) · F (s) →σgc0 F (b) · F (s0 ) = F (b · s0 ) • v = s ◦ t: Si la reducci´ on no ocurre en la ra´ız, tenemos dos casos: +

– w = s0 ◦ t, con s →σgc s0 : Por h.i., F (s) →σgc0 F (s0 ), luego +

F (s ◦ t) = F (s) ◦ F (t) →σgc0 F (s0 ) ◦ F (t) = F (s0 ◦ t) +

– w = s ◦ t0 , con t →σgc t0 : Por h.i., F (t) →σgc0 F (t0 ), luego +

F (s ◦ t) = F (s) ◦ F (t) →σgc0 F (s) ◦ F (t0 ) = F (s ◦ t0 ) Si la reducci´ on ocurre en la ra´ız, entonces hay que analizar todas las reglas que se pueden aplicar: – v = id ◦ s,

w = s: F (id ◦ s) = id ◦ F (s) →IdL F (s)

32

3.3 Presentaci´ on del c´ alculo AMAs

– v =↑ ◦id,

Normalizaci´on fuerte de σgc

w =↑ F (↑ ◦id) =↑ ◦id →Shif tId ↑= F (↑)

– v =↑ ◦(a · s),

w=s

F (↑ ◦(a · s)) =↑ ◦(F (a) · F (s)) →Shif tCons F (s) – v = (a · s) ◦ t,

w = a[t] · (s ◦ t), con t p. a

F ((a · s) ◦ t)

(F (a) · F (s)) ◦ F (t)

= →M ap

F (a[t] · (s ◦ t))

= – v = (a · s) ◦ t,

w = a · (s ◦ t), con t p\. a

F ((a · s) ◦ t)

= →M ap →K

(F (a) · F (s)) ◦ F (t) (F (a) ◦ F (t)) · (F (s) ◦ F (t)) F (a) · (F (s) ◦ F (t)) F (a · (s ◦ t))

= – v = (s ◦ t) ◦ u,

(F (a) ◦ F (t)) · (F (s) ◦ F (t))

w = s ◦ (t ◦ u)

F ((s◦t)◦u) = (F (s)◦F (t))◦F (u) →Ass F (s)◦(F (t)◦F (u)) = F (s◦(t◦u))

Proposici´ on 53. Si σgc0 es SN, entonces σgc es SN. Demostraci´ on. Los lemas 50 y 52 nos lo garantizan.

3.3

Presentaci´ on del c´ alculo AMAs

Definimos un nuevo c´ alculo AMAs que constar´a de las reglas2 Abs, Map, y Ass de σgc0 , y Emb(σgc0 ). Las reglas de reescritura quedan definidas como se muestra en la figura 3.2. Proposici´ on 54. Si AMAs es SN, entonces σgc0 es SN. Demostraci´ on. Es f´ acil notar que la funci´on identidad es una funci´on estricta entre σgc0 y AMAs. Luego, por lema 50, probando SN de AMAs se obtiene SN de σgc0 .

3.4

AMAs es SN

Sea AMAs0 el sub-TRS de AMAs conformado por las reglas Abs, Map, y Ass. Por el teorema 16, AMAs es totalmente terminante sii AMAs0 es totalmente terminante. Podemos notar que Map es una regla distribuidora para ·, luego por el teorema 20, AMAs0 es totalmente terminante sii Erase· (AMAs0 ) es totalmente terminante. El TRS Erase· (AMAs0 ) queda conformado por las reglas 2 De

all´ı su nombre: Abs, Map, Ass

33

3.4 AMAs es SN

Normalizaci´on fuerte de σgc

(Abs) (Map) (Ass)

(λs) ◦ t (s · t) ◦ u (s ◦ t) ◦ u s◦t s◦t s·t s·t λs

−→ −→ −→ −→ −→ −→ −→ −→

λ(s ◦ (1 · (t◦ ↑))) (s ◦ u) · (t ◦ u) s ◦ (t ◦ u) s t s t s

Figura 3.2: C´alculo AMAs (Abs1) (Abs2) (Ass)

(λs) ◦ t (λs) ◦ t (s ◦ t) ◦ u

−→ −→ −→

λ(s ◦ 1) λ(s ◦ (t◦ ↑)) s ◦ (t ◦ u)

Lema 55. Erase· (AMAs0 ) es totalmente terminante. Demostraci´ on. Vamos a mostrar que este TRS es TT mostrando un ´algebra monotona bien fundada y compatible. Como conjunto soporte utilizaremos el espacio A = (N × N × N), y como orden > utilizamos el ´ orden lexicogr´afico. La interpretaci´on de los s´ımbolos de funci´ on estar´ a dada por: 1A =↑A

=

(0, 0, 0)

λA (x1 , x2 , x3 )

=

(x1 + 1, x2 , x3 )

(x1 , x2 , x3 ) ◦A (y1 , y2 , y3 )

=

(x1 + y1 , x1 · (y1 + 1) + x2 + y2 , 2 · x3 + y3 + 1)

Hay que ver que ◦A y λA son mon´otonas en todos sus argumentos. Para la abstracci´ on esto es inmediato. Mostramos que tambi´en vale para la composici´on, es decir: ~x > ~z =⇒ (∀~y ) ~x ◦ ~y > ~z ◦ ~y ∧ ~y ◦ ~x > ~y ◦ ~z Separamos seg´ un la definici´ on de ´orden lexicogr´afico: • x1 > z1 : Como x1 + y1 > z1 + y1 , es cierto para todo v, w que (x1 + y1 , v, w) > (z1 + y1 , v, w) y por ende ~x ◦ ~y > ~z ◦ ~y . De forma an´aloga se prueba para ~y ◦ ~x > ~y ◦ ~z • x1 = z1 ∧x2 > z2 : Restamos los vectores resultantes y vemos si el resultado es mayor a (0, 0, 0): – ~x ◦ ~y > ~z ◦ ~y 1. x1 + y1 − (z1 + y1 ) = 0 2. x1 · (y1 + 1) + x2 + y2 − (z1 · (y1 + 1) + z2 + y2 ) = x2 − z2 > 0 – ~y ◦ ~x > ~y ◦ ~z 1. y1 + x1 − (y1 + z1 ) = 0 2. y1 · (x1 + 1) + y2 + x2 − (y1 · (z1 + 1) + y2 + z2 ) = x2 − z2 > 0

34

3.4 AMAs es SN

Normalizaci´on fuerte de σgc

Notar que no hace falta tener en cuenta la tercer componente del resultado. • x1 = z1 ∧x2 = z2 ∧x3 > z3 : Es f´acil notar que las dos primeras componentes del resultado van a ser iguales, puesto que s´olo utilizan las dos primeras componentes de los operandos. Luego, analizamos la tercer componente: – ~x ◦ ~y > ~z ◦ ~y 2 · x3 + y3 + 1 − (2 · z3 + y3 + 1) = 2 · x3 − 2 · z3 > 0 – ~y ◦ ~x > ~y ◦ ~z 2 · y3 + x3 + 1 − (2 · y3 + z3 + 1) = x3 − z3 > 0 Ahora s´ olo resta ver que esta interpretaci´on es compatible con el sistema Erase· (AMAs0 ). Para ello hay que mostrar que para todas las reglas el lado izquierdo es mayor al lado derecho en esta interpretaci´on. Vamos a calcular regla por regla el valor de cada lado, y compararemos luego el resultado. Abs1 l.

(λ(x1 , x2 , x3 )) ◦ (y1 , y2 , y3 ) = (x1 + 1, x2 , x3 ) ◦ (y1 , y2 , y3 ) = (x1 + 1 + y1 , (x1 + 1) · (y1 + 1) + x2 + y2 , 2 · x3 + y3 + 1)

r.

λ((x1 , x2 , x3 ) ◦ 1) = λ(x1 , x1 + x2 , 2 · x3 + 1) = (x1 + 1, x1 + x2 , 2 · x3 + 1)

Resulta obvio que l > r. Abs2 l.

(λ(x1 , x2 , x3 )) ◦ (y1 , y2 , y3 ) = (x1 + 1 + y1 , (x1 + 1) · (y1 + 1) + x2 + y2 , 2 · x3 + y3 + 1) = (x1 + 1 + y1 , x1 · y1 + x1 + y1 + x2 + y2 + 1, 2 · x3 + y3 + 1)

r.

λ((x1 , x2 , x3 ) ◦ ((y1 , y2 , y3 )◦ ↑)) = λ((x1 , x2 , x3 ) ◦ (y1 , y1 + y2 , 2 · y3 + 1)) = λ(x1 + y1 , x1 · (y1 + 1) + x2 + y1 + y2 , 2 · x3 + 2 · y3 + 2) = (x1 + y1 + 1, x1 · (y1 + 1) + x2 + y1 + y2 , 2 · x3 + 2 · y3 + 2)

Resulta obvio que l > r, puesto que la segunda componente es mayor en l que en r. Ass l.

((x1 , x2 , x3 ) ◦ (y1 , y2 , y3 )) ◦ (z1 , z2 , z3 ) = (x1 + y1 , x1 · (y1 + 1) + x2 + y2 , 2x3 + y3 + 1) ◦ (z1 , z2 , z3 ) = (x1 + y1 + z1 , (x1 + y1 ) · (z1 + 1) + x1 · (y1 + 1) + x2 + y2 + z2 , 2 · (2x3 + y3 + 1) + z3 + 1) = (x1 + y1 + z1 , x1 · (2 + y1 + z1 ) + y1 · (1 + z1 ) + x2 + y2 + z2 , 4 · x3 + 2 · y3 + z3 + 3)

r.

(x1 , x2 , x3 ) ◦ ((y1 , y2 , y3 ) ◦ (z1 , z2 , z3 )) = (x1 , x2 , x3 ) ◦ (y1 + z1 , y1 · (z1 + 1) + y2 + z2 , 2 · y3 + z3 + 1) = (x1 + y1 + z1 , x1 · (y1 + z1 + 1) + x2 + y1 · (z1 + 1) + y2 + z2 , 2 · x3 + 2 · y3 + z3 + 2) = (x1 + y1 + z1 , x1 · (1 + y1 + z1 ) + y1 · (1 + z1 ) + x2 + y2 + z2 , 2 · x3 + 2 · y3 + z3 + 2) 35

3.4 AMAs es SN

Normalizaci´on fuerte de σgc

Resulta obvio que l > r, puesto que la segunda componente es mayor o igual, y la tercera componente es mayor en l que en r. Queda demostrado que Erase· (AMAs0 ) tiene un ´algebra mon´otona bien fundada y compatible, y como el orden lexicogr´afico es total, resulta totalmente terminante.

Lema 56. AMAs es SN. Demostraci´ on. Por lema 55, Erase· (AMAs0 ) es TT. Por teorema 20, AMAs0 es TT. Luego, por teorema 16, AMAs es TT. Finalmente, por teorema 14, AMAs es SN. Ya podemos demostrar el punto principal de este cap´ıtulo: Teorema 57. σgc es fuertemente normalizante. Demostraci´ on. Por lema 56, AMAs es SN, luego por la proposici´on 54 obtenemos SN de σgc0 . Finalmente, la proposici´on 53 nos permite concluir SN de σgc .

36

Cap´ıtulo 4

Lemas u ´ tiles En este cap´ıtulo presentaremos distintos lemas utilizados en los pr´oximos cap´ıtulos. Por ejemplo, en el cap´ıtulo 5 se presenta la necesidad de encontrar un reducto com´ un entre a[s] y a[s ◦ t], para a un t´ermino, s y t sustituciones, tales que s p. a y t p\. a[s]. Este lema, el 78, se llama ClosGcR. Si se intenta demostrar este lema por inducci´on, se encuentra rapidamente con que no es posible. Si la inducci´on es en el t´ermino a, entonces en el caso inductivo a = λb se tiene (λb)[s] →Abs λb[1 · (s◦ ↑)] y (λb)[s ◦ t] →Abs λb[1 · ((s ◦ t)◦ ↑)] con lo que no es posible aplicar la hip´otesis inductiva. Algo similar ocurre si se hace inducci´ on en s. Intuitivamente, si t p\. a[s] es porque no va a modificar a los t´erminos en s, ni va a modificar las variables libres en a[s], con lo que el resultado de sustituir s ◦ t en a es el mismo que el de sustituir s en a. Dicho de otra forma, cada variable libre de a ser´ a reemplazada por el mismo t´ermino ya sea utilizando s como s ◦ t. Hemos formalizado este concepto en el lema 75, en el cual se establece para un t´ermino a, y sustituciones s y t que si para toda variables libre i de a se obtiene que existe un reducto com´ un entre i[s] y i[t], entonces existe un reducto com´ un entre a[s] y a[t]. Luego la demostraci´ on del lema ClosGcR se reduce a mostrar que para toda variable libre i de a existe un reducto com´ un entre i[s] y i[s ◦ t] Tambi´en se demuestra de igual forma el lema 80, que establece la existencia de un reducto com´ un entre a[t] y a[s ◦ t] si s p\. a. Al menos que se especifique lo contrario, notaremos →σgc y σgc como → y , respectivamente. Para algunas demostraciones, vamos a utilizar la siguiente Definici´ on 58. Dada una estrategia de reducci´on cualquiera (por ejemplo, left-most), llamamos σgc 0 (t) a la σgc -f.n. del t´ermino t utilizando esa estrategia particular. Por el teorema 57 sabemos que tal forma normal existe.

37

Lemas u ´tiles

Lema 59. Sean b un t´ermino, s y t sustituciones tales que |s| = (m, n) y |t| = (p, q) FV(b) 6= ∅ ∧ s ◦ t p\. b =⇒ m − n = q − p ∧ (∀i ∈ FV(b)) i > m Demostraci´ on. Dividimos seg´ un la definici´on de s ◦ t. • Si p ≥ n, |s ◦ t| = (m + p − n, q). Por definici´on de p\. , debe suceder que m + p − n = q ∧ (∀i ∈ FV(b)) i > m + p − n Luego, m+p−n=q

⇐⇒

m−n=q−p

y como p ≥ n, (∀i ∈ FV(b)) i > m + p − n =⇒ (∀i ∈ FV(b)) i > m • Si p < n, |s ◦ t| = (m, q + n − p). Por definici´on de p\. , debe suceder que m = q + n − p ∧ (∀i ∈ FV(b)) i > m Luego, m=q+n−p

⇐⇒

m−n=q−p

Lema 60. Sean b un t´ermino, s y t sustituciones: 1. Si s p. b y t p\. b[s], entonces s ◦ t p. b. 2. Si s p\. b y t p. b, entonces s ◦ t p. b. 3. Si s p\. b y t p\. b, entonces s ◦ t p\. b. 4. No es cierto que si s p. b y t p. b[s], entonces s ◦ t p. b. 5. Si s p. b y s ◦ t p\. b, entonces t p. b[s]. 6. Si t p. b y s ◦ t p\. b, entonces s p. b. 7. Si s p\. b y s ◦ t p\. b, entonces t p\. b. 8. Si t p\. b[s] y s ◦ t p\. b, entonces s p\. b. 9. Si s p\. b y s ◦ t p. b, entonces t p. b. Demostraci´ on. Sea |s| = (m, n) y |t| = (p, q). 1. s p. b ∧ t p\. b[s] =⇒ s ◦ t p. b: Suponemos que s ◦ t p\. b. Como s p. b, entonces FV(b) 6= ∅

(4.1)

m−n=q−p

(4.2)

Por lema 59,

38

Lemas u ´tiles

y (∀i ∈ FV(b)) i > m

(4.3)

Si suponemos m = n, por ecuaci´on 4.3 suceder´ıa que s p\. b, lo que es una contradicci´ on. Luego, m 6= n, y por ecuaci´on 4.2, p 6= q

(4.4)

Por hip´ otesis, t p\. b[s], y por ecuaci´on 4.4, FV(b[s]) = ∅. Luego, FV(b[s]) = ∅

=⇒

(FV(b)>m + n − m) ∪ FV(s) = ∅

=⇒

FV(b)>m + n − m = ∅

⇐⇒

FV(b)>m = ∅

Pero por las ecuaciones 4.1 y 4.3, (∃i ∈ FV(b)) i > m, que contradice lo anterior. La contradicci´ on surge de suponer que s ◦ t p\. b. 2. s p\. b ∧ t p. b =⇒ s ◦ t p. b: Como t p. b, entonces FV(b) 6= ∅

(4.5)

p 6= q ∨ (∃i ∈ FV(b)) i ≤ p

(4.6)

y Como s p\. b, por ecuaci´ on 4.5 debe suceder que m = n. Suponemos s◦t p\. b. Por lema 59, m − n = q − p ⇐⇒ m − m = q − p ⇐⇒ p = q Luego, por ecuaci´ on 4.6, (∃i ∈ FV(b)) i ≤ p

(4.7)

Separamos seg´ un la definici´on de peso: • Si p ≥ m, |s ◦ t| = (m + p − m, q) = (p, q). Por suposici´on, (∀i ∈ FV(b)) i > p. Esto contradice la ecuaci´on 4.7. • Si p < m, |s ◦ t| = (m, m + q − p). Por suposici´on, (∀i ∈ FV(b)) i > m > p. Esto contradice la ecuaci´on 4.7. Absurdo, luego s ◦ t p. b. 3. s p\. b ∧ t p\. b =⇒ s ◦ t p\. b: Si FV(b) = ∅, entonces s ◦ t p\. b. Sino, debe suceder que m = n y que p = q y que toda variable libre de b es mayor que p y que m. Luego, por definici´ on de peso: • Si p ≥ m, |s ◦ t| = (m + p − m, p) = (p, p). Como todas las variables libres de b son mayores que p, s ◦ t p\. b. • Si p < m, |s ◦ t| = (m, m + p − p) = (m, m). Como todas las variables libres de b son mayores que m, s ◦ t p\. b. 4. s p. b ∧ t p. b[s] ; s◦t p. b: En la secci´on 2.3 se muestra un contraejemplo. 39

Lemas u ´tiles

5. s p. b ∧ s ◦ t p\. b =⇒ t p. b[s]: Si suponemos que t p\. b[s], como s p. b, por 1 debe suceder que s ◦ t p. b, lo que contradice la hip´ otesis. 6. t p. b ∧ s ◦ t p\. b =⇒ s p. b: Si suponemos que s p\. b, como t p. b, entonces por 2 debe suceder que s ◦ t p. b, lo que contradice la hip´otesis. 7. s p\. b ∧ s ◦ t p\. b =⇒ t p\. b: Si suponemos que t p. b, como s p\. b, entonces por 2 debe suceder que s ◦ t p. b, lo que contradice la hip´otesis. 8. t p\. b[s] ∧ s ◦ t p\. b =⇒ s p\. b: Si suponemos que s p. b, como t p\. b[s], entonces por 1 debe suceder que s ◦ t p. b, lo que contradice la hip´otesis. 9. s p\. b ∧ s ◦ t p. b =⇒ t p. b: Si suponemos que t p\. b, como s p\. b, entonces por 3 debe suceder que s ◦ t p\. b, lo que contradice la hip´otesis.

Lema 61. Sean s y t dos sustituciones de la forma s = a1 · . . . · am · ↑n = b1 · . . . · bp · ↑q

t Entonces

 s◦t

a01 · . . . · a0m · bm+1 · . . . · bp · ↑q a01 · . . . · a0m · ↑q+n−p

Con a0i

 =

si n < p si n ≥ p

ai [t] si t p. ai ai si t p\. ai

Demostraci´ on. s◦t

=

(a1 · . . . · am · ↑n ) ◦ t

→(Map o MapGC)m

a01 · . . . · a0m · (↑n ◦t)

→Assn

a01 · . . . · a0m · (↑ ◦(. . . ◦ (↑ ◦t) . . .)

(si n < p)

→ShiftConsn

a01 · . . . · a0m · bn+1 · . . . · bp · ↑q

(si n ≥ p)

→ShiftConsp

a01 · . . . · a0m · ↑q+n−p

Lema 62 (Caracterizaci´ on de las formas normales). Las σgc -f.n. son las mismas que las σ-f.n., es decir, est´ an dadas por t (Λσgc )nf { a ::= 1 | 1[↑n ] | a a | λa s (Λσgc )nf { s ::= id | ↑n | a · s

40

Lemas u ´tiles

Demostraci´ on. Es claro que los t´erminos generados por la gram´atica son formas normales. Queda por ver que no hay otras formas normales. Separamos los casos por sort. • Sea a un t´ermino de λσgc en σgc -f.n. Vamos a mostrar por inducci´on que el mismo est´ a generado por la gram´atica. – a = 1, es generado por la gram´atica. – a = b c, con b y c en forma normal. Por h. i., b y c est´an generados por la gram´ atica. Entonces b c est´a generado por la gram´atica. – a = λb, con b y s en forma normal. Por h. i., b est´a generado por la gram´ atica. Luego λb est´a generado por la gram´atica. – a = b[s], con b en forma normal. Analizamos seg´ un la forma de b: ∗ b = 1, analizamos s: · s = id, se podr´ıa aplicar GC, con lo que no estar´ıa en forma normal. · s =↑, la gram´atica genera 1[↑]. · s = (c · t), se podr´ıa aplicar VarCons, con lo que no estar´ıa en forma normal. · s = t ◦ u, si t fuera id se podr´ıa aplicar IdL; si t fuera a · s se podr´ıa aplicar Map o MapGC ; si t fuera t1 ◦t2 se podr´ıa aplicar Ass. Con lo que t debe ser ↑. Luego, s =↑ ◦u. Probamos que si ↑ ◦u est´a en σgc -f.n., entonces ∃n ≥ 1, u =↑n : u = id, se podr´ıa aplicar ShiftId. u =↑ u = a · s, se podr´ıa aplicar ShiftCons. u = v ◦ w, como antes, debe suceder que v =↑ y por h.i. w =↑m , con lo que u =↑m+1 Luego, si a = b[s], debe ser b = 1 ∧ s =↑n . ∗ b = b1 b2 , se podr´ıa aplicar GC o alguna App, con lo que no estar´ıa en forma normal. Notar que por lema 45 siempre se puede aplicar alguna de las reglas mencionadas. ∗ b = λc, se podr´ıa aplicar Abs o GC, con lo que no estar´ıa en forma normal. Notar que siempre se puede aplicar alguna de las reglas mencionadas. ∗ b = c[t], se podr´ıa aplicar GC o Clos o ClosGC, con lo que no estar´ıa en forma normal. Notar que siempre se puede aplicar alguna de las reglas mencionadas. Luego s´ olo puede suceder que a = 1[↑n ]. • Sea s una sustituci´ on de λσgc . Vamos a mostrar por inducci´on que la misma est´ a generada por la gram´atica. – s = id, es generada por la gram´atica. – s =↑, es generada por la gram´atica. – s = (a · t), con a y t en forma normal. Por h. i., a y t son generadas por la gram´ atica, luego a · t es generada por la gram´atica.

41

Lemas u ´tiles

– s = s1 ◦ s2 , se sigue el mismo razonamiento que en el item anterior para concluir que s =↑n .

De ahora en m´ as, ∀i ∈ N>1 , i = 1[↑i−1 ]. Lema 63. Para dos sustituciones s y t, s →λσgc t =⇒ |s| = |t| Demostraci´ on. Por inducci´ on en s: • s = id, ↑, no hay reducci´on posible, se satisface vacuamente. • s = a · u, s´ olo es posible reducir en alguno de los t´erminos. – Si t = a0 · u, el peso se mantiene. – Si t = a · u0 , por h. i. |u| = |u0 |. Luego debe ocurrir que |a · u| = |a · u0 |. • s = u ◦ v, pueden ocurrir las siguientes situaciones: – Si t = u0 ◦ v, por h. i. |u| = |u0 |, y se concluye que |s| = |t|. – Si t = u ◦ v 0 , por h. i. |v| = |v 0 |, y se concluye que |s| = |t|. – Si u = id y se aplica IdL, entonces t = v, y |s| = |v| = |t|. – Si u =↑ y v = id, y se aplica ShiftId, entonces t =↑, y |s| = | ↑ | = |t|. – Si u =↑ y v = a · w, y se aplica ShiftCons, entonces t = w. Si |w| = (p, q), entonces |v| = (p+1, q). Entonces |s| = (0 + (p + 1) − 1, q) = (p, q), con lo que |s| = |t|. – Si u = a · w, y se aplica Map o MapGC, entonces t = b · (w ◦ v) (con b = a o b = a[v]). Sea |w| = (m, n) y |v| = (p, q).  (m + 1 + p − n, q) si p ≥ n |s| = |(a · w) ◦ v| = (m + 1, q + n − p) si p < n  |t| = |b · (w ◦ v)| =

(m + p − n + 1, q) si p ≥ n (m + 1, q + n − p) si p < n

En cualquier caso resulta |s| = |t|. – Si u = (w ◦ z), y se aplica Ass, entonces t = w ◦ (z ◦ v). Sean |w| = (m, n) |z| = (p, q) |v| = (i, j)  (m + p − n, q) si p ≥ n |w ◦ z| = (m, q + n − p) si p < n  |z ◦ v| =

(p + i − q, j) si i ≥ q (p, j + q − i) si i < q

42

Lemas u ´tiles

|(w ◦ z) ◦ v| =

|w ◦ (z ◦ v)| =

  (m + p − n + i − q, j) i ≥ q   p≥n   (m + p − n, j + q − i) i < q     (m + i − (q + n − p), j)    pm + n − m) ∪ FV(s) =

FV(c[s])

=

FV(a)

(c) b = c s p\. c Por definici´ on de p. , puede suceder – FV(c) = ∅: FV(b) = ∅ ⊆ FV(a) – FV(c) 6= ∅: m = n ∧ (∀i ∈ FV(c)) i > m FV(a)

=

FV(c[s])

=

(FV(c)>m + m − m) ∪ FV(s)

= FV(c) ∪ FV(s) ⊇ FV(c) =

FV(b)

(d) a = 1[b · s] FV(a)

=

FV(1[b · s])

=

(FV(1)>m+1 + n − (m + 1)) ∪ FV(b · s)

=

FV(b · s)

=

FV(b) ∪ FV(s)

⊇

FV(b)

(e) a = (c d)[s] b = c[s] d[s] s p. c ∧ s p. d FV((c d)[s])

=

(FV(c d)>m + n − m) ∪ FV(s)

=

((FV(c) ∪ FV(d))>m + n − m) ∪ FV(s)

=

(FV(c)>m + n − m) ∪ (FV(d)>m + n − m) ∪ FV(s)

=

((FV(c)>m + n − m) ∪ FV(s)) ∪ ∪((FV(d)>m + n − m) ∪ FV(s))

=

FV(c[s]) ∪ FV(d[s])

=

FV(c[s] d[s])

(f) a = (c d)[s] b = c[s] d FV((c d)[s])

s p. c ∧ s p\. d

=

(FV(c d)>m + n − m) ∪ FV(s)

=

((FV(c)>m + n − m) ∪ FV(s)) ∪ ∪((FV(d)>m + n − m) ∪ FV(s))

=

FV(c[s]) ∪ FV(d[s])

⊇ FV(c[s]) ∪ FV(d) =

FV(c[s] d) 45

Por razonamiento an´alogo al item c

Lemas u ´tiles

(g) a = (c d)[s] b = c d[s] s p\. c ∧ s p. d Por razonamiento an´alogo al anterior. (h) a = (λc)[s] b = λc[1 · (s◦ ↑)] s p. λc FV(a)

FV(b)

=

FV((λc)[s])

=

(FV(λc)>m + n − m) ∪ FV(s)

=

((FV(c) − 1)>m + n − m) ∪ FV(s)

=

FV(λc[1 · (s◦ ↑)])

=

FV(c[1 · (s◦ ↑)]) − 1

=

((FV(c)>m+1 + n + 1 − (m + 1)) ∪ FV(1 · (s◦ ↑)])) − 1

=

((FV(c)>m+1 + n − m) ∪ FV(1) ∪ FV(s◦ ↑)) − 1

=

((FV(c)>m+1 + n − m) ∪ {1} ∪ (FV(s) + 1)) − 1

=

(FV(c)>m+1 + n − m − 1) ∪ FV(s)

=Obs 39

((FV(c) − 1)>m + n − m) ∪ FV(s)

(i) a = c[s][t] b = c[s ◦ t] s p. c ∧ t p. c[s] ∧ s ◦ t p. c Por observaci´ on 42. (j) a = b[s][t] s p. b ∧ t p. b[s] ∧ s ◦ t p\. b Por observaci´ on 42 se tiene que FV(b[s][t]) = FV(b[s ◦ t]). Como s ◦ t p\. b, se sigue el mismo razonamiento que en el item c, y se concluye que FV(b) ⊆ FV(b[s ◦ t]) = FV(b[s][t]) 2.

• a = id, ↑: No hay reducci´on posible, se satisface vacuamente. • s = a · u: (a) t = b · u

a → b: FV(t)

=

FV(b · u)

=

FV(b) ∪ FV(u)

⊆h.i.

(b) t = a · v

FV(a) ∪ FV(u)

=

FV(a · u)

=

FV(s)

=

FV(a · v)

=

FV(a) ∪ FV(v)

⊆h.i.

FV(a) ∪ FV(u)

u → v: FV(t)

• s = u ◦ v: Sean |u| = (m, n) y |v| = (p, q)

46

=

FV(a · u)

=

FV(s)

Lemas u ´tiles

(a) t = w ◦ v

u → w: FV(t)

=

FV(w ◦ v)

=

(FV(w)>p + q − p) ∪ FV(v)

⊆h.i.

(FV(u)>p + q − p) ∪ FV(v)

=

FV(u ◦ v)

=

FV(s)

(b) t = u ◦ w v → w: Por lema 63, |w| = (p, q) FV(t)

=

FV(u ◦ w)

=

(FV(u)>p + q − p) ∪ FV(w)

⊆h.i.

(FV(u)>p + q − p) ∪ FV(v)

=

FV(u ◦ v)

=

FV(s)

(c) s = id ◦ t: FV(s) = FV(id ◦ t) = FV(t) (d) s =↑ ◦id

t =↑:

FV(s) = FV(↑ ◦id) = ∅ = FV(↑) = FV(t) (e) s =↑ ◦(a · t): FV(s)

=

FV(↑ ◦(a · t))

=

FV(a · t)

=

FV(a) ∪ FV(t)

⊇ FV(t) (f) s = (a · u) ◦ v t = a[v] · (u ◦ v) v p. a: Sea |v| = (p, q), FV(s)

=

FV((a · u) ◦ v)

=

(FV(a · u)>p + q − p) ∪ FV(v)

=

((FV(a) ∪ FV(u))>p + q − p) ∪ FV(v)

=

(FV(a)>p + q − p) ∪ (FV(u)>p + q − p) ∪ FV(v)

=

((FV(a)>p + q − p) ∪ FV(v)) ∪ ((FV(u)>p + q − p) ∪ FV(v))

=

((FV(a)>p + q − p) ∪ FV(v)) ∪ FV(u ◦ v)

=

FV(a[v]) ∪ FV(u ◦ v)

=

FV(a[v] · (u ◦ v))

=

FV(t)

(g) s = (a · u) ◦ v

t = a · (u ◦ v) v p\. a:

47

Lemas u ´tiles

Sea |v| = (p, q), FV(s)

=

FV((a · u) ◦ v)

=

FV(a[v]) ∪ FV(u ◦ v) Por razonamiento an´alogo al item anterior

⊇ FV(a) ∪ FV(u ◦ v) Por razonamiento an´alogo al item c =

FV(a · (u ◦ v))

=

FV(t)

(h) s = (u ◦ v) ◦ w t = u ◦ (v ◦ w): Sean |v| = (m, n) y |w| = (p, q), FV(s)

=

FV((u ◦ v) ◦ w)

=

(FV(u ◦ v)>p + q − p) ∪ FV(w)

=

(((FV(u)>m + n − m) ∪ FV(v))>p + q − p) ∪ FV(w)

=

((FV(u)>m + n − m)>p + q − p) ∪

=

((FV(u)>m + n − m)>p + q − p) ∪ FV(v ◦ w)

∪(FV(v)>p + q − p) ∪ FV(w)

Separamos en casos: – p ≥ n: |v ◦ w| = (m + p − n, q) FV(s)

=

((FV(u)>m + n − m)>p + q − p) ∪ FV(v ◦ w)

=

((FV(u)>m )>p−n+m + n − m + q − p) ∪ FV(v ◦ w)

=Obs 39 FV(t)

((FV(u)>p−n+m + n − m + q − p) ∪ FV(v ◦ w)

=

FV(u ◦ (v ◦ w))

=

(FV(u)>m+p−n + q − (m + p − n)) ∪ FV(v ◦ w)

=

(FV(u)>p−n+m + n − m + q − p) ∪ FV(v ◦ w)

– p < n: |v ◦ w| = (m, q + n − p) FV(s)

FV(t)

=

((FV(u)>m + n − m)>p + q − p) ∪ FV(v ◦ w)

=

(FV(u)>m + n − m + q − p) ∪ FV(v ◦ w)

=

FV(u ◦ (v ◦ w))

=

(FV(u)>m + q + n − p − m) ∪ FV(v ◦ w)

Corolario 66 (Preservaci´ on de las variables libres por reducci´on). Sean a y b t´erminos, s y t sustituciones, 1. a λσgc b =⇒ FV(b) ⊆ FV(a) 2. s λσgc t =⇒ FV(t) ⊆ FV(s) 48

Lemas u ´tiles

Demostraci´ on. Por inducci´ on en la cantidad de pasos, aplicando el lema anterior.

Lema 67. Sean a, b t´erminos y s, t sustituciones tales que a λσgc b

,

s λσgc t

,

s p\. a

Entonces s p\. b y t p\. b Demostraci´ on. Por el corolario 66, FV(b) ⊆ FV(a). Luego, por definici´on de p. • o bien FV(a) = ∅, con lo que FV(b) = ∅, luego s p\. b y t p\. b, • o bien |s| = (m, m) y (∀i ∈ FV(a)) i > m, con lo que (∀i ∈ FV(b)) i > m, luego s p\. b. Por lema 63, |t| = (m, m), luego t p\. b

Lema 68. Sea s una sustituci´ on tal que |s| = (m, n). Entonces existen t´erminos a1 , . . . , am tales que σgc 0 (s) = a1 · a2 · ... · am · ↑n con el caso especial σgc 0 (s) = id cuando m = 0 y n = 0. Demostraci´ on. Por lema 62, debe ocurrir que σgc 0 (s) = a1 · a2 · ... · ap · ↑q

∨ σgc 0 (s) = id

Claramente, dicha sustituci´ on tiene peso (p, q), pero como por corolario 64 el peso se mantiene, debe ocurrir que p = m y que q = n.

Lema 69 (IdR). Sea s una sustituci´on, entonces s ◦ id  s. Demostraci´ on. Por inducci´ on estructural en la sustituci´on s: • s = id, tenemos id ◦ id →IdL id • s =↑, tenemos ↑ ◦id →ShiftId ↑ • s = a · t, tenemos (a · t) ◦ id →MapGC a · (t ◦ id)

h.i.



• s = s1 ◦ s2 , tenemos (s1 ◦ s2 ) ◦ id →Ass s1 ◦ (s2 ◦ id)

a·t h.i.



s1 ◦ s2

Lema 70. Sea s una sustituci´on en σgc -forma normal, tal que |s| = (m, n). Por lema 68, existen t´erminos a1 , . . . , am tales que s = a1 · ... · am · ↑n Sea i una variable. 49

∨

s = id

Lemas u ´tiles

1. Si i > m, entonces i[s]  i + n − m. 2. Si i ≤ m, entonces i[s]  ai . Adem´ as, dicha derivaci´ on es u ´nica. Demostraci´ on. Separamos en casos: • Si s = id, i[s] →GC i = i + 0 − 0 • Si i = 1, 1. Si 1 > m, entonces m = 0. 1[↑n ] est´a en forma normal, y corresponde a 1+n−m 2. Si 1 ≤ m, entonces i[a1 · ... · am · ↑n ] →VarCons a1 • Si i = 1[↑i−1 ] y s p\. i. Por definici´on de p. , debe ocurrir que m = n, y que i > m. Luego i[s] →GC i = i + n − m • Si i = 1[↑i−1 ] y s p. i, y ↑i−1 ◦s p. 1. 1[↑i−1 ][s]

1[↑i−1 ◦s]

→Clos =

1[(↑ ◦(↑ ◦(...(↑ ◦ ↑)...))) ◦ s]

→Ass

1[↑ ◦((↑ ◦(...(↑ ◦ ↑)...)) ◦ s)]

→Assi−2

1[↑ ◦(↑ ◦(...(↑ ◦(↑ ◦s))...))] 1[↑ ◦(↑ ◦(...(↑ ◦(↑ ◦(a1 · ... · am · ↑n )))...))]

= 1. 2.

→ShiftConsm

1[↑i−1−m ◦ ↑n ]

→Assi−1−m

1[↑i+n−m−1 ] = i + n − m

→ShiftConsi−1 →VarShift

1[ai · ... · am ↑n ] ai

• Si i = 1[↑i−1 ] y s p. i, pero ↑i−1 ◦s p\. 1. Por definici´on de p. , debe ocurrir que | ↑i−1 ◦s| = (0, 0). Luego, como | ↑i−1 | = (0, i − 1), | ↑i−1 ◦s| = (0 + m − (i − 1), n) = (0, 0) entonces n = 0, y m = i − 1, con lo que 1[↑i−1 ][s] →ClosGC 1 = i + n − m Notar que en cada paso no se pudo aplicar otra regla. La regla ClosGC es imprescindible para lograr esta unicidad en la reducci´on, como lo muestra el siguiente ejemplo: 1 GC

1[↑][a · id]

Clos

1[↑ ◦(a · id)] Sh

ift

50

Co ns

1[id]

Lemas u ´tiles

Lema 71. Sea a un t´ermino en σgc -f. n., y sea s una sustituci´on en σgc -f. n. Si (∀i ∈ FV(a)) i[s]  i entonces a[s]  a. Demostraci´ on. Por inducci´ on en la σgc -f. n. de a: • Caso a = i: Por hip´ otesis vale. • Caso a = a1 a2 : Como FV(ai ) ⊆ FV(a) para i ∈ {1, 2}, vale por h.i. que ai [s]  ai . Luego, a1 a2

≡

GC

(a1 a2 )[s]

App1

a1 [s] a2 [s]

h. i.

h. Ap p 2

a1 [s] a2

h.

a1 a2

i. i.

p3

p

A

a1 a2 [s]

• Caso a = λb: Si s p\. a, (λb)[s] →GC λb = a Sino, (λb)[s] →Abs λb[1 · (s◦ ↑)] Por estar s en σgc -f. n., s = a1 ·...·am · ↑n (notar que s 6= id porque s p. a). Luego, λb[1 · ((a1 · ... · am · ↑n )◦ ↑)]

Map o MapGC

λb[1 · a01 · ... · a0m · ↑n+1 ]

Con a0i = ai o a0i = ai [↑]. Por hip´otesis, sabemos que si i ∈ FV(a), i[s]  i. Por definici´ on de FV, para i > 1, i ∈ FV(λb) ⇔ i + 1 ∈ FV(b). Luego puede ocurrir – Si i + 1 ≤ m + 1, por lema 70 (i + 1)[1 · a01 · ... · a0m · ↑n+1 ]  a0i Por lema 70, hay una u ´nica derivaci´on i[s] = i[a1 · ... · am · ↑n ]  ai Por hip´ otesis, i[s]  i, con lo que ai = i (pues ai est´a en σgc -f.n.). Luego, a0i = ai [↑] = i[↑]  i + 1

51

Lemas u ´tiles

– Si i + 1 > m + 1, por lema 70 (i + 1)[1 · a01 · ... · a0m · ↑n+1 ]  i + 1 + (n + 1) − (m + 1) Como i > m, por lema 70 existe una u ´nica derivaci´on de i[s]  i + n − m Por hip´ otesis, i[s]  i, luego n = m. Con lo que queda (i + 1)[1 · a01 · ... · a0m · ↑n+1 ]  i + 1 En ambos casos, queda (i + 1)[1 · (s◦ ↑)]  i + 1. Si 1 ∈ FV(b), 1[1 · (s◦ ↑)] →VarCons 1. Luego, (∀i ∈ FV(b)) i[1 · (s◦ ↑)]  i, con lo que se puede aplicar h. i. Luego, λb[1 · (s◦ ↑)]  λb

Lema 72. Sean s y t sustituciones en σgc -f. n. y sea i una variable. Si ocurre que |s| = (m, n) ∧ |t| = (p, p) ∧ i > p y (∃c) i[s]  c  i[t] entonces i[s]  i  i[t] Demostraci´ on. Por el lema 70 sabemos que existe una u ´nica derivaci´on a partir de i[t] i[t] → c1 → ... → cn = i Luego, c debe pertenecer a ese camino, es decir i[t] → c1 → ... → c → ... → cn = i Con lo que si i[s]  c, entonces i[s]  c → ... → cn = i

Lema 73. Sean s y t sustituciones en σgc -f. n. y sea a un t´ermino en σgc -f. n. Si ocurre que • s p. a • t p\. a • (∀i ∈ FV(a))(∃ci ) i[s]  ci  i[t] 52

Lemas u ´tiles

Entonces a[s]  a, m´ as a´ un, a[s]  a  a[t] Demostraci´ on. Como s p. a, entonces FV(a) 6= ∅. Luego, con p ∈ N |t| = (p, p) ∧ (∀i ∈ FV(a)) i > p Luego por lema 72 sabemos que (∀i ∈ FV(a)) i[s]  i  i[t] y por lema 71 concluimos que a[s]



←GC

a

a[t]

Lema 74. Sean s y t sustituciones en σgc -f. n. y sea i una variable. Si ocurre que (∃d) i[s]  d  i[t] Entonces, con s = a1 · . . . · am · ↑n t

= b1 · . . . · bp · ↑q

Ocurre 1.

i≤m∧i≤p

=⇒

d  ai = bi

2.

i≤m∧i>p

=⇒

d  ai = i + q − p

3.

i>m∧i≤p

=⇒

d  bi = i + n − m

4.

i>m∧i>p

=⇒

d  i+n−m=i+q−p

Demostraci´ on. 1. Por el lema 70 sabemos que i[s]  ai y i[t]  bi . Adem´as, ambas derivaciones son u ´nicas, luego debe suceder que i[s] → c1 → . . . → cl = d → . . . → cj = ai y i[t] → e1 → . . . → eh = d → . . . → ek = bi Al existir una u ´nica u ´nica derivaci´on desde d hasta ai , sucede que eh+1 = cl+1 ∧ . . . ∧ ej = ck Luego ai = bi . Notar que ai y bi se encuentran en σgc -f. n. 2, 3, 4. Misma demostraci´ on, pero cambiando los t´erminos cj y ek por lo que corresponda seg´ un el lema 70. 53

Lemas u ´tiles

Lema 75 (Reemplazo de variables libres). Sea a un t´ermino en σgc -f. n., y sean s y t dos sustituciones en σgc -f. n. Si (∀i ∈ FV(a))(∃bi ) i[s]  bi  i[t] entonces (∃c) a[s]  c  a[t] Demostraci´ on. Por inducci´ on estructural en a: • Caso a = i: Por hip´ otesis vale. • Caso a = a1 a2 : ≡

a1 a2

a1 a2 G C

C

G

App1

A

p p 2

h. i.

a1 [s] a2 [s] a1 [s] a2

p3 Ap

a1 a2 [s]

a01 a02

h. i.

h. i.

a01 a2

h. i.

h. i.

a1 a02

h. i.

a1 [t] a2 [t] App a1 [t] a2

1

(a1 a2 )[t]

p2

p A

Ap p 3

(a1 a2 )[s]

a1 a2 [t]

El resto de las combinaciones corresponden a casos en los que una sustituci´ on afecta a alguno de los subt´erminos, pero la otra no. En ese caso, por hip´ otesis y por lema 73, se cierra el diagrama. Mostramos un ejemplo: Suponemos que s p. a1 ∧ s p\. a2 ∧ t p\. a1 ∧ t p. a2 (a1 a2 )[s]

→App2

a1 [s] a2

(a1 a2 )[t]

→App3

a1 a2 [t]

Por hip´ otesis, (∀i ∈ FV(a1 ))(∃bi ) i[s]  bi  i[t] (∀j ∈ FV(a2 ))(∃cj ) j[s]  cj  j[t] Luego por lema 73, a1 [s]  a1 y a2 [t]  a2 . Con lo que a1 [s] a2  a1 a2  a1 a2 [t] • Caso a = λb: Para el caso en que alguna de las sustituciones no afecte a a, por el lema 73, o simplemente aplicando GC, sabemos que a[s]



a



a[t]

Para el caso en que ambas sustituciones afecten a a: 54

Lemas u ´tiles

Sean s y t s = c1 · . . . · cm · ↑n t

= d1 · . . . · dp · ↑q

Entonces (λb)[s]

→Abs λb[1 · (s◦ ↑)] = λb[1 · ((c1 · . . . · cm · ↑n )◦ ↑)] (Map o MapGC)m +Ass∗ λb[1 · c01 · . . . · c0m · ↑n+1 ]

(λb)[t]

→Abs λb[1 · (t◦ ↑)] = λb[1 · ((d1 · . . . · dp · ↑q )◦ ↑)] (Map o MapGC)p +Ass∗ λb[1 · d01 · . . . · d0p · ↑q+1 ]

Con

c0i = ci [↑] ∨ c0i = ci d0i = di [↑] ∨ d0i = di

Queremos ver que (∀i ∈ FV(b))(∃ei ) i[1 · c01 · . . . · c0m · ↑n+1 ]  ei  i[1 · d01 · . . . · d0p · ↑q+1 ] Si i ∈ FV(b), entonces o i = 1, o i − 1 ∈ FV(a). Por hip´otesis, (i − 1)[s]  bi−1  (i − 1)[t] Si i = 1, 1[1 · c01 · . . . · c0m · ↑n+1 ]  1  1[1 · d01 · . . . · d0p · ↑q+1 ] Si i > 1, i[1 · c01 · . . . · c0m · ↑n+1 ]  i[1 ·

d01

· ... ·

d0p ·

q+1

↑



 ]

c0i−1 i + (n + 1) − (m + 1) d0i−1 i + (q + 1) − (p + 1)

si i ≤ m + 1 si i > m + 1 si i ≤ p + 1 si i > p + 1

Consideramos los distintos casos: – i ≤ m + 1 ∧ i ≤ p + 1: Por hip´otesis y por lema 74 ci−1 = di−1 . Luego ↑ p. ci−1 ⇐⇒ ↑ p. di−1 , con lo que c0i−1 = d0i−1 . Entonces, i[1 · (s◦ ↑)]  c0i−1 = d0i−1  i[1 · (t◦ ↑)] – i ≤ m+1 ∧ i > p+1: Por hip´otesis y por lema 74 ci−1 = i−1+q −p. Luego, i[1 · (s◦ ↑)]  c0i−1 = (i − 1 + q − p)[↑]  i + q − p  i[1 · (t◦ ↑)] – i > m+1 ∧ i ≤ p+1: Por hip´otesis y por lema 74 di−1 = i−1+n−m. Luego, i[1 · (s◦ ↑)]  i + n − m  (i − 1 + n − m)[↑] = d0i−1  i[1 · (t◦ ↑)] 55

Lemas u ´tiles

– i > m + 1 ∧ i > p + 1: Por hip´otesis y por lema 74 i − 1 + n − m = i − 1 + q − p. Luego, i[1 · (s◦ ↑)]  

(i − 1 + n − m)[↑]  i + n − m = i + q − p (i − 1 + q − p)[↑]  i[1 · (t◦ ↑)]

Encontramos que (∀i ∈ FV(b))(∃ei ) i[1 · (s◦ ↑)]  ei  i[1 · (t◦ ↑)] con lo que por h. i. (∃b0 ) λb[1 · (s◦ ↑)]  b0  λb[1 · (t◦ ↑)]

Observaci´ on 76. Sean s y t dos sustituciones, a un t´ermino, con s = a1 · . . . · am · ↑n y t p\. a[s]. Entonces (∀i) 0 < i ≤ m =⇒ t p\. ai Demostraci´ on. Sea |t| = (p, q). Como t p\. a[s], FV(a[s]) = ∅

∨

p = q ∧ (∀i ∈ FV(a[s])) i > p

Por definici´ on de FV, FV(a[s]) = (FV(a)>m + n − m) ∪ FV(s) = (FV(a)>m + n − m) ∪

m [

FV(aj )

j=1

Luego, para cada aj , o FV(aj ) = ∅ o (∀i ∈ FV(aj )) i > p. Luego, t p\. aj . Lema 77. Sean s y t sustituciones en σgc -f. n., a un t´ermino en σgc -f. n. Si t p\. a[s], entonces (∃c) a[s ◦ t]  c  a[s] Demostraci´ on. Si FV(a) = ∅, entonces a[s ◦ t] →GC a ver qu´e sucede en el otro caso.

←GC

a[s]. Vamos a

Queremos ver que (∀i ∈ FV(a)) (∃di ) i[s ◦ t]  di  i[s] para concluir con el lema 75 que (∃c) a[s ◦ t]  c  a[s] Por estar en forma normal, s = b1 · ... · bm · ↑n

t = c1 · ... · cp · ↑q

Por observaci´ on 76, como t p\. a[s], (∀i) 0 < i ≤ m =⇒ t p\. bi . Entonces s ◦ t →MapGCm b1 · ... · bm · (↑n ◦t)

56

Lemas u ´tiles

Luego, 

n

b1 · ... · bm · (↑ ◦t) Ass + ShiftCons

b1 · ... · bm · cn+1 · ... · cp · ↑q b1 · ... · bm · ↑n+q−p

si n < p si n ≥ p

En el caso que FV(a[s]) = ∅, por definici´on de FV sucede que FV(a)>m = ∅. Luego, (∀i ∈ FV(a)) i ≤ m, con lo que i[s ◦ t]  bi  i[s]. Si FV(a[s]) 6= ∅, entonces p = q. Analizamos los casos: 1. Si n ≥ p, entonces s ◦ t  b1 · ... · bm · ↑n = s, con lo que a[s ◦ t]  a[s]. 2. Si n < p, sea i ∈ FV(a). • Si i ≤ m, entonces i[s]  bi  i[s ◦ t]. • Si i > m, entonces i[s]  i + n − m. Como t p\. a[s], significa que (∀j ∈ FV(a[s])) j > p ⇐⇒ (∀j ∈ (FV(a)>m +n−m)∪FV(s))) j > p Con lo que en particular, al ser i ∈ FV(a), i > m, i + n − m > p ⇐⇒ i > p + m − n Como hay p + m − n t´erminos en b1 · ... · bm · cn+1 · ... · cp · ↑q , por lema 70 tenemos que i[s ◦ t]  i + q − (p + m − n) = i + n − m  i[s] Luego, (∀i ∈ FV(a))(∃di ) i[s◦t]  di  i[s]. Luego por lema 75 obtenemos que (∃d) a[s ◦ t]  d  a[s] En ambos casos se tiene que existe d tal que a[s ◦ t]  d  a[s]. Lema 78 (ClosGcR). Sean s y t sustituciones, a un t´ermino. Si t p\. a[s], entonces (∃c) a[s ◦ t]  c  a[s]. Demostraci´ on. Sean s0

= σgc 0 (s)

t0

= σgc 0 (t)

a0

= σgc 0 (a)

Luego a[s ◦ t]  a0 [s0 ◦ t0 ] a[s]  a0 [s0 ] Por el lema 67, t0 p\. a0 [s0 ]. Luego, por lema 77, (∃c) a0 [s0 ◦ t0 ]  c  a0 [s0 ] Luego (∃c) a[s ◦ t]  c  a[s]

57

Lemas u ´tiles

Lema 79. Sean s y t sustituciones en σgc -f. n., a un t´ermino en σgc -f. n. Si s p\. a, entonces (∃c) a[s ◦ t]  c  a[t]. Demostraci´ on. Si FV(a) = ∅, entonces a[s ◦ t] →GC a ver qu´e sucede en el otro caso. Queremos ver que

←GC

a[t]. Vamos a

(∀i ∈ a) (∃di ) i[s ◦ t]  di  i[t] para concluir con el lema 75 que (∃c) a[s ◦ t]  c  a[t] Por estar en forma normal, s = b1 · ... · bm · ↑n

t = c1 · ... · cp · ↑q

Como estamos en el caso en el que FV(a) 6= ∅, debe suceder que m = n y (∀i ∈ FV(a)) i > m. De ahora en m´as, utilizaremos m en vez de n. Sea b0i = bi [t] ∨ b0i = bi si t p. bi o no, respectivamente. Entonces s ◦ t →(Map o MapGC)m b01 · ... · b0m · (↑m ◦t) Luego, b01 · ... · b0m · (↑m ◦t) Ass + ShiftCons



b01 · ... · b0m · cm+1 · ... · cp · ↑q b01 · ... · b0m · ↑m+q−p

si m < p si m ≥ p

Sea i ∈ FV(a), sabiendo que i > m, analizamos seg´ un el caso: 1. Si m < p, entonces, i[s ◦ t]  i[b01 · ... · b0m · cm+1 · ... · cp · ↑q ] L 70 ci L 70 i[t] 2. Si m ≥ p, entonces i > p, con lo que i[s◦t]  i[b01 ·...·b0m · ↑m+q−p ] L 70 i+(m+q−p)−m = i+q−p L 70 i[t] Luego, (∀i ∈ FV(a))(∃di ) i[s ◦ t]  di  i[t]. Luego por lema 75 obtenemos que (∃d) a[s ◦ t]  d  a[t] Lema 80 (ClosGcL). Sean s y t sustituciones, a un t´ermino. Si s p\. a, entonces (∃c) a[s ◦ t]  c  a[t]. Demostraci´ on. Sean s0

= σgc 0 (s)

t0

= σgc 0 (t)

a0

= σgc 0 (a)

Luego a[s ◦ t]  a0 [s0 ◦ t0 ] a[t]  a0 [t0 ]

58

Lemas u ´tiles

Por el lema 67, s0 p\. a0 . Luego, por lema 79, (∃c) a0 [s0 ◦ t0 ]  c  a0 [t0 ] Luego (∃c) a[s ◦ t]  c  a[t]

Lema 81. Sean a un t´ermino y s una sustituci´on tal que s p. λa, entonces s0 = 1 · (s◦ ↑) p. a. Demostraci´ on. Sea |s| = (m, n). Como s p. λa, entonces FV(λa) 6= ∅ y, o bien m 6= n, o existe i ∈ FV(λa) tal que i ≤ m. Notar que FV(a) 6= ∅. Luego, 1. Si m 6= n, entonces |s0 | = (m + 1, n + 1) cumple con m + 1 6= n + 1, luego s0 p. a. 2. Si existe i ∈ FV(λa) tal que i ≤ m, por definici´on de FV vale que i + 1 ∈ FV(a), con lo que i + 1 ≤ m + 1, y nuevamente s0 p. a.

Lema 82. Sean s una sustituci´on y a un t´ermino, s p\. λa =⇒ (∃c) λa[1 · (s◦ ↑)]  c  λa Demostraci´ on. Sean: |s| = (m, n)

a0 = σgc 0 (a)

t0 = σgc 0 (1 · (s◦ ↑))

Vamos a ver que (∀i ∈ FV(a0 )) i[t0 ]  i Para concluir por lema 71 que λa[1 · (s◦ ↑)]  λa0 [t0 ]  λa0  λa Notar que t0 = 1 · σgc 0 (s◦ ↑) Por definici´ on de p\. , tenemos dos casos: • FV(λa) = ∅: Como FV(λa) = FV(a) \ 1 = ∅, se pueden dar dos casos: – FV(a) = ∅: En este caso, se llega directamente a la conclusi´on sin utilizar el lema: λa[1 · (s◦ ↑)] →GC λa – FV(a) = {1}: Mostramos que se aplican las hip´otesis del lema 71. Como 1[t0 ] →VarCons 1 y por corolario 66 FV(a0 ) ⊆ FV(a), se tiene que (∀i ∈ FV(a0 )) i[t0 ]  i 59

Lemas u ´tiles

• FV(λa) 6= ∅: Entonces m = n y (∀i ∈ FV(λa)) i > m. Luego, como |1 · (s◦ ↑)| = (m + 1, m + 1), para toda variable i ∈ FV(a) tenemos si i > 1

=⇒

i > m + 1 ∧ i[t0 ] L 70 i

si i = 1

=⇒

1[1 · (s◦ ↑)] →VarCons 1

Luego, como por corolario 66 FV(a0 ) ⊆ FV(a), (∀i ∈ FV(a0 )) i[t0 ]  i

Corolario 83. Sean s, t sustituciones y a un t´ermino, s ◦ t p\. λa =⇒ (∃c) λa[1 · (s ◦ (t◦ ↑))]  c  λa Demostraci´ on. La demostraci´ on es igual a la anterior, puesto que para |s ◦ t| = (m, n), |1 · (s ◦ (t◦ ↑))| = |1 · ((s ◦ t)◦ ↑)| = (m + 1, n + 1)

60

Cap´ıtulo 5

Confluencia de σgc En el presente cap´ıtulo se muestra que para t´erminos cerrados (i.e. sin metavariables) se cumple la propiedad de confluencia para el c´alculo asociado. Para ello, vamos a mostrar en 5.1 que el c´alculo es localmente confluente (WCR), para concluir por SN (ver cap´ıtulo 3) que el c´alculo es confluente (CR).

5.1

Confluencia local de σgc

En la presente secci´ on se muestra que para t´erminos cerrados, se cumple la propiedad de confluencia d´ebil o local para el c´alculo asociado. Para ello, utilizaremos el Critical Pair Lemma (lema 11), mostrando que todos los pares cr´ıticos del c´ alculo pueden cerrarse, es decir, si (t0 , t00 ) es un par cr´ıtico, entonces 000 existe t tal que t0  t000  t00 En el contexto de un TRS infinito, se tendr´an infinitos pares cr´ıticos. Por ello, los pares cr´ıticos conformados por reglas-esquemas en realidad ser´an esquemas de pares cr´ıticos. Al mostrar la convergencia de un par cr´ıtico-esquema, se estar´ a mostrando la convergencia de todos los pares cr´ıticos definidos por ´el. De aqu´ı en adelante no se har´ a distinci´on entre par cr´ıtico y par cr´ıtico-esquema. A continuaci´ on mostramos la lista de todos los posibles pares cr´ıticos de σgc , sin tener en cuenta las condiciones de las reglas. Caso por caso, analizamos cuando dichas condiciones no permiten la superposici´on. Como notaci´on utilizaremos t ⇒ (t1 , t2 ) para indicar al par cr´ıtico (t1 , t2 ) que nace del t´ermino t. 1. GC + VarCons: 1[a · s] ⇒ (1, a). No es posible, puesto que a · s p. 1. 2. GC + App1 : (a b)[s] ⇒ (a b, a[s] b[s]). No es posible, puesto que por lema 45 s p\. a b ⇐⇒ s p\. a ∧ s p\. b. 3. GC + App2 : (a b)[s] ⇒ (a b, a[s] b). No es posible por mismo razonamiento que en el item 2. 4. GC + App3 : (a b)[s] ⇒ (a b, a b[s]). No es posible por mismo razonamiento que en el item 2. 5. GC + Abs: (λa)[s] ⇒ (λa, λa[1·(s◦ ↑)]). No es posible pues las condiciones son excluyentes. 61

5.1 Confluencia local de σgc

Confluencia de σgc

6. GC + Clos: a[s][t] ⇒ (a[t], a[s ◦ t]). No es posible pues las condiciones son excluyentes. 7. GC + Clos: a[s][t] ⇒ (a[s], a[s ◦ t]). No es posible pues las condiciones son excluyentes. 8. GC + ClosGC: a[s][t] ⇒ (a[s], a). No es posible pues las condiciones son excluyentes. 9. GC + ClosGC: a[s][t] ⇒ (a[t], a). No es posible pues las condiciones son excluyentes. 10. VarCons + Clos: 1[a·s][t] ⇒ (a[t], 1[(a·s)◦t]). Ser´a analizado m´as adelante. 11. VarCons + ClosGC: 1[a·s][t] ⇒ (a[t], 1). No es posible pues las condiciones son excluyentes. 12. Appi + Appj : para i, j ∈ [1, 3]. No es posible pues las condiciones son excluyentes. 13. Appi + Clos: para i ∈ [1, 3]. Ser´an analizados m´as adelante. 14. Appi + ClosGC: para i ∈ [1, 3]. Ser´an analizados m´as adelante. 15. Abs + Clos: (λa)[s][t] ⇒ ((λa[1 · (s◦ ↑)])[t], (λa)[s ◦ t]). Ser´a analizado m´as adelante. 16. Abs + ClosGC: (λa)[s][t] ⇒ ((λa[1 · (s◦ ↑)])[t], λa). Ser´a analizado m´as adelante. 17. Clos + Clos: a[s][t][u] ⇒ (a[s◦t][u], a[s][t◦u]). Ser´a analizado m´as adelante. 18. Clos + ClosGC: a[s][t][u] ⇒ (a[s ◦ t][u], a[s]). Ser´a analizado m´as adelante. 19. ClosGC + Clos: a[s][t][u] ⇒ (a[u], a[s][t ◦ u]). Ser´a analizado m´as adelante. 20. ClosGC + ClosGC: a[s][t][u] ⇒ (a[u], a[s]). Ser´a analizado m´as adelante. 21. IdL + Ass: (id ◦ s) ◦ t ⇒ (s ◦ t, id ◦ (s ◦ t)). Ser´a analizado m´as adelante. 22. ShiftId + Ass: (↑ ◦id) ◦ t ⇒ (↑ ◦t, ↑ ◦(id ◦ t)). Ser´a analizado m´as adelante. 23. ShiftCons + Ass: (↑ ◦(a · s)) ◦ t ⇒ (s ◦ t, ↑ ◦((a · s) ◦ t)). Ser´a analizado m´ as adelante. 24. Map + Ass: ((a · s) ◦ t) ◦ u ⇒ ((a[t] · (s ◦ t)) ◦ u, (a · s) ◦ (t ◦ u)). Ser´a analizado m´ as adelante. 25. Map + MapGC: (a · s) ◦ t ⇒ (a[t] · (s ◦ t), a · (s ◦ t)). No es posible pues las condiciones son excluyentes. 26. MapGC + Ass: ((a·s)◦t)◦u ⇒ ((a·(s◦t))◦u, (a·s)◦(t◦u)). Ser´a analizado m´ as adelante. 27. Ass + Ass: ((s ◦ t) ◦ u) ◦ v ⇒ ((s ◦ (t ◦ u)) ◦ v, (s ◦ t) ◦ (u ◦ v)). Ser´a analizado m´ as adelante. Para presentar a los pares cr´ıticos vamos a utilizar la siguiente notaci´on: 62

5.1 Confluencia local de σgc

Confluencia de σgc

Regla1 + Regla2 condicion1 , condicion2 , . . . , condicionn para indicar el an´ alisis del par cr´ıtico generado por las reglas Regla1 y Regla2, bajo la condici´ on condicion1 ∧ condicion2 ∧ . . . ∧ condicionn Luego, analizaremos las derivaciones por separado, marcando con un rect´angulo numerado cuando las derivaciones encuentran un t´ermino en com´ un. Seg´ un las reglas que se puedan aplicar, puede ser que las derivaciones se bifurquen seg´ un determinadas condiciones. Estos casos ser´an anotados como sub´ındices de la derivaci´ on original, con las condiciones remarcadas en cada caso: 1.

→Regla1 t0

t

→Reglai . . . →Reglak

i. (si condicioni ) ii.

→Reglaii . . . →Reglakk

(si condicionii )

2.

→Reglaj . . . →Reglal

i. (si condicioni )

→Reglajj . . . →Reglall

(si condicionii )

VarCons + Clos t p. 1[a · s]

1.

1[a · s][t]

1

→VarCons

i. (si t p\. a) 2.

→GC

1[a · s][t]

a

a[t] 2

→Clos 1[(a · s) ◦ t] →Map 1[a[t] · (s ◦ t)]

i. (si t p. a)

→VarCons ii. (si t p\. a)

1

a[t]

→MapGC 1[a · (s ◦ t)] →VarCons

a

2

App1 + Clos s p. a1 ,

s p. a2 ,

t p. (a1 a2 )[s],

1

t000 ii

2

→Regla2 t00

t

ii.

t000 i

s ◦ t p. a1 a2

1. (a1 a2 )[s][t]

→Clos (a1 a2 )[s ◦ t]

2. (a1 a2 )[s][t]

→App1 (a1 [s] a2 [s])[t] 63

t000 i

1

t000 ii

2

5.1 Confluencia local de σgc

Confluencia de σgc

Vemos como se cierran las distintas derivaciones, separando por casos. Notar que t p. (a1 a2 )[s] =⇒ t p. (a1 [s] a2 [s]) pues FV((a b)[s]) = FV(a[s] b[s]) • s ◦ t p. a1 ,

s ◦ t p. a2

1.

(a1 a2 )[s ◦ t]

2.

(a1 [s] a2 [s])[t]

→App1

i. (si t p. a1 [s] ∧ t p. a2 [s])

→App1 a1 [s][t] a2 [s][t] →Clos ×2

ii. (si t p. a1 [s] ∧ t p\. a2 [s])

a1 [s ◦ t] a2 [s ◦ t]

a1 [s ◦ t] a2 [s ◦ t]

→App2 a1 [s][t] a2 [s] →Clos a1 [s ◦ t] a2 [s]

iii. (si t p\. a1 [s] ∧ t p. a2 [s])

→App3 a1 [s] a2 [s][t] →Clos a1 [s] a2 [s ◦ t]

Los casos 2.ii y 2.iii se cierran con el lema 78. • s ◦ t p. a1 ,

s ◦ t p\. a2 , entonces por lema 60.5 t p. a2 [s] 1.

(a1 a2 )[s ◦ t]

2.

(a1 [s] a2 [s])[t] i. (si t p. a1 [s])

→App2

a1 [s ◦ t] a2

→App1 a1 [s][t] a2 [s][t] →Clos + ClosGC

ii. (si t p\. a1 [s])

a1 [s ◦ t] a2

→App3 a1 [s] a2 [s][t] →ClosGC a1 [s] a2

El caso 2.ii se cierra con el lema 78. • s ◦ t p\. a1 , s ◦ t p. a2 , entonces por lema 60.5 t p. a1 [s]. Luego se cierra de forma an´ aloga al caso anterior.

App1 + ClosGC s p. a1 , s p. a2 , t p. (a1 a2 )[s], s ◦ t p\. a1 a2 Por lema 45, s ◦ t p\. a1 y s ◦ t p\. a2 . Luego, por lema 60.5, t p. a1 [s] y t p. a2 [s].

64

5.1 Confluencia local de σgc

Confluencia de σgc

1. (a1 a2 )[s][t]

→ClosGC

2. (a1 a2 )[s][t]

→App1 (a1 [s] a2 [s])[t]

a1 a2

→App1 a1 [s][t] a2 [s][t] →ClosGC ×2

a1 a2

App2 + Clos s p. a1 ,

s p\. a2 ,

t p. (a1 a2 )[s],

s ◦ t p. a1 a2 .

1. (a1 a2 )[s][t]

→App2 (a1 [s] a2 )[t]

2. (a1 a2 )[s][t]

→Clos (a1 a2 )[s ◦ t]

Analizamos los distintos casos: 1. t p. a1 [s],

t p. a2 . Por lema 60.2, s ◦ t p. a2 . (a1 [s] a2 )[t]

→App1 a1 [s][t] a2 [t]

i. (si s ◦ t p. a1 )

→Clos a1 [s ◦ t] a2 [t]

ii. (si s ◦ t p\. a1 )

→ClosGC a1 a2 [t]

1.

(a1 a2 )[s ◦ t]

2.

i. (si s ◦ t p. a1 )

→App1 a1 [s ◦ t] a2 [s ◦ t]

ii. (si s ◦ t p\. a1 )

→App3 a1 a2 [s ◦ t]

Los casos 1.i y 2.i se cierran con el lema 80. Los mismo sucede con los casos 1.ii y 2.ii. No hay otra combinaci´on posible. 2. t p. a1 [s], t p\. a2 . Por lema 60.3, s ◦ t p\. a2 . Por hip´otesis, s ◦ t p. a1 a2 , luego s ◦ t p. a1 . 1.

→App2 a1 [s][t] a2

(a1 [s] a2 )[t]

→Clos 2. 3. t p\. a1 [s],

(a1 a2 )[s ◦ t]

→App2

a1 [s ◦ t] a2 a1 [s ◦ t] a2

t p. a2 . Por lema 60.1, s ◦ t p. a1 y por lema 60.2, s ◦ t p. a2 . 1.

(a1 [s] a2 )[t]

2. (a1 a2 )[s ◦ t]

→App3 a1 [s] a2 [t] →App1 a1 [s ◦ t] a2 [s ◦ t] 65

5.1 Confluencia local de σgc

Confluencia de σgc

El diagrama se cierra con los lemas 80 y 78. 4. t p\. a1 [s],

t p\. a2 . Vamos a mostrar que este caso no puede suceder.

Vamos a mostrar que FV((a1 a2 )[s]) = FV(a1 [s] a2 ), para concluir que si t p\. a1 [s] y t p\. a2 , entonces t p\. (a1 a2 )[s], lo que es absurdo. Sea |s| = (m, n) y |t| = (p, q). Por definici´on de p. , como s p\. a2 debe suceder que m = n y (∀i ∈ FV(a2 )) i > m, o FV(a2 ) = ∅. FV((a1 a2 )[s])

=

(FV(a1 a2 )>m + n − m) ∪ FV(s)

=

(FV(a1 )>m + n − m) ∪ FV(s) ∪ (FV(a2 )>m + n − m)

=

FV(a1 [s]) ∪ FV(a2 )

=

FV(a1 [s] a2 )

Como t p\. a1 [s] y t p\. a2 , se tiene que dar uno de los siguientes casos: • FV(a1 [s]) = FV(a2 ) = ∅: entonces FV(a1 [s] a2 ) = FV((a1 a2 )[s]) = ∅, luego t p\. (a1 a2 )[s], absurdo. • p = q y (∀i ∈ FV(a1 [s]) ∪ FV(a2 )) i > p. Como FV(a1 [s]) ∪ FV(a2 ) = FV(a1 [s] a2 ) = FV((a1 a2 )[s]) se tiene t p\. (a1 a2 )[s], absurdo. En ambos casos se llega al absurdo, entonces no puede suceder que t p\. a1 [s] y t p\. a2 .

App2 + ClosGC s p. a1 , s p\. a2 , t p. (a1 a2 )[s], s ◦ t p\. a1 a2 Por lema 45, s ◦ t p\. a1 a2 =⇒ s ◦ t p\. a1 ∧ s ◦ t p\. a2 . Luego, por lema 60.5, t p. a1 [s] y por lema 60.7, t p\. a2 . 1. (a1 a2 )[s][t]

→ClosGC

2. (a1 a2 )[s][t]

→App2 (a1 [s] a2 )[t]

a1 a2

→App2 a1 [s][t] a2 →ClosGC

a1 a2

App3 + Clos s p\. a1 , s p. a2 , t p. (a1 a2 )[s], s ◦ t p. a1 a2 Demostraci´ on an´ aloga al par cr´ıtico App2 + Clos App3 + ClosGC s p\. a1 , s p. a2 , t p. (a1 a2 )[s], s ◦ t p\. a1 a2 Demostraci´ on an´ aloga al par cr´ıtico App2 + ClosGC

66

5.1 Confluencia local de σgc

Confluencia de σgc

Abs + Clos s p. λa,

t p. (λa)[s], 1. (λa)[s][t]

s ◦ t p. λa →Abs (λa[1 · (s◦ ↑)])[t] →Abs λa[1 · (s◦ ↑)][1 · (t◦ ↑)] →Clos λa[(1 · (s◦ ↑)) ◦ (1 · (t◦ ↑))] →Map λa[1[1 · (t◦ ↑)] · ((s◦ ↑) ◦ (1 · (t◦ ↑)))] →VarCons λa[1 · ((s◦ ↑) ◦ (1 · (t◦ ↑)))] →Ass λa[1 · (s ◦ (↑ ◦(1 · (t◦ ↑))))] →ShiftCons

2. (λa)[s][t]

λa[1 · (s ◦ (t◦ ↑))]

→Clos (λa)[s ◦ t] →Abs λa[1 · ((s ◦ t)◦ ↑)] →Ass

λa[1 · (s ◦ (t◦ ↑))]

Notar que en la primera derivaci´on el segundo paso de Abs se puede realizar puesto que FV((λa)[s]) = FV(λa[1 · (s◦ ↑)]) Notar que para aplicar Clos debemos asegurar que • 1 · (s◦ ↑) p. a. El lema 81 asegura esta condici´on. • 1 · (t◦ ↑) p. a[1 · (s◦ ↑)]. Anteriormente vimos que t p. λa[1 · (s◦ ↑)]. Luego, por lema 81 se tiene que 1 · (t◦ ↑) p. a[1 · (s◦ ↑)] • Sea u = (1 · (s◦ ↑)) ◦ (1 · (t◦ ↑)), u p. a. Como s ◦ t p. λa, por lema 81 obtenemos que 1 · ((s ◦ t)◦ ↑) p. a. F´acilmente se comprueba que u



1 · (s ◦ (t◦ ↑))

y como 1 · ((s ◦ t)◦ ↑) →Ass 1 · (s ◦ (t◦ ↑)) por corolario 64 se tiene que |u| = |1 · (s ◦ (t◦ ↑))| = |1 · ((s ◦ t)◦ ↑)| Luego u p. a ⇐⇒ 1 · ((s ◦ t)◦ ↑) p. a, luego u p. a.

Abs + ClosGC s p. λa,

t p. (λa)[s],

s ◦ t p\. λa

67

5.1 Confluencia local de σgc

1.

Confluencia de σgc

→Abs (λa[1 · (s◦ ↑)])[t]

(λa)[s][t]

→Abs λa[1 · (s◦ ↑)][1 · (t◦ ↑)] i. (si (1 · (s◦ ↑)) ◦ (1 · (t◦ ↑)) p. a)

→Clos λa[(1 · (s◦ ↑)) ◦ (1 · (t◦ ↑))] →Map λa[1[1 · (t◦ ↑)] · ((s◦ ↑) ◦ (1 · (t◦ ↑)))] →VarCons λa[1 · ((s◦ ↑) ◦ (1 · (t◦ ↑)))] →Ass λa[1 · (s ◦ (↑ ◦(1 · (t◦ ↑))))] →ShiftCons λa[1 · (s ◦ (t◦ ↑))]

ii. (si (1 · (s◦ ↑)) ◦ (1 · (t◦ ↑)) p\. a)

→ClosGC

λa

(λa)[s][t]

→ClosGC

λa

2.

Las condiciones t p. λa[1·(s◦ ↑)], 1·(s◦ ↑) p. a, y 1·(t◦ ↑) p. a[1·(s◦ ↑)] necesarias en la primera derivaci´ on se justifican de igual manera que en la demostraci´on anterior. Un reducto com´ un entre la derivaci´on 1.i y 2 puede encontrarse gracias al corolario 83. Clos + Clos s p. a,

t p. a[s], 1.

u p. a[s][t],

s ◦ t p. a,

t ◦ u p. a[s] →Clos a[s ◦ t][u]

a[s][t][u] i. (si (s ◦ t) ◦ u p. a)

→Clos a[(s ◦ t) ◦ u] →Ass

ii. (si (s ◦ t) ◦ u p\. a) 2.

a[s ◦ (t ◦ u)]

→ClosGC

a

2

→Clos a[s][t ◦ u]

a[s][t][u] i. (si s ◦ (t ◦ u) p. a)

→Clos

a[s ◦ (t ◦ u)]

ii. (si s ◦ (t ◦ u) p\. a)

→ClosGC

a

2

Consideraciones: Las derivaciones se corresponden como est´a indicado pues ((s ◦ t) ◦ u) p. a ⇐⇒ (s ◦ (t ◦ u)) p. a Esto resulta como corolario del lema 63. Clos + ClosGC s p. a,

t p. a[s],

u p. a[s][t],

1

s ◦ t p. a, 68

t ◦ u p\. a[s]

1

5.1 Confluencia local de σgc

Confluencia de σgc

Notar que FV(a[s][t]) = FV(a[s ◦ t]), con lo que u p. a[s ◦ t]. 1.

a[s][t][u]

→Clos a[s ◦ t][u] →Clos a[(s ◦ t) ◦ u] →Ass a[s ◦ (t ◦ u)]

2.

a[s][t][u]

→ClosGC a[s]

En la primera derivaci´ on, para aplicar la regla Clos por segunda vez, es necesario mostrar que (s ◦ t) ◦ u p. a. Como s p. a y t ◦ u p\. a[s], por lema 60.1 obtenemos s ◦ (t ◦ u) p. a. Como |(s ◦ t) ◦ u| = |s ◦ (t ◦ u)|, entonces (s ◦ t) ◦ u p. a. El diagrama se cierra con el lema 78. ClosGC + Clos s p. a,

t p. a[s],

s ◦ t p\. a,

u p. a[s][t],

1.

→ClosGC a[u]

a[s][t][u] i. (si u p\. a)

2.

t ◦ u p. a[s]

→GC

a

→Clos a[s][t ◦ u]

a[s][t][u] i. (si s ◦ (t ◦ u) p\. a)

→ClosGC

ii. (si s ◦ (t ◦ u) p. a)

→Clos a[s ◦ (t ◦ u)]

a

Mostramos que u p. a ⇐⇒ s ◦ (t ◦ u) p. a: • Si u p. a, como s ◦ t p\. a, por lema 60.2 se tiene que (s ◦ t) ◦ u p. a. • Si u p\. a, como s ◦ t p\. a, por lema 60.3 se tiene que (s ◦ t) ◦ u p\. a. Luego, como |(s◦t)◦u| = |s◦(t◦u)|, entonces (s◦t)◦u p. a ⇐⇒ s◦(t◦u) p. a. Con esto queda demostrado la correspondencia entre las derivaciones 1.i y 2.i. Nos queda mostrar que existe un reducto com´ un entre las derivaciones 1 y 2.ii. Tomamos una σgc -forma normal de cada t´ermino o sustituci´on que interviene: a0 = σgc 0 (a) s0 = σgc 0 (s)

=

s1 · . . . · sm · ↑n

t = σgc (t)

=

t1 · . . . · tp · ↑q

u0 = σgc 0 (u)

=

u1 · . . . · uj · ↑k

0

0

Con lo que 1. 2.ii

 a0 [u0 ]

a[u] a[s ◦ (t ◦ u)]

69

 a0 [s0 ◦ (t0 ◦ u0 )]

5.1 Confluencia local de σgc

Confluencia de σgc

Queremos ver que (∀i ∈ FV(a0 )) (∃ci ) i[u0 ]  ci  i[s0 ◦ (t0 ◦ u0 )] para concluir con el lema 75 que (∃d) a0 [u0 ]  d  a0 [s0 ◦ (t0 ◦ u0 )] Por lema 70, sabemos que i[u0 ]  ui

si

i≤j

i[u ]  i + k − j

si

i>j

0

Analizamos la relaci´ on entre las componentes del peso. |s ◦ t| = (m + p − n, q)

con p ≥ n

|s ◦ t| = (m, q + n − p)

con p < n

Como s ◦ t p\. a, pero FV(a) 6= ∅, entonces debe suceder que m+p−n=q

⇐⇒

m=q+n−p

⇐⇒

m−n=q−p

y ∀i ∈ FV(a) i > m + p − n si

p≥n

i > m si

p m + p − n = q, i[s0 ◦ (t0 ◦ u0 )]  ui

si

i≤j

i[s ◦ (t0 ◦ u0 )]  i + k − j

si

i>j

0

– j+p−q >n>p (s1 ·. . .·sm · ↑n )◦(t01 ·. . .·t0p ·uq+1 ·. . .·uj · ↑k ) L 61 s01 ·. . .·s0m ·uq+1+n−p ·. . .·uj · ↑k Como (∀i ∈ FV(a0 )) i > m = q + n − p, 0

i[s0 ◦ (t0 ◦ u0 )]  ui

si

i≤j

0

si

i>j

0

i[s ◦ (t ◦ u )]  i + k − j – n≥j+p−q

(s01 ·. . .·s0m · ↑n )◦(t01 ·. . .·t0p ·uq+1 ·. . .·uj · ↑k ) L 61 s01 ·. . .·s0m · ↑k+n−(j+p−q) Como (∀i ∈ FV(a0 )) i > m = q + n − p, i[s0 ◦ (t0 ◦ u0 )]  i + (k + m − j) − m = i + k − j Notar que q + n − p ≥ j, con lo que i > j. 70

5.1 Confluencia local de σgc

• j < q:

Confluencia de σgc

s0 ◦ (t0 ◦ u0 ) L 61 s0 ◦ (t01 · . . . · t0p · ↑k+q−j )

– p≥n (s01 ·. . .·s0m · ↑n )◦(t01 ·. . .·t0p · ↑k+q−j ) L 61 s01 ·. . .·s0m ·t0n+1 ·. . .·t0p · ↑k+q−j Como (∀i ∈ FV(a0 )) i > m + p − n = q, i[s0 ◦ (t0 ◦ u0 )]  i + k + q − j − q = i + k − j Notar que i > q > j. – p m, y n − p − m = −q, i[s0 ◦ (t0 ◦ u0 )]  i + k + q − j + n − p − m = i + k − j Notar que i > m = q + n − p > q > j. Hemos probado que (∀i ∈ FV(a0 ))(∃ci ) i[u0 ]  ci  i[s0 ◦ (t0 ◦ u0 )] Por lema 75, entonces (∃d) a0 [u0 ]  d  a0 [s0 ◦ (t0 ◦ u0 )] Luego ambos t´erminos convergen. ClosGC + ClosGC s p. a, t p. a[s], u p. a[s][t], Notar que FV(a) 6= ∅

s ◦ t p\. a,

t ◦ u p\. a[s]

1.

a[s][t][u]

→ClosGC a[u]

2.

a[s][t][u]

→ClosGC a[s]

Sean |s| =

(m, n)

|t| =

(p, q)

|u| =

(j, k)

Analizamos los pesos de s ◦ t y t ◦ u para ver las condiciones en las que esto sucede: |s ◦ t| = (m + p − n, q)

con p ≥ n

|s ◦ t| = (m, q + n − p)

con p < n

71

5.1 Confluencia local de σgc

Confluencia de σgc

En cualquier caso tenemos: s ◦ t p\. a =⇒ (∀i ∈ FV(a)) i > m ∧ m − n = q − p

|t ◦ u| = (p + j − q, k)

con j ≥ q

|t ◦ u| = (p, k + q − j)

con j < q

(5.1)

Como t ◦ u p\. a[s], tenemos p−q =k−j

(5.2)

y (∀i ∈ FV(a[s])) i > p + j − q

con j ≥ q

(∀i ∈ FV(a[s]))

con j < q

i>p

Por definici´ on de FV: (∀i ∈ FV(a)>m ) i + n − m > p + j − q

con j ≥ q

(∀i ∈ FV(a)>m )

con j < q

i+n−m>p

Entonces, por 5.1, (∀i ∈ FV(a)) i + n − m > p + j − q

con j ≥ q

(5.3)

(∀i ∈ FV(a))

con j < q

(5.4)

i+n−m>p

De 5.1 y 5.2 se deduce que m−n=j−k

(5.5)

Para ver que existe un reducto com´ un, vamos a reducir a una forma normal cada t´ermino o sustituci´ on que interviene. Sean a0

= σgc 0 (a)

s0

= σgc 0 (s)

u0

= σgc 0 (u)

Luego a[s] 

a0 [s0 ]

a[u] 

a0 [u0 ]

Queremos ver que (∀i ∈ FV(a0 )) (∃ci ) i[s0 ]  ci  i[u0 ] para concluir con el lema 75 que (∃d) a0 [s0 ]  d  a0 [u0 ] De 5.1 y el lema 70, se deduce que (∀i ∈ FV(a0 )) i[s0 ]  i + n − m 72

5.1 Confluencia local de σgc

Confluencia de σgc

Si mostramos que (∀i ∈ FV(a0 )) i > j entonces tendr´ıamos que, por lema 70 y ecuaci´on 5.5 (∀i ∈ FV(a0 )) i[u0 ]  i + k − j = i + n − m Separamos en los dos casos del peso de t ◦ u: • j ≥ q: por 5.1 y 5.3, i+n−m>p+j−q

⇐⇒

i+p−q >j+p−q

=⇒

• j < q: por 5.1 y 5.4, i+n−m>p=q−m+n

=⇒

i>q

Hemos probado que (∀i ∈ FV(a0 ))(∃ci ) i[u0 ]  ci  i[s0 ] Por lema 75, entonces (∃d) a0 [u0 ]  d  a0 [s0 ] Luego ambos t´erminos convergen. IdL + Ass

1. (id ◦ s) ◦ t

→IdL

2. (id ◦ s) ◦ t

→Ass id ◦ (s ◦ t) →IdL

s◦t

s◦t

ShiftId + Ass

1. (↑ ◦id) ◦ t

→ShiftId

2. (↑ ◦id) ◦ t

→Ass ↑ ◦(id ◦ t) →IdL

73

↑ ◦t

↑ ◦t

=⇒

i>j

i>j

5.1 Confluencia local de σgc

Confluencia de σgc

ShiftCons + Ass

1. (↑ ◦(a · s)) ◦ t

→ShiftCons

s◦t

2. (↑ ◦(a · s)) ◦ t

→Ass ↑ ◦((a · s) ◦ t) →Map o MapGC ↑ ◦(a0 · (s ◦ t)) →ShiftCons

s◦t

Map + Ass t p. a 1.

((a · s) ◦ t) ◦ u

→Map (a[t] · (s ◦ t)) ◦ u

i. (si u p. a[t])

→Map a[t][u] · ((s ◦ t) ◦ u)

i.1. (si t ◦ u p. a)

→Clos + Ass

i.2. (si t ◦ u p\. a)

→ClosGC + Ass

ii. (si u p\. a[t])

→MapGC a[t] · ((s ◦ t) ◦ u)

a[t ◦ u] · (s ◦ (t ◦ u)) a · (s ◦ (t ◦ u))

1

2

→Ass a[t] · (s ◦ (t ◦ u)) 2.

((a · s) ◦ t) ◦ u

→Ass (a · s) ◦ (t ◦ u)

i. (si t ◦ u p. a)

→Map

ii. (si t ◦ u p\. a)

→MapGC

a[t ◦ u] · (s ◦ (t ◦ u)) a · (s ◦ (t ◦ u))

1

2

Si u p. a[t], entonces resulta evidente que 1.i.1 ⇐⇒ 2.i y 1.i.2 ⇐⇒ 2.ii Si u p\. a[t], entonces no se puede dar el caso 2.ii, pues si u p\. a[t] y t p. a, por lema 60.1, t ◦ u p. a. Luego 1.ii ⇐⇒ 2.i. Un reducto com´ un entre estas derivaciones se encuentra gracias al lema 78. MapGC + Ass t p\. a

74

5.2 Confluencia de σgc

1.

((a · s) ◦ t) ◦ u i. (si u p. a)

Confluencia de σgc

→MapGC (a · (s ◦ t)) ◦ u →Map a[u] · ((s ◦ t) ◦ u) →Ass a[u] · (s ◦ (t ◦ u))

ii. (si u p\. a)

→MapGC a · ((s ◦ t) ◦ u) →Ass

2.

a · (s ◦ (t ◦ u))

((a · s) ◦ t) ◦ u

→Ass (a · s) ◦ (t ◦ u)

i. (si t ◦ u p. a)

→Map a[t ◦ u] · (s ◦ (t ◦ u))

ii. (si t ◦ u p\. a)

→MapGC

a · (s ◦ (t ◦ u))

El paso 1.i cierra con el 2.i con el lema 80. Vemos que 1.i ⇐⇒ 2.i y 1.ii ⇐⇒ 2.ii: • 1.i =⇒ 2.i. Como t p\. a y u p. a, por lema 60.2, t ◦ u p. a. • 1.ii =⇒ 2.ii. Como t p\. a y u p\. a, por lema 60.3, t ◦ u p\. a. • 2.i =⇒ 1.i. Como t p\. a y t ◦ u p. a, por lema 60.9, u p. a. • 2.ii =⇒ 1.ii. Como t p\. a y t ◦ u p\. a, por lema 60.7, u p\. a.

Ass + Ass

1. ((s ◦ t) ◦ u) ◦ w

→Ass (s ◦ (t ◦ u)) ◦ w →Ass

2. ((s ◦ t) ◦ u) ◦ w

s ◦ (t ◦ (u ◦ w))

→Ass (s ◦ t) ◦ (u ◦ w) →Ass

s ◦ (t ◦ (u ◦ w))

Teorema 84. σgc es WCR Demostraci´ on. Hemos dedicado este cap´ıtulo a verificar que todos los pares cr´ıticos se cierran, y se conlcuye por lema 11.

5.2

Confluencia de σgc

Estamos en condiciones de presentar el resultado principal del cap´ıtulo: Teorema 85. [Confluencia σgc ] σgc es CR 75

5.2 Confluencia de σgc

Confluencia de σgc

Demostraci´ on. Por teorema 84, σgc es WCR. Por teorema 57 vimos que σgc es SN. Luego, por Newman (lema 5), σgc es CR. Notaci´ on. σgc (t) denota la u ´nica σgc -f. n. de t. Sabemos que dicha forma normal es u ´nica por CR y SN de σgc (lema 6). t s Lema 86. Sean a ∈ Λσgc y s, t ∈ Λσgc

(∀i ∈ FV(a))(∃bi ) i[s]  bi  i[t] =⇒ (∃c) a[s]  c  a[t] Demostraci´ on. Por confluencia de σgc , para cada i ∈ FV(σgc (a)) ⊆ FV(a) se cumple

i[s]

bi

i[t]

CR

CR b0i

i[σgc (s)]

b00i

CR

i[σgc (t)]

b000 i Luego, por lema 75, a[s]

σgc (a)[σgc (s)]

a[t]

c

σgc (a)[σgc (t)]

t s Lema 87. Sean a, b ∈ Λσgc , s, t ∈ Λσgc , entonces

1. σgc (a[s]) = σgc (σgc (a)[σgc (s)]) 2. σgc (a · s) = σgc (a) · σgc (s) 3. σgc (a b) = σgc (a) σgc (b) 4. σgc (λa) = λσgc (a) 5. σgc (s ◦ t) = σgc (σgc (s) ◦ σgc (t)) Demostraci´ on. 1. Trivial por CR de σgc 2. No hay reglas que se puedan aplicar en la ra´ız del t´ermino, luego 76

5.2 Confluencia de σgc

Confluencia de σgc

a·s σgc (a · s)

CR

=

σgc (a) · σgc (s)

3. Se sigue el mismo razonamiento de la demostraci´on anterior. 4. Se sigue el mismo razonamiento de la demostraci´on anterior. 5. Trivial por CR de σgc

77

Cap´ıtulo 6

Confluencia de λσgc En el presente cap´ıtulo vamos a mostrar la confluencia de λσgc por medio del lema de interpretaci´ on (lema 7). Utilizaremos el resultado del lema 62, y la convenci´ on (∀i ∈ N>1 ) i = 1[↑i−1 ]. Notar que, con dicha convenci´on, las σgc -f. n. son los t´erminos ΛDB . Para poder cumplir con las hip´otesis del lema de interpretaci´on, demostraremos que el c´ alculo tiene las propiedades Simulaci´ on (secci´on 6.1) y Correcci´ on (secci´ on 6.2). Sea →β 0 la menor reducci´ on compatible generada por (λa) b →β 0

a{1 ← b}

t )nf , →β 0 coincide con →β sobre ΛDB . Sobre (Λσgc s Sobre (Λσgc )nf , a1 · . . . · ai · . . . · an · ↑n →β 0 t ssi t = a1 · . . . · a0i · . . . · an · ↑n con ai →β a0i

Lema 88. →β 0 es confluente sobre (Λσgc )nf . Demostraci´ on. Vemos que ∀w ∈ (Λσgc )nf w0  w  w00 00 w

∃w000 w0  w000 

t 1. w ∈ (Λσgc )nf : como β 0 coincide con β y β es confluente, es inmediato. s 2. w ∈ (Λσgc )nf : w = a1 · . . . · an · ↑n

w  w0 =⇒ w0 = a01 · . . . · a0n · ↑n con ai  a0i y w  w00 =⇒ w00 = a001 · . . . · a00n · ↑n con ai  a00i Por el punto anterior, para los t´erminos ai vale la confluencia. Es decir, a0i a000 i

ai a00i

79

6.1 Simulaci´ on

Confluencia de λσgc

Luego, a01 · . . . · a0n · ↑n 000 n a000 1 · . . . · an · ↑

w a001 · . . . · a00n · ↑n

6.1

Simulaci´ on

En la presente secci´ on mostraremos que λσgc simula λDB , es decir w, v ∈ (Λσgc )nf w →β 0 v =⇒ w λσgc v Notaci´ on. Salvo indicaci´ on contraria, utilizaremos → y  para indicar →σgc y σgc , respectivamente. Definici´ on 89. Sean i ≥ 0, n ≥ 1, se define si n como si n = 1 · 2 · . . . · i· ↑i+n−1

s0 n =↑n−1

s0 1 = id

Notar que |si n | = (i, i + n − 1) Observaci´ on 90. 1. n[↑] = 1[↑n−1 ][↑] → 1[↑n−1 ◦ ↑]  1[↑n ] = n + 1 2. 1 · (si n ◦ ↑) = 1 · ((1 · . . . · i· ↑i+n−1 )◦ ↑)  1 · ((1[↑] · . . . · i[↑] · (↑i+n−1 ◦ ↑)))  1 · 2 · . . . · i + 1· ↑i+n = si+1 n Lema 91. Sea j ∈ N, entonces U1j (a) = a Demostraci´ on. Por inducci´ on en el t´ermino, como se menciona en [Rio93]. Lema 92. Sean n, j ∈ N, entonces (∀i ∈ FV(a)) i ≤ j =⇒ Unj (a) = a Demostraci´ on. Por inducci´ on en el t´ermino. • a = m: Por hip´ otesis, m ≤ j. Unj (m) = m • a = c d: Unj (b c) = Unj (b) Unj (c) =h. i. b c 80

6.1 Simulaci´ on

Confluencia de λσgc

• a = λb: Unj (λb) = λUnj+1 (b) =h. i. λb La h. i. se puede aplicar pues (∀i ∈ FV(λb)) i ≤ j =⇒ (∀i ∈ FV(b)) i ≤ j + 1

Lema 93. Sean i, n ∈ N, a ∈ ΛDB , entonces si n p\. a =⇒ Uni (a) = a Demostraci´ on. Por definici´ on de p. y de si n , puede ocurrir: 1. FV(a) = ∅: Por lema 92, Uni (a) = a. 2. n = 1: Por lema 91, U1i (a) = a.

Lema 94. Sean b ∈ ΛDB , i ≥ 0, n ≥ 1, entonces b[si n ] σgc Uni (b) Demostraci´ on. Por inducci´ on en b: • b=1 – i=0 ∗ n = 1 1[s0 1 ] = 1[id] →GC 1 = U10 (1) ∗ n > 1 1[s0 n ] = 1[↑n−1 ] = n = Un0 (1) – i>0 1[si n ] →VarCons 1 = Uni (1) • b=cd – (c d)[si n ] →App1 c[si n ] d[si n ] h. i. Uni (c) Uni (d) = Uni (c d) – (c d)[si n ] →App2 c[si n ] d h. i. Uni (c) d =L 93 Uni (c) Uni (d) = Uni (c d) – (c d)[si n ] →App3 c d[si n ] h. i. c Uni (d) =L 93 Uni (c) Uni (d) = Uni (c d) – (c d)[si n ] →GC c d =L 93 Uni (c d) • b = λc – (λc)[si n ] →Abs λc[1 · (si n ◦ ↑)] Obs 90 λc[si+1 n ] h. i. λUni+1 (c) = Uni (λc) – (λc)[si n ] →GC λc =L 93 Uni (λc) • b=k>1 k[si n ] = 1[↑k−1 ][si n ] →Clos 1[↑k−1 ◦si n ]  k · . . . · i· ↑n+i−1 k − 1 < i ↑k−1 ◦1 · 2 · . . . · i· ↑n+i−1  ↑n+k−2 k−1≥i   k k−11 1 · (bk ◦ ↑)

=

1 · ((1 · . . . · k − 1 · b[↑k−1 ]· ↑k−1 )◦ ↑)



1 · 2 · . . . · k · b[↑k ]· ↑k = bk+1

2. FV(b) = ∅ • k=1 1 · (b1 ◦ ↑) = 1 · ((b · id)◦ ↑)  1 · (b· ↑) = b2 • k>1 1 · (bk ◦ ↑)

=

1 · ((1 · . . . · k − 1 · b· ↑k−1 )◦ ↑)



1 · 2 · . . . · k · b· ↑k = bk+1

Lema 97. Sean k > 0, a, b ∈ ΛDB , entonces (∀i ∈ FV(a)) i < k =⇒ a{k ← b} = a Demostraci´ on. Por inducci´ on en a. • i{k ← b} = i • (c d){k ← b} = c{k ← b} d{k ← b} =h. i. c d • (λc){k ← b} = λc{k + 1 ← b} =h. i. λc

Lema 98. Sean k > 0, a, b ∈ ΛDB , entonces bk p\. a =⇒ a{k ← b} = a 82

6.1 Simulaci´ on

Confluencia de λσgc

Demostraci´ on. Por definici´ on de bk y p. , FV(a) = ∅. Luego, por lema 97, a{k ← b} = a Lema 99. Sean a, b ∈ ΛDB , k ≥ 1, entonces a[bk ]  a{k ← b} Demostraci´ on. Inducci´ on en a • a=1 – k=1 1[b1 ] = 1[b · id] → b =L 91 U10 (b) = 1{1 ← b} – k>1 1[bk ] → 1 = 1{k ← b} • a=cd – (c d)[bk ] →App1 c[bk ] d[bk ] h. i. c{k ← b} d{k ← b} = (c d){k ← b} – (c d)[bk ] →App2 c[bk ] d h. i. c{k ← b} d =L 98 c{k ← b} d{k ← b} = (c d){k ← b} – (c d)[bk ] →App3 c d[bk ] h. i. c d{k ← b} =L 98 c{k ← b} d{k ← b} = (c d){k ← b} – (c d)[bk ] →GC c d =L 98 (c d){k ← b} • a = λc – (λc)[bk ] →Abs λc[1 · (bk ◦ ↑)] Obs 96 λc[bk+1 ] h. i. λc{k + 1 ← b} = (λc){k ← b} – (λc)[bk ] →GC λc =L 98 (λc){k ← b} • a=m>1

m[bk ] = 1[↑m−1 ][bk ] → 1[↑m−1 ◦bk ]

– k=1 1[↑m−1 ◦(b · id)]  1[↑m−2 ] = m − 1 = m{1 ← b} – k>1   m · . . . · k − 1 · b0 · ↑k−1 m < k m−1 0 k−1 b0 · ↑k−1 m=k ↑ ◦(1 · . . . · k − 1 · b · ↑ )  m−2 ↑ m>k    mk Con b0 = b si FV(b) = ∅ o b0 = b[↑k−1 ] si no.

Corolario 100. Sean a, b ∈ ΛDB , k ≥ 1, entonces σgc (a[b · id]) = a{1 ← b} Demostraci´ on. Por CR de σgc y por estar a{1 ← b} en σgc -f.n.

83

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

Teorema 101. [Simulaci´ on] Sean w, v ∈ (Λσgc )nf , entonces w →β 0 v =⇒ w λσgc v En particular,

a, b ∈ ΛDB a →β b =⇒ a λσgc b

Demostraci´ on. Por inducci´ on en w • w = 1, n, id, ↑n : se satisface vacuamente. • w=ab – v = a0 b

con a →β 0 a0 h. i.

a  λσgc a0 =⇒ a b λσgc a0 b – v = a b0

con b →β 0 b0 h. i.

b  λσgc b0 =⇒ a b λσgc a b0 – a = λc

v = c{1 ← b}

(λc) b →Beta c[b · id] σgc σgc (c[b · id]) =Coro 100 c{1 ← b} • w = λa

v = λa0

con a →β 0 a0 h. i.

a  λσgc a0 =⇒ λa λσgc λa0 • w =a·s – v = a0 · s

con a →β 0 a0 h. i.

a  λσgc a0 =⇒ a · s λσgc a0 · s – v = a · s0

con s →β 0 s0 h. i.

s  λσgc s0 =⇒ a · s λσgc a · s0

6.2

Correcci´ on y confluencia de λσgc

En la presente secci´ on mostraremos que el c´alculo λσgc cumple la propiedad de Correcci´ on (tambi´en conocida como Soundness), es decir, para w, v ∈ (Λσgc )nf , entonces w λσgc v =⇒ w β 0 v y concluiremos probando que se cumple la propiedad de confluencia para λσgc , mediante el lema de interpretaci´on.

84

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

t s Lema 102. Sean a ∈ Λσgc , s ∈ Λσgc , entonces

σgc ((λa)[s]) = σgc (λa[1 · (s◦ ↑)]) Demostraci´ on. • s p. (λa): es trivial. • s p\. (λa): Por lema 82 sabemos que existe c tal que (λa)[s]  c  λa[1 · (s◦ ↑)] Entonces, por CR de σgc , debe ocurrir que su forma normal sea la misma.

t s Lema 103. Sean a, b ∈ Λσgc , s ∈ Λσgc , entonces

σgc ((a b)[s]) = σgc (a[s]) σgc (b[s]) Demostraci´ on. Por CR de σgc y aplicaci´on de GC o alg´ un App. t s Lema 104. Sean a, b ∈ Λσgc , s ∈ Λσgc , entonces

σgc (a[1 · (s◦ ↑)][b · id]) = σgc (a[b · s]) Demostraci´ on. Separamos en casos: • 1 · (s◦ ↑) p. a: Notar que 1 ∈ FV(a[1 · (s◦ ↑)]), entonces b · id p. a[1 · (s◦ ↑)] – (1 · (s◦ ↑)) ◦ (b · id) p. a a[1 · (s◦ ↑)][b · id]

→Clos

a[(1 · (s◦ ↑)) ◦ (b · id)]

→Map

a[1[b · id] · ((s◦ ↑) ◦ (b · id))]

→VarCons

a[b · ((s◦ ↑) ◦ (b · id))]

→Ass

a[b · (s ◦ (↑ ◦(b · id)))]

→ShiftCons IdR

a[b · (s ◦ id)] a[b · s]

– (1 · (s◦ ↑)) ◦ (b · id) p\. a: Notar que |(1 · (s◦ ↑)) ◦ (b · id)| = |b · s| Luego, a[1 · (s◦ ↑)][b · id] →ClosGC a

←GC

a[b · s]

• 1 · (s◦ ↑) p\. a: – FV(a) = ∅: a[1 · (s◦ ↑)][b · id] →GC a[b · id] →GC a 85

←GC

a[b · s]

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

– FV(a) 6= ∅: |s| = (m, m) |1 · (s◦ ↑)| = (m + 1, m + 1)

(∀i ∈ FV(a)) i > m + 1

Luego |b · s| = (m + 1, m) a[1 · (s◦ ↑)][b · id] →GC a[b · id] Como, por lema 70, (∀i ∈ FV(a)) i[b · id]



i−1

(∀i ∈ FV(a)) i[b · s]



i−1

y Por lema 86 es cierto σgc (a[b · id]) = σgc (a[b · s])

t s Lema 105. Sean a, b ∈ Λσgc , s ∈ Λσgc , entonces

σgc (a[b[s] · s]) = σgc (a[b · id][s]) Demostraci´ on. Separamos en casos: • b · id p. a – s p. a[b · id] ∗ (b · id) ◦ s p. a a[b · id][s]

→Clos

a[(b · id) ◦ s]

→Map o MapGC

a[b0 · (id ◦ s)]

→IdL

a[b0 · s]

Con b0 = b[s] o b0 = b seg´ un si s p. b o s p\. b. Luego, σgc (a[b[s] · s]) = σgc (a[b · id][s]) ∗ (b · id) ◦ s p\. a Como |(b · id) ◦ s| = |b[s] · s| a[b · id][s] →ClosGC a

←GC

a[b[s] · s]

– s p\. a[b · id] ∗ FV(a[b · id]) = ∅: FV(a[b · id]) = (FV(a)>1 + 0 − 1) ∪ FV(b) = ∅ =⇒ (∀i ∈ FV(a)) i ≤ 1 ∧ FV(b) = ∅

86

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

Como b·id p. a, entonces FV(a) 6= ∅. Luego FV(a) = {1}. Vemos que para la u ´nica variable libre de a ambas sustituciones convergen a un mismo t´ermino, para concluir por lema 86 que ambos t´erminos convergen. 1[b · id][s] →VarCons b[s]

←VarCons

1[b[s] · s]

Luego por lema 86, entonces σgc (a[b[s] · s]) = σgc (a[b · id][s]) ∗ FV(a[b · id]) 6= ∅: Sea |s| = (m, m) |b[s] · s| = (m + 1, m) FV(a[b · id]) = (FV(a)>1 + 0 − 1) ∪ FV(b) Luego, (∀i ∈ FV(a[b · id])) i > m =⇒ (∀i ∈ FV(a)>1 ) i − 1 > m Luego, sea i ∈ FV(a) · i = 1: 1[b[s] · s] →VarCons b[s]

←VarCons

1[b · id][s]

· i > 1: Es cierto que i > m + 1, luego por lema 70 i[b[s] · s]



i−1



(i − 1)[s]



i[b · id][s]

Por lema 86 es cierto σgc (a[b[s] · s]) = σgc (a[b · id][s]) • b · id p\. a: S´ olo puede ocurrir si FV(a) = ∅. Luego a[b · id][s] →GC a[s] →GC a

←GC

a[b[s] · s]

t s Observaci´ on 106. Sea a ∈ Λσgc , s, t ∈ Λσgc , entonces

σgc ((a · s) ◦ t) = σgc (a[t] · (s ◦ t)) Demostraci´ on. Se aplica Map o MapGC en el t´ermino de la izquierda, y si corresponde GC en el de la derecha. s Lema 107. Sean a, b ∈ ΛDB , t, u, s ∈ (Λσgc )nf , entonces

1. a →β 0 b =⇒ σgc (a[s]) →β 0 σgc (b[s]) 2. t →β 0 u =⇒ σgc (t ◦ s) →β 0 σgc (u ◦ s) Demostraci´ on. 87

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

1. Inducci´ on en a: • a = 1, n • a = λc

se satisface vacuamente. c → β 0 c0

b = λc0

σgc ((λc)[s])

=L 102

σgc (λc[1 · (s◦ ↑)])

=L 87

λσgc (c[1 · (s◦ ↑)])

=L 87

λσgc (σgc (c)[σgc (1 · (s◦ ↑))])

=

λσgc (c[σgc (1 · (s◦ ↑))])

h.i. →β 0

λσgc (c0 [σgc (1 · (s◦ ↑))]) λσgc (σgc (c0 )[σgc (1 · (s◦ ↑))])

= =L 87

λσgc (c0 [1 · (s◦ ↑)])

=L 87

σgc (λc0 [1 · (s◦ ↑)])

=L 102

σgc ((λc0 )[s])

• a = a1 a2 – a1 →β 0 a01

b = a01 a2

σgc ((a1 a2 )[s])

– a2 →β 0 a02

σgc (a1 [s]) σgc (a2 [s])

→β 0 h.i.

σgc (a01 [s]) σgc (a2 [s])

=L 103

σgc (a01 [s] a2 [s])

=L 103

σgc (a1 [s]) σgc (a2 [s])

→β 0 h.i.

σgc (a1 [s]) σgc (a02 [s])

=L 103

σgc (a1 [s] a02 [s])

b = a1 a02

σgc ((a1 a2 )[s])

– a1 = λc

=L 103

b = c{1 ← a2 }

σgc (((λc) a2 )[s])

=L 103

σgc ((λc)[s]) σgc (a2 [s])

=L 102

σgc (λc[1 · (s◦ ↑)]) σgc (a2 [s])

=L 87

λσgc (c[1 · (s◦ ↑)]) σgc (a2 [s])

→β 0

σgc (c[1 · (s◦ ↑)]){1 ← σgc (a2 [s])}

=Coro 100

σgc (σgc (c[1 · (s◦ ↑)])[σgc (a2 [s]) · id])

=L 87

σgc (c[1 · (s◦ ↑)][a2 [s] · id])

=L 104

σgc (c[a2 [s] · s])

=L 105

σgc (c[a2 · id][s])

=L 87

σgc (σgc (c[a2 · id])[s])

=Coro 100

σgc ((c{1 ← a2 })[s])

2. Inducci´ on en t: • t = id, ↑n

se satisface vacuamente.

• t = a · t1 88

6.2 Correcci´ on y confluencia de λσgc

– a →β 0 a0

Confluencia de λσgc

u = a0 · t1 σgc (t ◦ s)

=Obs 106 =L 87

σgc (a[s]) · σgc (t1 ◦ s)

→β 0 item 1

σgc (a0 [s]) · σgc (t1 ◦ s)

=L 87

– t1 →β 0 t01

σgc (a[s] · (t1 ◦ s))

σgc (a0 [s] · (t1 ◦ s))

=Obs 106

σgc (u ◦ s)

=Obs 106

σgc (a[s] · (t1 ◦ s))

u = a · t01 σgc (t ◦ s)

=L 87

σgc (a[s]) · σgc (t1 ◦ s)

→β 0 h. i.

σgc (a[s]) · σgc (t01 ◦ s)

=L 87 =Obs 106

σgc (a[s] · (t01 ◦ s)) σgc (u ◦ s)

s )nf , entonces Corolario 108. Sean a, b ∈ ΛDB , t, u, s ∈ (Λσgc

1. a β 0 b =⇒ σgc (a[s]) β 0 σgc (b[s]) 2. t β 0 u =⇒ σgc (t ◦ s) β 0 σgc (u ◦ s) Demostraci´ on. Por inducci´ on en la longitud de la derivaci´on. s )nf , con s →β 0 t, entonces Lema 109. Sean a ∈ ΛDB , t, u, s ∈ (Λσgc

1. σgc (a[s]) β 0 σgc (a[t]) 2. σgc (u ◦ s) β 0 σgc (u ◦ t) t = a1 ·. . .·a0i ·. . .·ak · ↑n

Demostraci´ on. s = a1 ·. . .·ai ·. . .·ak · ↑n

con ai →β 0 a0i

1. Inducci´ on en a. Notar que i ≥ 1, pues si no no existir´ıa un redex. • a=1 – i=1 σgc (1[s]) = a1 →β 0 a01 = σgc (1[t]) – i>1 σgc (1[s]) = a1 = σgc (1[t]) • a=m>1 – m≤k

i=m σgc (1[↑m−1 ][s]) = ai →β 0 a0i = σgc (1[↑m−1 ][t])

– m≤k

i 6= m σgc (1[↑m−1 ][s]) = am = σgc (1[↑m−1 ][t])

89

6.2 Correcci´ on y confluencia de λσgc

Confluencia de λσgc

– m>k σgc (1[↑m−1 ][s]) = n + m − k = σgc (1[↑m−1 ][t]) • a=bc σgc ((b c)[s])

=L 103

σgc (b[s]) σgc (c[s])

β 0

σgc (b[t]) σgc (c[t])

h.i.

=L 103

σgc ((b c)[t])

• a = λb σgc ((λb)[s])

=L 102

σgc (λb[1 · (s◦ ↑)])

=L 87

λσgc (b[1 · (s◦ ↑)])

=L 87

λσgc (σgc (b)[σgc (1 · (s◦ ↑))])

=

λσgc (b[σgc (1 · (s◦ ↑))])

=L 87

λσgc (b[1 · (σgc (s◦ ↑))])

L 107+h.i. β 0

λσgc (b[1 · (σgc (t◦ ↑))])

=L 87

λσgc (b[1 · (t◦ ↑)])

=L 102

σgc ((λb)[t])

2. Inducci´ on en u: • u = id σgc (id ◦ s) = s →β 0 t = σgc (id ◦ t) • u =↑m – mm σgc (↑m ◦s) = am+1 ·. . .·ai ·. . .·ak · ↑n →β 0 am+1 ·. . .·a0i ·. . .·ak · ↑n = σgc (↑m ◦t) – m0 ) (∃C) si ◦ si+1  C[si+1 ◦ si+2 ] obteniendo as´ı la derivaci´ on infinita. En λσgc , en vez de aplicar Map como primer paso, se aplica MapGC, puesto que para i > 1, |si | = (0, 0). Luego, la derivaci´on ser´a s1 ◦ s2

=

(((λa) b) · id) ◦ s2

→MapGC

((λa) b) · (id ◦ s2 )

→Beta + IdL

a[b · id] · s2

En el ap´endice C se muestra un programa que obtiene la prueba para T ∈ SN λσgc mediante el an´ alisis exhaustivo de todas las derivaciones posibles.

8.2

?

?

Problema abierto: SN λσ ⊂ SN λσgc ⊃ SN λ

Si se estableciera que todo t´ermino fuertemente normalizante de λσ es SN en λσgc , entonces se tendr´ıa que, efectivamente, λσgc se encuentra “m´as cerca” de preservar la normalizaci´ on fuerte que λσ. La figura 8.1 muestra gr´aficamente esto. Sea λσ + GC el c´ alculo resultante de agregar la regla GC a λσ. Se puede ver que todo t´ermino SN de este c´alculo es SN en λσgc , puesto que la funci´on identidad es una funci´ on estricta de λσ + GC a λσgc (ver cap´ıtulo 3). Luego, quedar´ıa por ver que todo t´ermino SN de λσ es SN en λσ +GC. Cabe mencionar que esto no es cierto si se quita la condici´on de la regla GC, como lo muestra el siguiente ejemplo: (1 1)[↑][(λ1 1) · id] Si se eliminara la sustituci´ on [↑], queda la versi´on `a la λσ de Ω. Notar que este t´ermino efectivamente es SN. Por u ´ltimo, quedar´ıa por establecer si con la definici´on de “basura” presentada en este trabajo se logra efectivamente la preservaci´on de la normalizaci´on fuerte. Si as´ı fuera, y suponiendo lo expuesto anteriormente, la relaci´on entre 98

?

?

8.2 Problema abierto: SN λσ ⊂ SN λσgc ⊃ SN λ

λσgc y PSN

SN λ SN λσgc

SN λσ

Figura 8.1: Relaci´ on hipot´etica entre los t´erminos fuertemente normalizantes de λ, λσ, y λσgc los conjuntos de t´erminos fuertemente normalizantes quedar´ıa establecida como en la figura 8.2. Cabe mencionar aqu´ı que antes del cierre de este trabajo se cre´ıa que λσgc no cumpl´ıa PSN. Para ello se presentaba un t´ermino tipable con una supuesta derivaci´ on infinita. Para esta demostraci´on se introdujo el sistema tipado (cap´ıtulo 7). En la construcci´on de dicha derivaci´on infinita se encontr´ o un error, que no fue posible subsanar. En el estudio en profundidad de las derivaciones de este t´ermino se observ´o que, aunque restrictiva, la definici´on de “basura” aqu´ı presentada reduce considerablemente la cantidad de pasos de reducci´ on. Las complicaciones que pueden surgir para establecer PSN son: 1. Si bien λσgc toma ideas de λes, la traducci´on entre uno y otro no es inmediata (ver la diferencia entre la basura en uno y otro c´alculo que se brinda en la secci´ on 2.1). Esto no permite establecer PSN por medio de una traducci´ on entre estos c´alculos. Pruebas basadas en la traducci´on entre dos c´ alculos se muestran en, por ejemplo, [Kes07] y [KR95]. 2. No tenemos conocimiento de un c´alculo con sustituciones m´ ultiples que cumpla esta propiedad, y habr´ıa que estudiar con cuidado si las pruebas realizadas para c´ alculos con sustituciones simples pueden ser extendidas para contemplar este caso. Por ejemplo, Bloo y Geuvers idean una t´ecnica en [BG97] que permite establecer PSN para λx, λs, y λυ, mediante la traducci´ on a un c´ alculo con labels, pero sustituciones simples.

99

?

?

8.2 Problema abierto: SN λσ ⊂ SN λσgc ⊃ SN λ

λσgc y PSN

SN λ SN λσgc

SN λσ

Figura 8.2: Relaci´ on hipot´etica entre los t´erminos fuertemente normalizantes de λ, λσ, y λσgc , si λσgc preservara la normalizaci´on fuerte.

100

Cap´ıtulo 9

Conclusiones En este trabajo hemos presentado un conjunto de herramientas te´oricas para comprender y refinar el concepto de basura en un c´alculo como λσ. Primero, en la subsecci´ on 1.4.3, se mostr´o una forma precisa de obtener las variables libres de un t´ermino. Luego, en la secci´on 2.1 se di´o un caracterizaci´on a la basura, aunque se mostr´ o que tal caracterizaci´on era limitada, en tanto que no toda substituci´ on que es basura en λx es basura en λσgc . A´ un as´ı, se mostr´ o en 8.1 que existen t´erminos que no pertenecen a SN λσ pero s´ı a SN λσgc , demostrando la eficacia de colectar las substituciones basura. Adem´ as, en el cap´ıtulo 4 se estableci´o una forma original de mostrar la confluencia, mostrando que si para toda variable libre i del t´ermino a vale i[s]  bi  i[t] para dos sustituciones s y t, entonces vale a[s]  c  a[t]. A continuaci´ on presentamos distintos problemas que podr´ıan constituir una extensi´ on del presente trabajo.

9.1

Generalizaci´ on de lemas a λσ

En el cap´ıtulo 4 presentamos distintos lemas aplicables a λσgc . El estudio de las condiciones bajo las cuales estos lemas podr´ıan generalizarse a λσ brindar´ıa una valiosa base te´ orica para futuros trabajos relacionados con este c´alculo. Como ejemplo, el lema 75 podr´ıa ser u ´til en el estudio de la confluencia de extensiones a λσ, tal como lo ha sido en λσgc (cap´ıtulo 5).

9.2

Confluencia en t´ erminos puros

λσgc no cumple la propiedad de confluencia en t´erminos abiertos. Esto se demuestra con el mismo contraejemplo del teorema 34: a[b[s] · s]  ((λa) b)[s]  a[b[s] · (s ◦ id)] En λσ, para cerrar este par cr´ıtico hay que agregar la regla (IdR)

s ◦ id

−→

s

que trae consigo nuevos pares cr´ıticos. En [Rio93] se presenta un c´alculo denominado λσSP , que agrega la regla IdR y otras reglas derivadas de los pares 101

9.3 Acercamiento a λes

Conclusiones

cr´ıticos que se van formando. Si bien no vale MC para t´erminos y sustituciones con metavariables, s´ı vale MC para t´erminos puros, es decir, con metavariables en los t´erminos y no en las sustituciones. En λσgc , agregar esta regla no genera nuevos pares cr´ıticos que no se puedan cerrar, con lo que quedar´ıa ver si el sistema λσgc + IdR es WCR en t´erminos puros. Para ello es necesario determinar cuando una sustituci´on afecta o no un t´ermino, con lo que es necesario conocer de antemano las variables libres de los t´erminos. Para ello, puede utilizarse la t´ecnica utilizada en [Kes07], donde las metavariables son anotadas con un conjunto de variables, que representan las variables libres de la metavariable. Luego, restar´ıa ver que los lemas utilizados en la prueba de WCR de σgc siguen valiendo para t´erminos puros. Cabe destacar que si se agregan los lemas 78 y 80 como reglas al c´alculo, se generan infinitos nuevos pares cr´ıticos, con lo que no es una posibilidad.

9.3

Acercamiento a λes

Como se mencion´ o en la secci´on 2.1, otras variantes de la definici´on de “basura” pueden ser estudiadas, con el objetivo de obtener una versi´on similar a la definida por λes.

9.4

λsgc : Garbage collection para λs

En [KR95] se presenta un c´alculo con sustituciones expl´ıcitas e ´ındices de de Bruijn, que resulta de incorporar la metasustituci´on de λDB como reglas del c´ alculo, de igual forma que lo hace λx para λ. Podr´ıa estudiarse si una versi´on con garbage collection permite una extensi´on que cumpla PSN y MC. Para ello, podr´ıa extenderse el operador ϕij para que permita a i ser 0, para conseguir que ϕ00 (a) sea reducir en 1 todos los ´ındices de a. Luego, la regla GC quedar´ıa como (GC)

aσ i b

−→

ϕ00 (b)

102

(si i 6∈ FV(a))

Ap´ endice A

Demostraciones para λσ En este cap´ıtulo se demuestra el lema 122, necesario para demostrar el lema 47. Para ello, son necesarios algunos lemas adicionales. Tomamos la definici´ on de [Rio93]: Definici´ on 117. Sean i ≥ 0, n ≥ 1, se define si n como si n = 1 · 2 · . . . · i· ↑i+n−1

s0 n =↑n−1

s0 1 = id

Lema 118. 1 · (si n ◦ ↑) σ si+1 n Demostraci´ on. La demostraci´ on es muy simple y se encuentra en [Rio93]. Lema 119. Para todo t´ermino a en σ-f.n., a[si 1 ] σ a. En particular, a[id]  a Demostraci´ on. Por inducci´ on en el t´ermino: • a = 1: – i = 0: 1[id] →VarId 1 – i > 0: 1[1 · . . . · i· ↑i ] →VarCons 1 • a = 1[↑k ]: 1[↑k ][si 1 ] →Clos 1[↑k ◦si 1 ] Separamos seg´ un k e i. Los detalles de estos pasos se pueden ver en [Rio93]. – Si k < i, 1[↑k ◦si 1 ] = 1[↑k ◦(1·. . .·i· ↑i )] σ 1[k+1·. . .·i· ↑i ] →VarCons k+1 = 1[↑k ] – Si k ≥ i, 1[↑k ◦si 1 ] = 1[↑k ◦(1 · . . . · i· ↑i )] σ 1[↑i+k−i ] = 1[↑k ] • a = b c: (b c)[si 1 ] →App b[si 1 ] c[si 1 ] h.i. b c • a = λb: (λb)[si 1 ]

→Abs L 118 h.i. 103

λb[1 · (si 1 ◦ ↑)] λb[si+1 1 ] λb

Demostraciones para λσ

Lema 120. Sea s una sustituci´on tal que |s| = (m, n). Por lema 68, existen t´erminos a1 , . . . , am tales que σ(s) = a1 · ... · am · ↑n

∨ σ(s) = id

Sea i una variable. 1. Si i > m, entonces σ(i[s]) = i + n − m. 2. Si i ≤ m, entonces σ(i[s]) = ai . Demostraci´ on. Parte de esta prueba se encuentra en [Rio93], pero la repetimos aqu´ı por claridad. Por confluencia de σ se tiene que σ(i[s]) = σ(σ(i)[σ(s)]) = σ(i[σ(s)]) Tomamos la σ-f. n. de s y separamos en casos: • Si σ(s) = id, por lema 119, i[id] σ i. • Si i = 1, 1. Si 1 > m, entonces m = 0 y σ(s) =↑n . 1[↑n ] est´a en forma normal, y corresponde a 1 + n − m 2. Si 1 ≤ m, entonces i[a1 · ... · am · ↑n ] →VarCons a1 y est´a en σ-f.n. • Si i = 1[↑i−1 ] 1[↑i−1 ][σ(s)]

→Clos =

1[(↑ ◦(↑ ◦(...(↑ ◦ ↑)...))) ◦ σ(s)]

→Ass

1[↑ ◦((↑ ◦(...(↑ ◦ ↑)...)) ◦ σ(s))]

→Assi−2 = 1.(i > m) 2.(i ≤ m)

1[↑i−1 ◦σ(s)]

1[↑ ◦(↑ ◦(...(↑ ◦(↑ ◦σ(s)))...))] 1[↑ ◦(↑ ◦(...(↑ ◦(↑ ◦(a1 · ... · am · ↑n )))...))]

→ShiftConsm

1[↑i−1−m ◦ ↑n ]

→Assi−1−m

1[↑i+n−m−1 ] = i + n − m

→ShiftConsi−1 →VarShift

1[ai · ... · am ↑n ] ai

Lema 121. Sea a un t´ermino en σ-f. n., y sea s una sustituci´on. Si (∀i ∈ FV(a)) σ(i[s]) = i entonces a[s]  a. Demostraci´ on. Por estar a en σ-f.n. basta con mostrar que σ(a[s]) = a. Se demuestra por inducci´ on en la σ-f. n. de a:

104

Demostraciones para λσ

• Caso a = i: Por hip´ otesis vale. • Caso a = a1 a2 : Como FV(ai ) ⊆ FV(a) para i ∈ {1, 2}, vale por h.i. que ai [s]  ai . Luego, (a1 a2 )[s] →App a1 [s] a2 [s] h.i. a1 a2 • Caso a = λb: Sea s0 = σ(s) – Si s0 = id, entonces (λb)[s]  (λb)[id] L 119 λb – Si s0 = a1 · ... · am · ↑n , con |s| = (m, n), (λb)[s]  (λb)[s0 ] →Abs λb[1 · (s0 ◦ ↑)] Luego, λb[1 · ((a1 · ... · am · ↑n )◦ ↑)]

Map

λb[1 · a1 [↑] · ... · am [↑]· ↑n+1 ]

Sea s00 = σ(1 · a1 [↑] · ... · am [↑]· ↑n+1 ) = 1 · a01 · ... · a0m · ↑n+1 para a0i = σ(ai [↑]). Por hip´ otesis, sabemos que si i ∈ FV(a), σ(i[s]) = i. Por definici´on de FV, para i > 1, i ∈ FV(λb) ⇔ i + 1 ∈ FV(b). Luego puede ocurrir ∗ Si i + 1 ≤ m + 1, por lema 120 σ((i + 1)[1 · (s0 ◦ ↑)]) = σ((i + 1)[s00 ]) = a0i Por lema 120 nuevamente, σ(i[s]) = i[a1 · ... · am · ↑n ] = ai Por hip´ otesis, σ(i[s]) = i, con lo que ai = i (pues ai est´a en σ-f.n. y σ es CR). Luego, a0i = σ(ai [↑]) = σ(i[↑]) = i + 1 ∗ Si i + 1 > m + 1, por lema 120 σ((i + 1)[1 · (s0 ◦ ↑)]) = i + 1 + (n + 1) − (m + 1) Como i > m, por lema 120 nuevamente, σ(i[s]) = i + n − m Por hip´ otesis, σ(i[s]) = i, luego, por ser σ CR, n = m. Con lo que queda σ((i + 1)[s00 ]) = i + 1 + (n + 1) − (m + 1) = i + 1 En ambos casos, queda σ((i + 1)[1 · (s◦ ↑)]) = i + 1. Si 1 ∈ FV(b), σ(1[1 · (s◦ ↑)]) = 1. Luego, (∀i ∈ FV(b)) σ(i[1 · (s◦ ↑)]) = i, con lo que se puede aplicar h. i. Luego, λb[1 · (s◦ ↑)]  λb 105

Demostraciones para λσ

Lema 122. Sean s una sustituci´on y a un t´ermino en σ-f.n., s p\. λa =⇒ λa[1 · (s◦ ↑)]  λa Demostraci´ on. Sean: |s| = (m, n)

t0 = σ(1 · (s◦ ↑))

Vamos a ver que (∀i ∈ FV(a)) σ(i[t0 ]) = i Para concluir por lema 121 que λa[1 · (s◦ ↑)]  λa Notar que t0 = 1 · σ(s◦ ↑) Por definici´ on de p\. , tenemos dos casos: • FV(λa) = ∅: Como FV(λa) = FV(a) \ 1 = ∅, se pueden dar dos casos: – FV(a) = ∅: Se puede aplicar el lema 121 de forma trivial. – FV(a) = {1}: Mostramos que se aplican las hip´otesis del lema 121. Como 1[t0 ] →VarCons 1 se tiene que (∀i ∈ FV(a)) σ(i[t0 ]) = i • FV(λa) 6= ∅: Entonces m = n y (∀i ∈ FV(λa)) i > m. Luego, como |1 · (s◦ ↑)| = (m + 1, m + 1), para toda variable i ∈ FV(a) tenemos si i > 1

=⇒

i > m + 1 ∧ σ(i[t0 ]) =L 120 i

si i = 1

=⇒

1[1 · (s◦ ↑)] →VarCons 1

Luego, (∀i ∈ FV(a)) σ(i[t0 ]) = i En todos los casos se puede aplicar el lema 121, luego λa[1 · (s◦ ↑)]  λa

106

Ap´ endice B

Programa int´ erprete de λσ en Prolog En este ap´endice mostraremos un simple int´erprete de λσ realizado en Prolog. El predicado contraejemplo busca ocurrencias del t´ermino a = 1[↑ ◦ ↑ ][1[↑] · id] en todas las posibles derivaciones del t´ermino a[s], con s = 1· ↑. Este predicado no se cumple, como muestra la siguiente salida de Prolog ?- [sigma]. % sigma compiled 0.01 sec, 736 bytes Yes ?- contraejemplo. No De esta forma se concluye que no siempre para un t´ermino a y una sustituci´on s, a[s] σ a. a ( s u s t ( s u s t ( one , c l o s ( s h i f t , s ( c o n s ( one ,

s h i f t ) ) , c o n s ( s u s t ( one ,

shift )) .

c o n t r a e j e m p l o :− a (A) , s ( S ) , s t e p s ( s u s t (A, S ) , A) . s t e p ( app (A, B) , app (C, B) ) :− s t e p (A, C) . s t e p ( app (A, B) , app (A, C) ) :− s t e p (B, C) . s t e p ( abs (A) , abs (B) ) :− s t e p (A, B) . s t e p ( s u s t (A, S ) , s u s t (B, S ) ) :− s t e p (A, B) . s t e p ( s u s t (A, S ) , s u s t (A, T) ) :− s t e p ( S , T) . s t e p ( c o n s (A, S ) , c o n s (B, S ) ) :− s t e p (A, B) . s t e p ( c o n s (A, S ) , c o n s (A, T) ) :− s t e p ( S , T) . s t e p ( c l o s ( S , T) , c l o s (U, T) ) :− s t e p ( S , U) . s t e p ( c l o s ( S , T) , c l o s ( S , U) ) :− s t e p (T, U) . % beta s t e p ( app ( abs (X) , Y) , s u s t (X, c o n s (Y, i d ) ) ) .

107

s h i f t ) , id ) ) ) .

Programa int´erprete de λσ en Prolog

% varid s t e p ( s u s t ( one , i d ) , one ) . % varcons s t e p ( s u s t ( one , c o n s (A, ) ) , A) . % app s t e p ( s u s t ( app (A, B) , S ) , app ( s u s t (A, S ) , s u s t (B, S ) ) ) . % abs s t e p ( s u s t ( abs (A) , S ) , abs ( s u s t (A, c o n s ( one , c l o s ( S ,

shift ))))) .

% clos s t e p ( s u s t ( s u s t (A, S ) , T) , s u s t (A, c l o s ( S , T) ) ) . % idl s t e p ( c l o s ( id , S ) , S ) . % shiftid step ( clos ( shift , id ) , s h i f t ) . % shiftcons step ( c l o s ( s h i f t , cons ( , S) ) , S) . % map s t e p ( c l o s ( c o n s (A, S ) , T) , c o n s ( s u s t (A, T) , c l o s ( S , T) ) ) . % ass s t e p ( c l o s ( c l o s ( S , T) , U) , c l o s ( S , c l o s (T, U) ) ) . s t e p s (A, B) :− s t e p (A, C) , s t e p s (C, B) . s t e p s (A, B) :− s t e p (A, B) .

Listing B.1: Archivo sigma.pl

108

Ap´ endice C

Programa int´ erprete de λσgc en Java En este ap´endice mostraremos un simple int´erprete de λσgc realizado en Java. El siguiente archivo muestra la ejecuci´on para el contraejemplo de M`ellies: package s ig m ag c ; import j a v a . u t i l . L i n k e d L i s t ; import j a v a . u t i l . Queue ; public c l a s s R e c u r s i v e E x e c u t o r { private Sigmagc si gm a gc ; public R e c u r s i v e E x e c u t o r ( ) { s ig m ag c = new Sigmagc ( ) ; } public long e x e c u t e ( Term long i = 0 ; Queue l i s t = new s ig m ag c . addAllT ( l i s t , f o r ( Term term : l i s t ) i += e x e c u t e ( term ) + } return i ; } public Term Term Term

t) { L i n k e d L i s t () ; t); { 1;

s t a t i c void main ( S t r i n g [ ] a r g s ) { appId1 = Terms . app ( Terms . idFunc ( ) , Terms . one ) ; appIdAppId1 = Terms . app ( Terms . idFunc ( ) , appId1 ) ; m e l l i e s = Terms . abs ( Terms . app ( Terms . abs ( appIdAppId1 ) , appId1 . c l o n e ( ) ) ) ;

R e c u r s i v e E x e c u t o r l p e = new R e c u r s i v e E x e c u t o r ( ) ; long i = l p e . e x e c u t e ( m e l l i e s ) ; System . out . p r i n t l n ( ” M e l l i e s t i e n e ” + i + ” t e r m i n o s ” ) ; } }

109

Programa int´erprete de λσgc en Java

Listing C.1: Archivo RecursiveExecutor.java El siguiente archivo contiene la l´ogica de ejecuci´on de las reglas de λσgc : package s ig m ag c ; import import import import

java . java . java . java .

util util util util

. HashSet ; . LinkedList ; . Queue ; . Set ;

public c l a s s Sigmagc { public boolean a f e c t a ( Term t , S u s t s ) { int [ ] peso = s . getPeso ( ) ; Set f v = f v ( t ) ; return f v . s i z e ( ) > 0 && ( p e s o [ 0 ] != p e s o [ 1 ] | | e x i s t s L E ( fv , p e s o [ 0 ] ) ) ; }

private boolean e x i s t s L E ( Set v a r s , i n t i ) { for ( I n t e g e r var : vars ) { i f ( v a r 1) { newSet . add ( var −1) ; } } return newSet ; } e l s e i f ( t instanceof App) { App ap = (App) t ; Set f v 1 = f v ( ap . t 1 ) ; Set f v 2 = f v ( ap . t 2 ) ; fv1 . addAll ( fv2 ) ; return f v 1 ; } e l s e i f ( t instanceof TSust ) { TSust t s = ( TSust ) t ; Set f v t = f v ( t s . t ) ; Set f v s = f v ( t s . s ) ; int [ ] p = t s . s . getPeso ( ) ;

110

Programa int´erprete de λσgc en Java

for ( I n t e g e r var : f v t ) { i f ( var > p [ 0 ] ) { f v s . add ( v a r + p [ 1 ] − p [ 0 ] ) ; } } return f v s ; } else { throw new E r r o r ( ” no d e b e r i a s u c e d e r ” ) ; } } public Set f v ( S u s t s ) { i f ( s instanceof I d ) { return new HashSet() ; } e l s e i f ( s instanceof S h i f t ) { return new HashSet() ; } e l s e i f ( s instanceof Cons ) { Cons c = ( Cons ) s ; Set l i s t = f v ( c . t ) ; l i s t . addAll ( fv ( c . s ) ) ; return l i s t ; } e l s e i f ( s instanceof C l o s ) { Clos c = ( Clos ) s ; Set f v t = f v ( c . s 1 ) ; Set f v s = f v ( c . s 2 ) ; int [ ] p = c . s2 . getPeso ( ) ; for ( I n t e g e r var : f v t ) { i f ( var > p [ 0 ] ) { f v s . add ( v a r + p [ 1 ] − p [ 0 ] ) ; } } return f v s ; } else { throw new E r r o r ( ” no d e b e r i a s u c e d e r ” ) ; } }

public void addAllT ( Queue l i s t , Term curTerm ) { i f ( curTerm instanceof One ) { return ; } Term t 1 = a p p l y B e t a ( curTerm ) ; i f ( t 1 != n u l l ) { l i s t . add ( t 1 . c l o n e ( ) ) ; } Term t 2 = applyGc ( curTerm ) ; i f ( t 2 != n u l l ) { l i s t . add ( t 2 . c l o n e ( ) ) ; } Term t 3 = applyVarCons ( curTerm ) ;

111

Programa int´erprete de λσgc en Java

i f ( t 3 != n u l l ) { l i s t . add ( t 3 . c l o n e ( ) ) ; } Term t 4 = applyApp1 ( curTerm ) ; i f ( t 4 != n u l l ) { l i s t . add ( t 4 . c l o n e ( ) ) ; } Term t 5 = applyApp2 ( curTerm ) ; i f ( t 5 != n u l l ) { l i s t . add ( t 5 . c l o n e ( ) ) ; } Term t 6 = applyApp3 ( curTerm ) ; i f ( t 6 != n u l l ) { l i s t . add ( t 6 . c l o n e ( ) ) ; } Term t 7 = applyAbs ( curTerm ) ; i f ( t 7 != n u l l ) { l i s t . add ( t 7 . c l o n e ( ) ) ; } Term t 8 = a p p l y C l o s ( curTerm ) ; i f ( t 8 != n u l l ) { l i s t . add ( t 8 . c l o n e ( ) ) ; } Term t 9 = applyClosGC ( curTerm ) ; i f ( t 9 != n u l l ) { l i s t . add ( t 9 . c l o n e ( ) ) ; } i f ( curTerm instanceof App) { App ap = (App) curTerm ; L i n k e d L i s t l 1 = new L i n k e d L i s t () ; L i n k e d L i s t l 2 = new L i n k e d L i s t () ; addAllT ( l 1 , ap . t 1 ) ; addAllT ( l 2 , ap . t 2 ) ; f o r ( Term s t 1 : l 1 ) { l i s t . add ( Terms . app ( s t 1 , ap . t 2 ) ) ; } f o r ( Term s t 2 : l 2 ) { l i s t . add ( Terms . app ( ap . t1 , s t 2 ) ) ; } } e l s e i f ( curTerm instanceof Abs ) { Abs ab = ( Abs ) curTerm ; L i n k e d L i s t l 1 = new L i n k e d L i s t () ; addAllT ( l 1 , ab . t ) ; for ( Object s t 1 : l 1 ) { l i s t . add ( Terms . abs ( ( Term ) s t 1 ) ) ; } } e l s e i f ( curTerm instanceof TSust ) { TSust t s = ( TSust ) curTerm ; L i n k e d L i s t l 1 = new L i n k e d L i s t () ; L i n k e d L i s t l 2 = new L i n k e d L i s t () ; addAllT ( l 1 , t s . t ) ; addAllS ( l 2 , t s . s ) ; f o r ( Term s t 1 : l 1 ) {

112

Programa int´erprete de λσgc en Java

l i s t . add ( Terms . s u s t ( s t 1 , t s . s ) ) ; } for ( Sust s t 2 : l 2 ) { l i s t . add ( Terms . s u s t ( t s . t , s t 2 ) ) ; } } } public void addAllS ( Queue l i s t , S u s t c u r S u s t ) { i f ( c u r S u s t instanceof I d | | c u r S u s t instanceof S h i f t ) { return ; } S u s t s 1 = ap pl yI dL ( c u r S u s t ) ; i f ( s 1 != n u l l ) { l i s t . add ( s 1 . c l o n e ( ) ) ; } Sust s2 = a p p l y S h i f t I d ( curSust ) ; i f ( s 2 != n u l l ) { l i s t . add ( s 2 . c l o n e ( ) ) ; } Sust s3 = applyShiftCons ( curSust ) ; i f ( s 3 != n u l l ) { l i s t . add ( s 3 . c l o n e ( ) ) ; } S u s t s 4 = applyMap ( c u r S u s t ) ; i f ( s 4 != n u l l ) { l i s t . add ( s 4 . c l o n e ( ) ) ; } S u s t s 5 = applyMapGc ( c u r S u s t ) ; i f ( s 5 != n u l l ) { l i s t . add ( s 5 . c l o n e ( ) ) ; } S u s t s 6 = a pp l y A s s ( c u r S u s t ) ; i f ( s 6 != n u l l ) { l i s t . add ( s 6 . c l o n e ( ) ) ; } i f ( c u r S u s t instanceof Cons ) { Cons co = ( Cons ) c u r S u s t ; L i n k e d L i s t l 1 = new L i n k e d L i s t () ; L i n k e d L i s t l 2 = new L i n k e d L i s t () ; addAllT ( l 1 , co . t ) ; addAllS ( l 2 , co . s ) ; f o r ( Term s t 1 : l 1 ) { l i s t . add ( Terms . c o n s ( s t 1 , co . s ) ) ; } for ( Sust s t 2 : l 2 ) { l i s t . add ( Terms . c o n s ( co . t , s t 2 ) ) ; } } e l s e i f ( c u r S u s t instanceof C l o s ) { Clos c l = ( Clos ) curSust ; L i n k e d L i s t l 1 = new L i n k e d L i s t () ; L i n k e d L i s t l 2 = new L i n k e d L i s t () ; addAllS ( l 1 , c l . s 1 ) ; addAllS ( l 2 , c l . s 2 ) ;

113

Programa int´erprete de λσgc en Java

for ( Sust s t 1 : l 1 ) { l i s t . add ( Terms . c l o s ( s t 1 , c l . s 2 ) ) ; } for ( Sust s t 2 : l 2 ) { l i s t . add ( Terms . c l o s ( c l . s1 , s t 2 ) ) ; } } } public Term a p p l y B e t a ( Term t ) { i f ( ! ( t instanceof App) ) { return n u l l ; } App ap = (App) t ; i f ( ! ( ap . t 1 instanceof Abs ) ) { return n u l l ; } Abs t 1 = ( Abs ) ap . t 1 ; Term t 2 = ap . t 2 ; Term tp = t 1 . t ; S u s t s = Terms . c o n s ( t2 , Terms . i d ) ; return Terms . s u s t ( tp , s ) ; } public Term applyGc ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; if ( afecta ( ts . t , ts . s ) ) { return n u l l ; } return t s . t ; } public Term applyVarCons ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof One ) | | ! ( t s . s instanceof Cons ) ) { return n u l l ; } Cons co = ( Cons ) t s . s ; return co . t ; } public Term applyApp1 ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof App) ) { return n u l l ; } App ap = (App) t s . t ; i f ( ! a f e c t a ( ap . t1 , t s . s ) | | ! a f e c t a ( ap . t2 , t s . s ) ) { return n u l l ; } return Terms . app ( Terms . s u s t ( ap . t1 , t s . s ) , Terms . s u s t ( ap . t2 , t s .

114

Programa int´erprete de λσgc en Java

s)); } public Term applyApp2 ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof App) ) { return n u l l ; } App ap = (App) t s . t ; i f ( ! a f e c t a ( ap . t1 , t s . s ) | | a f e c t a ( ap . t2 , t s . s ) ) { return n u l l ; } return Terms . app ( Terms . s u s t ( ap . t1 , t s . s ) , ap . t 2 ) ; } public Term applyApp3 ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof App) ) { return n u l l ; } App ap = (App) t s . t ; i f ( a f e c t a ( ap . t1 , t s . s ) | | ! a f e c t a ( ap . t2 , t s . s ) ) { return n u l l ; } return Terms . app ( ap . t1 , Terms . s u s t ( ap . t2 , t s . s ) ) ; } public Term applyAbs ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof Abs ) ) { return n u l l ; } Abs ab = ( Abs ) t s . t ; if

( ! a f e c t a ( ab , t s . s ) ) { return n u l l ;

} return Terms . abs ( Terms . s u s t ( ab . t , Terms . c o n s ( Terms . one , Terms . c l o s ( t s . s , Terms . s h i f t ) ) ) ) ; } public Term a p p l y C l o s ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof TSust ) ) { return n u l l ; } TSust i n n e r T s = ( TSust ) t s . t ; Term term = i n n e r T s . t ;

115

Programa int´erprete de λσgc en Java

if

( ! a f e c t a ( term , i n n e r T s . s ) | | return n u l l ;

! afecta ( ts . t , ts . s ) ) {

} S u s t s u s t = Terms . c l o s ( i n n e r T s . s , t s . s ) ; i f ( ! a f e c t a ( term , s u s t ) ) { return n u l l ; } return Terms . s u s t ( term , s u s t ) ; } public Term applyClosGC ( Term t ) { i f ( ! ( t instanceof TSust ) ) { return n u l l ; } TSust t s = ( TSust ) t ; i f ( ! ( t s . t instanceof TSust ) ) { return n u l l ; } TSust i n n e r T s = ( TSust ) t s . t ; Term term = i n n e r T s . t ; i f ( ! a f e c t a ( term , i n n e r T s . s ) | | ! a f e c t a ( t s . t , t s . s ) ) { return n u l l ; } S u s t s u s t = Terms . c l o s ( i n n e r T s . s , t s . s ) ; i f ( a f e c t a ( term , s u s t ) ) { return n u l l ; } return term ; } public S u s t ap pl yI d L ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ; i f ( ! ( c l . s 1 instanceof I d ) ) { return n u l l ; } return c l . s 2 ; } public S u s t a p p l y S h i f t I d ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ; i f ( ! ( c l . s 1 instanceof S h i f t ) ) { return n u l l ; } i f ( ! ( c l . s 2 instanceof I d ) ) { return n u l l ; } return Terms . s h i f t ; } public S u s t a p p l y S h i f t C o n s ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ;

116

Programa int´erprete de λσgc en Java

if } if

( ! ( c l . s 1 instanceof S h i f t ) ) { return n u l l ; ( ! ( c l . s 2 instanceof Cons ) ) { return n u l l ;

} Cons co = ( Cons ) c l . s 2 ; return co . s ; } public S u s t applyMap ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ; i f ( ! ( c l . s 1 instanceof Cons ) ) { return n u l l ; } Cons co = ( Cons ) c l . s 1 ; i f ( ! a f e c t a ( co . t , c l . s 2 ) ) { return n u l l ; } return Terms . c o n s ( Terms . s u s t ( co . t , c l . s 2 ) , Terms . c l o s ( co . s , c l . s2 ) ) ; } public S u s t applyMapGc ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ; i f ( ! ( c l . s 1 instanceof Cons ) ) { return n u l l ; } Cons co = ( Cons ) c l . s 1 ; i f ( a f e c t a ( co . t , c l . s 2 ) ) { return n u l l ; } return Terms . c o n s ( co . t , Terms . c l o s ( co . s , c l . s 2 ) ) ; } public S u s t a p pl y A s s ( S u s t s ) { i f ( ! ( s instanceof C l o s ) ) { return n u l l ; } Clos c l = ( Clos ) s ; i f ( ! ( c l . s 1 instanceof C l o s ) ) { return n u l l ; } Clos c l 2 = ( Clos ) c l . s1 ; return Terms . c l o s ( c l 2 . s1 , Terms . c l o s ( c l 2 . s2 , c l . s 2 ) ) ; } }

Listing C.2: Archivo Sigmagc.java Los archivos que se listan a continuaci´on sontienen la estructura de t´erminos y sustituciones: package s ig m ag c ; import j a v a . i o . S e r i a l i z a b l e ;

117

Programa int´erprete de λσgc en Java

public abstract c l a s s Term implements S e r i a l i z a b l e { public abstract Term c l o n e ( ) ; public abstract boolean e q u a l s ( O b j e c t o b j ) ; }

Listing C.3: Archivo Term.java package s ig m ag c ;

public c l a s s One extends Term { public Term c l o n e ( ) { return Terms . one ; } public boolean e q u a l s ( O b j e c t o b j ) { return o b j instanceof One ; } }

Listing C.4: Archivo One.java package s ig m ag c ; public c l a s s Abs extends Term { public Term t ; public Abs ( Term toAbs ) { t = toAbs ; } public Term c l o n e ( ) { return new Abs ( t . c l o n e ( ) ) ; } public boolean e q u a l s ( O b j e c t o b j ) { return o b j instanceof Abs && t . e q u a l s ( ( ( Abs ) o b j ) . t ) ; } }

Listing C.5: Archivo Abs.java package s ig m ag c ; public c l a s s App extends Term { public Term t 1 ; public Term t 2 ; public App( Term l , Term r ) { t1 = l ; t2 = r ; } public Term c l o n e ( ) { return new App( t 1 . c l o n e ( ) , t 2 . c l o n e ( ) ) ; }

118

Programa int´erprete de λσgc en Java

public boolean e q u a l s ( O b j e c t o b j ) { i f ( o b j instanceof App) { App app = (App) o b j ; return t 1 . e q u a l s ( app . t 1 ) && t 2 . e q u a l s ( app . t 2 ) ; } return f a l s e ; } }

Listing C.6: Archivo App.java package s ig m ag c ; public c l a s s TSust extends Term { public Term t ; public S u s t s ; public TSust ( Term t , S u s t s ) { this . t = t ; this . s = s ; } public Term c l o n e ( ) { return new TSust ( t . c l o n e ( ) , s . c l o n e ( ) ) ; } public boolean e q u a l s ( O b j e c t o b j ) { i f ( o b j instanceof TSust ) { TSust t s u s t = ( TSust ) o b j ; return t . e q u a l s ( t s u s t . t ) && s . e q u a l s ( t s u s t . s ) ; } return f a l s e ; } }

Listing C.7: Archivo TSust.java package s ig m ag c ; import j a v a . i o . S e r i a l i z a b l e ; public abstract c l a s s S u s t implements S e r i a l i z a b l e { protected i n t [ ] p e s o ; public S u s t ( ) { p e s o = new i n t [ 2 ] ; } public abstract i n t [ ] g e t P e s o ( ) ; public abstract S u s t c l o n e ( ) ; public abstract boolean e q u a l s ( O b j e c t o ) ; }

Listing C.8: Archivo Sust.java package s ig m ag c ;

119

Programa int´erprete de λσgc en Java

public c l a s s I d extends S u s t { public I d ( ) { peso [ 0 ] = 0 ; peso [ 1 ] = 0 ; } public i n t [ ] g e t P e s o ( ) { return p e s o ; } public S u s t c l o n e ( ) { return Terms . i d ; } public boolean e q u a l s ( O b j e c t o b j ) { return o b j instanceof I d ; } }

Listing C.9: Archivo Id.java package s ig m ag c ; public c l a s s S h i f t extends S u s t { public S h i f t ( ) { peso [ 0 ] = 0 ; peso [ 1 ] = 1 ; } public i n t [ ] g e t P e s o ( ) { return p e s o ; } public S u s t c l o n e ( ) { return Terms . s h i f t ; } public boolean e q u a l s ( O b j e c t o b j ) { return o b j instanceof S h i f t ; } }

Listing C.10: Archivo Shift.java package s ig m ag c ; public c l a s s Cons extends S u s t { public Term t ; public S u s t s ; public Cons ( Term term , S u s t s u s t ) { t = term ; s = sust ; } public i n t [ ] g e t P e s o ( ) { i n t [ ] pesoS = s . g e t P e s o ( ) ; p e s o [ 0 ] = pesoS [ 0 ] + 1 ;

120

Programa int´erprete de λσgc en Java

p e s o [ 1 ] = pesoS [ 1 ] ; return p e s o ; } public S u s t c l o n e ( ) { return new Cons ( t . c l o n e ( ) , s . c l o n e ( ) ) ; } public boolean e q u a l s ( O b j e c t o b j ) { i f ( o b j instanceof Cons ) { Cons c o n s = ( Cons ) o b j ; return t . e q u a l s ( c o n s . t ) && s . e q u a l s ( c o n s . s ) ; } return f a l s e ; } }

Listing C.11: Archivo Cons.java package s ig m ag c ; public c l a s s C l o s extends S u s t { public S u s t s 1 ; public S u s t s 2 ; public C l o s ( S u s t s1 , S u s t s 2 ) { this . s1 = s1 ; this . s2 = s2 ; } public i n t [ ] g e t P e s o ( ) { i n t [ ] p1 = s 1 . g e t P e s o ( ) ; i n t [ ] p2 = s 2 . g e t P e s o ( ) ; i f ( p1 [ 1 ] peso [ 0 ] peso [ 1 ] } else { peso [ 0 ] peso [ 1 ] }