Problema 1

Enunciado

Definir por recursión sobre fórmulas las siguientes funciones

• nv(F) que calcula el número variables proposicionales que ocurren en la fórmula F. Por ejemplo,

  nv(p → p ∨ q) = 3.

• prof(F) que calcula la profundidad del árbol de análisis de la fórmula F. Por ejemplo,

  prof(p → p ∨ q) = 2.

Demostrar por inducción, que para toda fórmula F, nv(F) ≤ 2^prof(F)

Soluciones colaborativas

import Data.Char
--Pedro G. Ros

-- Primero definimos los operadores como tipo:

data F = Const Bool
           |Vari Char
           |Nega F
           |Conj F F
           |Impl F F

--Ahora las funciones:
nv:: F -> Int
nv (Vari a) = 1
nv (Impl a b) = (nv a) + (nv b)
nv (Nega p) = (nv p)
nv (Conj c d)= (nv c) + (nv d) 

-- *Main> nv (Impl (Vari 'p') (Conj (Vari 'p') (Vari 'q')))
-- 3

prof::F-> Int
prof (Vari a) = 0
prof (Impl a b) = 1 + (prof a) + (prof b)
prof (Nega b) = 1+ (prof b)
prof (Conj a b) = 1+ (prof a) + (prof b)

-- *Main> prof (Impl (Vari 'p') (Conj (Vari 'p') (Vari 'q')))
--2

{-
La demostración por inducción es sencilla:
Caso base:
nv (Vari a) = 1 <= 2^(prof (Vari a)) = 2^0 = 1

Supongamos cierta la hipótesis para m y n dos proposiciones, y pongamos los casos:

nv (Nega m) = (nv m) <= 1+ 2^(prof m)
y obviamente: prof (Nega m) = (prof m)<=  2^(prof m)

Ya que estamos practicando la inducción haré que 
n <= 2^n.
(i) Se cumple trivialmente en el 1.
(ii) Suponemos cierto que se cumple en n.
(iii) n<= 2^n ==> 2n<=2^(n+1), luego si (n+1)<=2n ya hemos acabado, cosa obvia si 1<=n.
 
nv (Impl m n) = (nv m) + (nv n) <= 2^(prof m) + 2^(prof n)
prof (Impl m n) = 1+ (prof m) + (prof n), y también es trivial ver que 2^(prof Impl m n) es una cota superior a la dada por la hipótesis de inducción.

nv (Conj m n) == nv (Impl m n)

Por lo que hemos acabado y queda demostrado para todo tipo de fórmula F.

-}

-- Reme Sillero

-- Mi definición de número de variables y de profundidad es prácticamente igual a la definida por mi compañero, pero he añadido más -- constructores que pienso que hacen falta.

-- Primero definimos todo lo necesario en cuanto a tipo y representación:

import Data.List

type SimboloProposicional = String

data Prop = Atom SimboloProposicional

         | Neg Prop 
         | Conj Prop Prop 
         | Disj Prop Prop 
         | Impl Prop Prop 
         | Equi Prop Prop 
         deriving (Eq,Ord)

instance Show Prop where

   show (Atom p)   = p
   show (Neg p)    = "no " ++ show p
   show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
   show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
   show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
   show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

p, p1, p2, q, r, s, t, u :: Prop p = Atom "p" p1 = Atom "p1" p2 = Atom "p2" q = Atom "q" r = Atom "r" s = Atom "s" t = Atom "t" u = Atom "u"

no :: Prop -> Prop no = Neg

infixr 5 \/ infixr 4 /\ infixr 3 --> infixr 2 <--> (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop (/\) = Conj (\/) = Disj (-->) = Impl (<-->) = Equi

-- Pasamos a definir las dos funciones pedidas:

--1.

n_variables :: Prop -> Integer n_variables (Atom p) = 1 n_variables (Neg p) = n_variables p n_variables (Conj p q) = n_variables p + n_variables q n_variables (Disj p q) = n_variables p + n_variables q n_variables (Impl p q) = n_variables p + n_variables q n_variables (Equi p q) = n_variables p + n_variables q

-- *SintaxisSemantica> n_variables (p <--> (p \/ q )) -- 3

--2.

profundidad :: Prop -> Integer profundidad (Atom p) = 0 profundidad (Neg p) = 1 + profundidad p profundidad (Conj p q) = 1 + profundidad p + profundidad q profundidad (Disj p q) = 1 + profundidad p + profundidad q profundidad (Impl p q) = 1 + profundidad p + profundidad q profundidad (Equi p q) = 1 + profundidad p + profundidad q

-- *SintaxisSemantica> profundidad (p --> (p \/ q )) -- 2