Implementación de la transformación SKI

Necesito implementar el siguiente algoritmo para convertir Cálculo Lambda en Lógica Combinatoria.

Las reglas son de https://en.wikipedia.org/wiki/Combinatorylogic#CompletenessoftheS-K_basis

T[x] => x T[(E₁ E₂)] => (T[E₁] T[E₂]) T[λx.E] => (K T[E]) (si x no aparece libre en E) T[λx.x] => I T[λx.λy.E] => T[λx.T[λy.E]] (si x aparece libre en E) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (si x aparece libre en E₁ o E₂)

Esto es lo que tengo hasta ahora:

data CLExpr = S | K | I | CLVar Int | CLApp CLExpr CLExpr data LamExpr = LamApp LamExpr LamExpr | LamAbs Int LamExpr | LamVar Int skiTransform :: LamExpr -> CLExpr skiTransform (LamVar x) = CLVar x -- Regla 1 skiTransform (LamAbs y (s)) | (free y s == False) = K (skiTransform(s)) -- Regla 3 skiTransform (LamAbs x (LamVar y)) | x == y = I -- Regla 4 skiTransform (LamAbs x (LamAbs y (s))) | (free x s) = skiTransform (LamAbs x (skiTransform (LamAbs y (s)))) -- Regla 5 free :: Int -> LamExpr -> Bool free x (LamVar y) = x == y free x (LamAbs y e) | x == y = False free x (LamAbs y e) | x /= y = free x e free x (LamApp e f) = (free x e) || (free x f)

El problema que tengo es, en la regla 5, cómo “anidar” mis funciones de transformación como se muestra en la parte superior. La transformación interna crea el tipo CLExpr, que luego no se puede usar como entrada para la transformación externa.

Tampoco estoy seguro de cómo implementar las reglas 2 y 6, que requieren separar dos expresiones una al lado de la otra, pero eso no es una prioridad todavía.

¡Gracias!

davy.ai

July 30, 2023 at 2:18 am

Para implementar la regla 5, se puede definir una función auxiliar que tome la expresión LamAbs y devuelva la transformación de CLExpr, así como el conjunto de variables ligadas. De esta manera, se puede utilizar la expresión transformada como entrada para la transformación externa y al mismo tiempo llevar un registro de las variables ligadas.

skiTransform :: LamExpr -> CLExpr
skiTransform (LamVar x) = CLVar x --Regla 1

skiTransform (LamAbs y s)
    | not (free y s) = CLApp K (skiTransform s) --Regla 3
    | otherwise = let (cl, bound) = skiTransform' (LamAbs y s) in
                      skiTransform (LamAbs y cl)

skiTransform (LamAbs x (LamVar y))
    | x == y = I --Regla 4

skiTransform (LamApp e@(LamAbs x _) f)
    | free x f = skiTransform (LamAbs x (LamApp e f)) --Regla 5
    | otherwise = CLApp S (skiTransform e) (skiTransform f)

skiTransform (LamApp e f) = CLApp (skiTransform e) (skiTransform f)

skiTransform' :: LamExpr -> (CLExpr, [Int])
skiTransform' (LamAbs x s) =
    let (cl, bound) = skiTransform' s in
        if x `elem` bound then
            let x' = freshVar bound in
                (CLAbs x' cl, x':bound)
        else
            (CLAbs x cl, x:bound)
skiTransform' e = (skiTransform e, [])

Para las reglas 2 y 6, se puede utilizar el patrón coincidente en skiTransform para separar las expresiones antes de aplicar la transformación de forma recursiva. Por ejemplo:

skiTransform (LamApp e1@(LamApp _ _) e2) = 
    CLApp (skiTransform $ LamApp e1' e2) e1''
    where (e1', e1'') = disassemble e1

Aquí, disassemble es una función auxiliar que devuelve las dos subexpresiones de una expresión de aplicación, de modo que se pueda aplicar la transformación a cada una por separado antes de combinarlas nuevamente utilizando CLApp.

Con estas modificaciones, tu función skiTransform debería manejar todas las seis reglas de transformación.

Answer

davy.ai

July 30, 2023 at 2:18 am
Para implementar la regla 5, se puede definir una función auxiliar que tome la expresión LamAbs y devuelva la transformación de CLExpr, así como el conjunto de variables ligadas. De esta manera, se puede utilizar la expresión transformada como entrada para la transformación externa y al mismo tiempo llevar un registro de las variables ligadas.
```
skiTransform :: LamExpr -> CLExpr
skiTransform (LamVar x) = CLVar x --Regla 1

skiTransform (LamAbs y s)
    | not (free y s) = CLApp K (skiTransform s) --Regla 3
    | otherwise = let (cl, bound) = skiTransform' (LamAbs y s) in
                      skiTransform (LamAbs y cl)

skiTransform (LamAbs x (LamVar y))
    | x == y = I --Regla 4

skiTransform (LamApp e@(LamAbs x _) f)
    | free x f = skiTransform (LamAbs x (LamApp e f)) --Regla 5
    | otherwise = CLApp S (skiTransform e) (skiTransform f)

skiTransform (LamApp e f) = CLApp (skiTransform e) (skiTransform f)

skiTransform' :: LamExpr -> (CLExpr, [Int])
skiTransform' (LamAbs x s) =
    let (cl, bound) = skiTransform' s in
        if x `elem` bound then
            let x' = freshVar bound in
                (CLAbs x' cl, x':bound)
        else
            (CLAbs x cl, x:bound)
skiTransform' e = (skiTransform e, [])
```
Para las reglas 2 y 6, se puede utilizar el patrón coincidente en skiTransform para separar las expresiones antes de aplicar la transformación de forma recursiva. Por ejemplo:
```
skiTransform (LamApp e1@(LamApp _ _) e2) = 
    CLApp (skiTransform $ LamApp e1' e2) e1''
    where (e1', e1'') = disassemble e1
```
Aquí, disassemble es una función auxiliar que devuelve las dos subexpresiones de una expresión de aplicación, de modo que se pueda aplicar la transformación a cada una por separado antes de combinarlas nuevamente utilizando CLApp.

Con estas modificaciones, tu función skiTransform debería manejar todas las seis reglas de transformación.

Comments are closed.

es.davy.ai

¿Tienes una pregunta?

Implementación de la transformación SKI

Answer

davy.ai