Tarea 3

CC41A Lenguajes de Programación

Martes 1 Mayo

El siguiente problema deben ser enviado en un solo archivo de nombre abc3.sml (donde abc son las inciales de su nombre y dos apellidos; por ejemplo el archivo de José Fernández Herrera será jfh3.sml; el 3 es por tarea 3) en attachment a cgutierr@dcc.uchile.cl con subject abc3.sml. Si el archivo no compila directamente, la tarea tiene un 1.

Substitución

El problema consiste en escribir una función que sustituya una variable en un contexto considerando los posibles choques de nombres. Para esto usaremos el modelo de cálculo lambda.

 datatype Exp = 
	  V of string 
	| Apl of Exp * Exp 
	| Lambda of string * Exp;

Escriba una función sub de tipo Exp * string * Exp --> Exp que para un triple (M,x,N) devuelva M[N/x] según las siguientes especificaciones:

$$\begin{align*}x[N/x] &= N \\ y[N/x] &= y \;\;\; y \neq x \\ (P\; Q)[N/x] &= ... ...z. P[z/y])[N/x], \;\;\; y \neq x, \; z \notin Lib(N) \cup Lib(P) \end{align*}$$

$$\begin{align*}Lib(x) &= \{ x \} \\ Lib((M N)) &= Lib(M) \cup Lib(N) \\ Lib(\lambda x. N) &= Lib(N) - \{ x \}. \end{align*}$$