i'm trying to write in Haskell the WHILE language from my Theory of Programming subject. Everything was being defined recursively at first, so code was flowing. Then we reached statements, and derivation trees appeared, even though i could still transform that into recursive definitions. Until we got into the OR and PAR statements.
The 2 big-step axioms for the OR statement: (S1 OR S2)
- If < S1, s> -> s' then < S1 OR S2, s> -> s'
- If < S2, s> -> s' then < S1 OR S2, s> -> s'
The 2 small-step axioms for the OR statement:
- < S1 OR S2 , s > => < S1 , s > - < S1 OR S2 , s > => < S2 , s >
where S1 and S2 are Statements and s, s' are functions Var -> Int
Apparently a good way to achieve this behaviour is randomize which of S1 or S2 gets executed when we run S1 OR S2 . Luckily i began my monad research months ago, reaching already the System.Random module and the State monad (monad Transformers are still unknown for me), so i can imagine some approaches (which i dislike)
- Get some "random" seed from both S1 and S2, something like (length . show), and passing that to System.Random . But i know that going that way leads to always choosing the same statement from S1 OR S2 when both S1 and S2 are fixed.
- Define new data (something like SpecialSTM) for the OR and PAR statements, so i can change the types of my functions (mainly semanticaSTM) to add some IO and real randomness .
So, is there a solution allowing me to keep the types just as they are now, but get some reasonable behaviour in the OR and PAR statements?
Here is all my code:
module WhileV4
(
-- La sintaxis:
Bin(Cero, Uno)
, Entero(N1,N2)
, AritVar(Avar)
, BoolVar(Bvar)
, Aexpr(A1,A2,Sum,Mult,Rest)
, Bexpr(Verdadero,Falso,Iguales,Distintos,MayorOigual,MenorOigual,Mayor,Menor,NO,Y,O,Entonces,Sii)
, Stm(AssA,AssB,Skip,Comp,Si,Mientras,Repetir)
-- La semantica:
, semanticaN
, semanticaA
, semanticaB
, freeAV
, freeAV'
, freeBV
, subsA
, subsA'
, subsB
, newStateA
, newStateB
, semanticaSTM
-- Otros:
, mkEnt -- para crear Enteros a partir de cadenas de 0s y 1s
, (.:) -- sinonimo infijo de Comp (otra opcion, usar la clase Monoid --> TO DO)
, (>+)
, (>*)
, (>-)
, (=:) -- asignacion para variables aritmeticas, sinonimo infijo
, (==:) -- asignacion para variables booleanas, sinonimo infijo
, (=.=)
, (=/=)
, (<.=)
, (>.=)
, factorial
, euclides
) where
import Data.Char (digitToInt)
import qualified Data.Set as S
import Control.Applicative
import Data.Maybe
----------------------------------------------------------
-- TEMA 1
----------------------------------------------------------
-- Comparando con lo visto en clase:
-- Num ~ Entero , Var ~ AritVar , Aexp ~ Aexpr , Bexp ~ Bexpr , Stm ~ Stm
-- Los constructores de cada expresion tienen distinta notacion para evitar interferencias con Haskell.
-- Faltan las BoolVar (se dejan como ejercicio en clase).
-- N ~ semanticaN , State ~ Astate , A ~ semanticaA
-- Definiciones de "definicion composicional" e "induccion estructural".
-- Observacion sobre la semantica de (-a)
-- Ej 1.8: Demostrar que las ecuaciones para A definen una funcion total.
-- Visto en clase: N es funcion total
-- B ~ semanticaB
-- Ej 1.10: Demostrar que las ecuaciones para B definen una funcion total.
-- Ej 1.11: (a) Se extiende Bexp a Bexp'; extender la funcion semantica B (ya implementado)
-- (b) Demostrar que para cada b' en Bexp' existe b en Bexp tal que b' y b son equivalentes.
-- FV ~ freeAV
-- Lema 1: Sean s,s' en State tales que para todo x en FV(a), s x == s' x => A[[a]]s == A[[a]]s'
-- Ej 1.13: Definir el conjunto de variables libres para una expresion booleana y demostrar un resultado similar al Lema 1.
-- ERROR: freeBV no es lo que pide el ejercicio 13 (pide freeAV')
-- substitucion ~ subsA , actualizar estado ~ newStateA
-- Ej 1.14: Demostrar que A[[ a[y->a0] ]]s = A[[a]](s[y->A[[a0]]s]) para cualquier estado s.
-- Ej 1.15: Definir la substitucion de expresiones booleanas b[y->a0] y demostrar un resultado similar al del ejercicio anterior.
data Bin = Cero | Uno
deriving Show
-- Para hacerlo como en clase:
-- data Entero = N1 Bin | N2 Entero Bin
-- pero podria hacerlo con listas que total tambien son recursivas
-- newtype Entero = N [Bin]
-- pero me toca las narices la lista vacia asi que voy a hacerlo como en clase
data Entero = N1 Bin | N2 Entero Bin
deriving Show
semanticaN :: Entero -> Int
semanticaN (N1 Cero) = 0
semanticaN (N1 Uno) = 1
semanticaN (N2 n Cero) = 2 * semanticaN n
semanticaN (N2 n Uno) = (2 * semanticaN n) + 1
data AritVar = Avar String
deriving (Eq, Ord, Show)
data BoolVar = Bvar String
deriving (Eq, Ord, Show)
-- el Ord lo necesito para hacer uniones de (Set AritVar) y (Set BoolVar)
data Aexpr = A1 Entero | A2 AritVar | Sum Aexpr Aexpr | Mult Aexpr Aexpr | Rest Aexpr Aexpr
data Bexpr = Verdadero | Falso | Iguales Aexpr Aexpr | Distintos Aexpr Aexpr | MayorOigual Aexpr Aexpr | MenorOigual Aexpr Aexpr | Mayor Aexpr Aexpr | Menor Aexpr Aexpr
| NO Bexpr | Y Bexpr Bexpr | O Bexpr Bexpr | Entonces Bexpr Bexpr | Sii Bexpr Bexpr | B BoolVar -- Bvar String
data Stm = AssA AritVar Aexpr | AssB BoolVar Bexpr | Skip | Comp Stm Stm | Si Bexpr Stm Stm | Mientras Bexpr Stm | Repetir Stm Bexpr
| Abortar | Asegurar Bexpr Stm | Or Stm Stm | Par Stm Stm
| Iniciar Dec
semanticaA :: Aexpr -> (AritVar -> Int) -> Int
semanticaA (A1 ent) s = semanticaN ent
semanticaA (A2 var) s = s var
semanticaA (Sum a1 a2) s = (semanticaA a1 s) + (semanticaA a2 s)
semanticaA (Mult a1 a2) s = (semanticaA a1 s) * (semanticaA a2 s)
semanticaA (Rest a1 a2) s = (semanticaA a1 s) - (semanticaA a2 s)
semanticaB :: Bexpr -> (AritVar -> Int) -> (BoolVar -> Bool) -> Bool
semanticaB Verdadero _ _ = True
semanticaB Falso _ _ = False
semanticaB (Iguales a1 a2) s _ = (semanticaA a1 s) == semanticaA a2 s
semanticaB (Distintos a1 a2) s _ = (semanticaA a1 s) /= semanticaA a2 s
semanticaB (MayorOigual a1 a2) s _ = (semanticaA a1 s) >= semanticaA a2 s
semanticaB (MenorOigual a1 a2) s _ = (semanticaA a1 s) <= semanticaA a2 s
semanticaB (Mayor a1 a2) s _ = (semanticaA a1 s) > semanticaA a2 s
semanticaB (Menor a1 a2) s _ = (semanticaA a1 s) < semanticaA a2 s
semanticaB (B boolvar) s1 s2 = s2 boolvar
semanticaB (NO bexpr) s1 s2 = not (semanticaB bexpr s1 s2)
semanticaB (Y b1 b2) s1 s2 = (semanticaB b1 s1 s2) && (semanticaB b2 s1 s2)
semanticaB (O b1 b2) s1 s2 = (semanticaB b1 s1 s2) || (semanticaB b2 s1 s2)
semanticaB (Entonces b1 b2) s1 s2 = semanticaB (NO (b1 `Y` (NO b2))) s1 s2
semanticaB (Sii b1 b2) s1 s2 = (semanticaB b1 s1 s2) == (semanticaB b2 s1 s2)
freeAV :: Aexpr -> S.Set AritVar
freeAV (A1 _) = S.empty
freeAV (A2 avar) = S.singleton avar
freeAV (Sum a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV (Mult a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV (Rest a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' :: Bexpr -> S.Set AritVar
freeAV' Verdadero = S.empty
freeAV' Falso = S.empty
freeAV' (Iguales a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (Distintos a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (MayorOigual a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (MenorOigual a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (Mayor a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (Menor a1 a2) = (freeAV a1) `S.union` (freeAV a2)
freeAV' (B boolvar) = S.empty
freeAV' (NO bexpr) = freeAV' bexpr
freeAV' (Y b1 b2) = (freeAV' b1) `S.union` (freeAV' b2)
freeAV' (O b1 b2) = (freeAV' b1) `S.union` (freeAV' b2)
freeAV' (Entonces b1 b2) = (freeAV' b1) `S.union` (freeAV' b2)
freeAV' (Sii b1 b2) = (freeAV' b1) `S.union` (freeAV' b2)
freeBV :: Bexpr -> S.Set BoolVar
freeBV Verdadero = S.empty
freeBV Falso = S.empty
freeBV (Iguales a1 a2) = S.empty
freeBV (Distintos a1 a2) = S.empty
freeBV (MayorOigual a1 a2) = S.empty
freeBV (MenorOigual a1 a2) = S.empty
freeBV (Mayor a1 a2) = S.empty
freeBV (Menor a1 a2) = S.empty
freeBV (B boolvar) = S.singleton boolvar
freeBV (NO bexpr) = freeBV bexpr
freeBV (Y b1 b2) = (freeBV b1) `S.union` (freeBV b2)
freeBV (O b1 b2) = (freeBV b1) `S.union` (freeBV b2)
freeBV (Entonces b1 b2) = (freeBV b1) `S.union` (freeBV b2)
freeBV (Sii b1 b2) = (freeBV b1) `S.union` (freeBV b2)
subsA :: Aexpr -> AritVar -> Aexpr -> Aexpr
subsA (A1 ent) _ _ = (A1 ent)
subsA (A2 avar) v a = if avar == v then a else (A2 avar)
subsA (Sum a1 a2) v a = Sum (subsA a1 v a) (subsA a2 v a)
subsA (Mult a1 a2) v a = Mult (subsA a1 v a) (subsA a2 v a)
subsA (Rest a1 a2) v a = Rest (subsA a1 v a) (subsA a2 v a)
subsA' :: Bexpr -> AritVar -> Aexpr -> Bexpr
subsA' Verdadero _ _ = Verdadero
subsA' Falso _ _ = Falso
subsA' (Iguales a1 a2) v a = Iguales (subsA a1 v a) (subsA a2 v a)
subsA' (Distintos a1 a2) v a = Distintos (subsA a1 v a) (subsA a2 v a)
subsA' (MayorOigual a1 a2) v a = MayorOigual (subsA a1 v a) (subsA a2 v a)
subsA' (MenorOigual a1 a2) v a = MenorOigual (subsA a1 v a) (subsA a2 v a)
subsA' (Mayor a1 a2) v a = Mayor (subsA a1 v a) (subsA a2 v a)
subsA' (Menor a1 a2) v a = Menor (subsA a1 v a) (subsA a2 v a)
subsA' (B boolvar) v a = (B boolvar)
subsA' (NO bexpr) v a = NO (subsA' bexpr v a)
subsA' (Y b1 b2) v a = (subsA' b1 v a) `Y` (subsA' b2 v a)
subsA' (O b1 b2) v a = (subsA' b1 v a) `O` (subsA' b2 v a)
subsA' (Entonces b1 b2) v a = (subsA' b1 v a) `Entonces` (subsA' b2 v a)
subsA' (Sii b1 b2) v a = (subsA' b1 v a) `Sii` (subsA' b2 v a)
subsB :: Bexpr -> BoolVar -> Bexpr -> Bexpr
subsB Verdadero _ _ = Verdadero
subsB Falso _ _ = Falso
subsB b@(Iguales a1 a2) _ _ = b
subsB b@(Distintos a1 a2) _ _ = b
subsB b@(MayorOigual a1 a2) _ _ = b
subsB b@(MenorOigual a1 a2) _ _ = b
subsB b@(Mayor a1 a2) _ _ = b
subsB b@(Menor a1 a2) _ _ = b
subsB (B boolvar) v b = if boolvar == v then b else (B boolvar)
subsB (NO bexpr) v b = NO (subsB bexpr v b)
subsB (Y b1 b2) v b = (subsB b1 v b) `Y` (subsB b2 v b)
subsB (O b1 b2) v b = (subsB b1 v b) `O` (subsB b2 v b)
subsB (Entonces b1 b2) v b = (subsB b1 v b) `Entonces` (subsB b2 v b)
subsB (Sii b1 b2) v b = (subsB b1 v b) `Sii` (subsB b2 v b)
newStateA :: (AritVar -> Int) -> AritVar -> Int -> (AritVar -> Int)
newStateA s y n x = if x == y then n else (s x)
newStateB :: (BoolVar -> Bool) -> BoolVar -> Bool -> (BoolVar -> Bool)
newStateB s y b x = if x == y then b else (s x)
----------------------------------------------------------
-- TEMA 2
----------------------------------------------------------
-- Comparando con lo visto en clase:
-- configuracion ~ Config , transicion ~ Transicion
-- Defs: La ejecucion de una sentencia S en un estado s: (¬ terminar = ciclar)
-- termina sii existe un estado s' tal que <S,s> -> s'
-- cicla sii no existe ningun estado s' tal que <S,s> -> s'
-- Ej 2.4: Determinar si las sentencias terminan / ciclan (o no) siempre:
-- while ¬(x=1) do (y := y*x ; x := x-1)
-- while 1<=x do (y := y*x ; x := x-1)
-- while true do skip
-- Def: S1 equivale semanticamente a S2 sii para todo s en State, <S1,s> -> s' si y solo si <S2,s> -> s'
-- Lema 2: {while b do S} es semánticamente equivalente a {if b then (S; while b do S) else skip}
-- Ej 2.6:
-- Demostrar que (S1;S2);S3 y S1;(S2;S3) son semanticamente equivalentes
-- Demostrar que en general S1;S2 no es semanticamente equivalente a S2;S1
-- Ej 2.7: Extender el lenguaje While con la sentencia repeat S until b
-- Demostrar que {repeat S until b} es semanticamente equivalente a {S; if b then skip else (repeat S until b)}
type Astate = AritVar -> Int
type Bstate = BoolVar -> Bool
type Config = (Stm,Astate,Bstate)
type Transicion = Config -> (Astate,Bstate)
semanticaSTM :: Transicion
semanticaSTM (AssA x a, s1, s2) = let n = semanticaA a s1 in (newStateA s1 x n , s2)
semanticaSTM (AssB x b, s1, s2) = let n = semanticaB b s1 s2 in (s1 ,newStateB s2 x n)
semanticaSTM (Skip, s1, s2) = (s1,s2)
semanticaSTM (Comp stm1 stm2, s1, s2) = let (s1' , s2') = semanticaSTM (stm1,s1,s2) in semanticaSTM (stm2,s1',s2')
semanticaSTM (Si b stm1 stm2, s1, s2) = if semanticaB b s1 s2 then semanticaSTM (stm1,s1,s2) else semanticaSTM (stm2,s1,s2)
semanticaSTM (Mientras b stm, s1, s2) = if semanticaB b s1 s2 then aux else (s1,s2)
where aux = let (s1' , s2') = semanticaSTM (stm,s1,s2) in semanticaSTM (Mientras b stm, s1', s2')
semanticaSTM (Repetir stm b, s1, s2) = if semanticaB b s1 s2 then semanticaSTM (stm,s1,s2) else aux
where aux = let (s1' , s2') = semanticaSTM (stm,s1,s2) in semanticaSTM (Repetir stm b , s1', s2')
semanticaSTM (Abortar , s1, s2) = error "La ejecucion del programa ha sido interrumpida por Abortar"
semanticaSTM (Asegurar b stm, s1, s2) = if (semanticaB b s1 s2) then semanticaSTM (stm,s1,s2) else error ("La ejecucion del programa ha sido interrumpida porque no se puede asegurar la condicion " ++ show b)
-- semanticaSTM (Or stm1 stm2 , s1, s2) = ???
-- semanticaSTM (Par stm1 stm2, s1, s2) = ???
----------------------------------------------------------
-- TEMA 3
----------------------------------------------------------
data Dec = DvA (String,Aexpr) Dec | DvB (String,Bexpr) Dec | NoMasVariables
----------------------------------------------------------
-- COSAS EXTRA
----------------------------------------------------------
-- Sinonimos infijos:
(.:) :: Stm -> Stm -> Stm
stm1 .: stm2 = Comp stm1 stm2
(>+) :: Aexpr -> Aexpr -> Aexpr
a1 >+ a2 = Sum a1 a2
(>*) :: Aexpr -> Aexpr -> Aexpr
a1 >* a2 = Mult a1 a2
(>-) :: Aexpr -> Aexpr -> Aexpr
a1 >- a2 = Rest a1 a2
(=:) :: AritVar -> Aexpr -> Stm
avar =: a = avar `AssA` a
(==:) :: BoolVar -> Bexpr -> Stm
bvar ==: b = bvar `AssB` b
(=.=) :: Aexpr -> Aexpr -> Bexpr
a1 =.= a2 = Iguales a1 a2
(=/=) :: Aexpr -> Aexpr -> Bexpr
a1 =/= a2 = Distintos a1 a2
(<.=) :: Aexpr -> Aexpr -> Bexpr
a1 <.= a2 = MenorOigual a1 a2
(>.=) :: Aexpr -> Aexpr -> Bexpr
a1 >.= a2 = MayorOigual a1 a2
crearEntero :: [Int] -> Entero
crearEntero [] = error "No se puede crear un Entero con la lista vacia"
crearEntero (n:ns) = foldl f aux ns
where
f ent 0 = N2 ent Cero
f ent 1 = N2 ent Uno
aux = if (n == 0) then (N1 Cero) else (N1 Uno)
mkEnt :: String -> Entero
mkEnt = crearEntero . map digitToInt
{- PRUEBAS EN PANTALLA
*While> mkEnt "100"
N2 (N2 (N1 Uno) Cero) Cero
*While> semanticaN (mkEnt "100")
4
*While> semanticaN (mkEnt "112")
*** Exception: While.hs:(41,5)-(42,24): Non-exhaustive patterns in function f
-}
a1 = Sum (A2 (Avar "x")) (A1 (N1 Uno))
x = Avar "x"
y = Avar "y"
z = Avar "z"
m = Avar "m"
n = Avar "n"
n0 = (N1 Cero)
n1 = (N1 Uno)
n2 = mkEnt "10"
n3 = mkEnt "11"
n4 = mkEnt "100"
n5 = mkEnt "101"
n6 = mkEnt "110"
n7 = mkEnt "111"
n8 = mkEnt "1000"
n9 = mkEnt "1001"
n10 = mkEnt "1010"
n11 = mkEnt "1011"
a2 = Rest (Sum (A2 x) (A2 y)) (Mult (A2 z) (A1 n5))
m' = A2 m
n' = A2 n
factorial :: Stm
factorial = (y =: (A1 n1)) .: (Mientras (NO (Iguales (A2 x) (A1 n1))) ((y=:(Mult (A2 y) (A2 x))) .: (x=:(Rest (A2 x) (A1 n1)))))
stateA1 :: Astate
stateA1 (Avar "_") = 5
stateB1 :: Bstate
stateB1 _ = True
euclides :: Stm
euclides = Mientras (NO (m' =.= n')) (Si (m' <.= n') (n =: (n' >- m')) (m =: (m' >- n')))
stA1 :: Astate
stA1 (Avar x) = if x=="n" then 20 else (if x=="m" then 8 else 0)
probandoShow :: Stm
probandoShow = Si Verdadero euclides factorial
{- pruebas en pantalla:
*While> :t fst $ semanticaSTM (factorial, stateA1, stateB1)
fst $ semanticaSTM (factorial, stateA1, stateB1) :: Astate
*While> let aux = fst $ semanticaSTM (factorial, stateA1, stateB1) in map aux [x,y]
[1,120]
(0.03 secs, 7942288 bytes)
*While> let aux = fst $ semanticaSTM (factorial, const 16, stateB1) in map aux [x,y]
[1,20922789888000]
(0.02 secs, 0 bytes)
*While> product [1..16]
20922789888000
(0.00 secs, 0 bytes)
*While> let aux = fst $ semanticaSTM (factorial, const 20, stateB1) in map aux [x,y]
[1,2432902008176640000]
(0.02 secs, 0 bytes)
*While> let aux = fst $ semanticaSTM (factorial, const 21, stateB1) in map aux [x,y]
[1,-4249290049419214848]
(0.00 secs, 0 bytes)
*WhileV3> let aux = fst $ semanticaSTM (euclides, stA1, stateB1) in map aux [n,m]
[4,4]
-}
-- instance Eq Entero where
-- n1 == n2 = (semanticaN n1) == (semanticaN n2)
-- instance Ord Entero where
-- compare n1 n2 = compare (semanticaN n1) (semanticaN n2)
instance Show Aexpr where
show (A1 n) = (show . semanticaN) n
show (A2 (Avar x)) = x
show (Sum a1 a2) = '(' : (show a1) ++ " + " ++ (show a2) ++ ")"
show (Mult a1 a2) = '(' : (show a1) ++ " * " ++ (show a2) ++ ")"
show (Rest a1 a2) = '(' : (show a1) ++ " - " ++ (show a2) ++ ")"
instance Show Bexpr where
show Verdadero = "Verdadero"
show Falso = "Falso"
show (Iguales a1 a2) = '(' : (show a1) ++ " = " ++ (show a2) ++ ")"
show (Distintos a1 a2) = '(' : (show a1) ++ " /= " ++ (show a2) ++ ")"
show (MayorOigual a1 a2) = '(' : (show a1) ++ " >= " ++ (show a2) ++ ")"
show (MenorOigual a1 a2) = '(' : (show a1) ++ " <= " ++ (show a2) ++ ")"
show (Mayor a1 a2) = '(' : (show a1) ++ " > " ++ (show a2) ++ ")"
show (Menor a1 a2) = '(' : (show a1) ++ " < " ++ (show a2) ++ ")"
show (B (Bvar x)) = x
show (NO bexpr) = '(' : 'N' : 'o' : ' ' : (show bexpr) ++ ")"
show (Y b1 b2) = '(' : (show b1) ++ " Y " ++ (show b2) ++ ")"
show (O b1 b2) = '(' : (show b1) ++ " O " ++ (show b2) ++ ")"
show (Entonces b1 b2) = '(' : (show b1) ++ " => " ++ (show b2) ++ ")"
show (Sii b1 b2) = '(' : (show b1) ++ " <=> " ++ (show b2) ++ ")"
instance Show Stm where
show s = "\n" ++ showStm s 0 ++ "\n"
showStm :: Stm -> Int -> String
showStm s n = let esp k = take k (repeat ' ') in
case s of
(AssA (Avar x) a) -> (esp n) ++ "(" ++ x ++ " := " ++ (show a) ++ ")"
(AssB (Bvar y) b) -> (esp n) ++ "(" ++ y ++ " :== " ++ (show b) ++ ")"
Skip -> (esp n) ++ "No hacer nada"
(Comp s1 s2) -> (showStm s1 n) ++ "; \n" ++ (showStm s2 n)
(Si b s1 s2) -> (esp n) ++ "Si " ++ (show b) ++ "\n" ++ (esp $ n+2) ++ "entonces \n" ++ (showStm s1 (n+4)) ++ "\n" ++ (esp $ n+2) ++ "en otro caso \n" ++ (showStm s2 (n+4))
(Mientras b s) -> (esp n) ++ "Mientras se cumpla " ++ (show b) ++ " hacer \n" ++ (showStm s (n+4))
(Repetir s b) -> (esp n) ++ "Repetir " ++ "\n" ++ (showStm s (n+4)) ++ "\n" ++ (esp $ n+2) ++ "hasta que " ++ (show b)
Aucun commentaire:
Enregistrer un commentaire