Ver el código de «Problema 1» - Lógica matemática y fundamentos (2012-13)

== 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 ==
<source lang="haskell">

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


-- Mis definiciones de número de variables y de profundidad son prácticamente iguales a las definidas por mi compañero pero he añadido
-- constructores que pienso que hacen falta.
 
-- Primero definimos todo lo relativo a tipo y a representación:

module SintaxisSemantica where


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 funciones:

--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


</source>