This commit is contained in:
Vladimir Lemus 2024-03-22 10:21:21 -06:00
parent 59626d34f6
commit 691d7e4b9e
14 changed files with 737 additions and 0 deletions

BIN
Alonzo_Church.jpeg Executable file

Binary file not shown.

After

Width:  |  Height:  |  Size: 39 KiB

BIN
Emil_Leon_Post.jpeg Executable file

Binary file not shown.

After

Width:  |  Height:  |  Size: 16 KiB

BIN
alan_turing.jpg Executable file

Binary file not shown.

After

Width:  |  Height:  |  Size: 110 KiB

58
fun.hs Executable file
View File

@ -0,0 +1,58 @@
pari :: Integral a => a -> Bool
pari n = n `mod` 2 == 0
divi :: Int -> [a] -> ([a],[a])
divi n xs = (take n xs, drop n xs)
reste :: [Float] -> [Float] -> [Float]
reste xs ys = zipWith (-) xs ys
absol :: Int -> Int
absol n = if n >= 0 then n else -n
signi :: Int -> String
signi n = if n < 0 then "negativo" else
if n == 0 then "cero" else "positivo"
signg :: Int -> String
signg n | n < 0 = "negativo"
| n > 0 = "positivo"
|otherwise = "cero"
cabeza :: (a,b) -> a
cabeza (x,_) = x
prob :: [Char] -> Bool
prob ['a',_,_] = True
prob _ = False
cabezo :: [a] -> a
cabezo (x:_) =x
suma :: Int -> Int -> Int
suma = \x -> (\y -> x+y)
consta :: a -> (b -> a)
consta x = \_ -> x
impa :: Int -> [Int]
impa n = map f [0..n-1]
where f x = x*2 + 1
impa2 :: Int -> [Int]
impa2 n = map (\x -> x*2 + 1) [0..n-1]
tam :: [a] -> Int
tam xs = sum [1| _ <- xs]
factores :: Int -> [Int]
factores n = [x | x <- [1..n], n `mod` x == 0]
primo :: Int -> Bool
primo n = factores n == [1,n]
primos :: Int -> [Int]
primos n = [x | x <- [2..n], primo x]
busca :: Eq a => a -> [(a,b)] -> [b]
busca k t = [v | (k',v) <- t, k==k']

BIN
haskell_curry.jpg Executable file

Binary file not shown.

After

Width:  |  Height:  |  Size: 12 KiB

2
inc.hs Executable file
View File

@ -0,0 +1,2 @@
suma (x,y) = x+y
inc (x) = suma (x,1)

3
incurry.hs Executable file
View File

@ -0,0 +1,3 @@
suma x y = x+y
inc = suma 1
map inc [1..10]

4
muta.py Executable file
View File

@ -0,0 +1,4 @@
x=1
oldID=id(x)
x=x+1
id(x)==oldID

5
ordenar.hs Executable file
View File

@ -0,0 +1,5 @@
ordenar [] = []
ordenar (x:xs) = ordenar chico ++ [x] ++ ordenar grande
where
chico =[a | a<-xs, a<=x]
grande = [b | b<- xs, b>x]

BIN
pres_haskell.pdf Normal file

Binary file not shown.

288
pres_haskell.tex Normal file
View File

@ -0,0 +1,288 @@
\documentclass[12pt]{beamer}
\usetheme{Copenhagen}
\usepackage[utf8]{inputenc}
\usepackage[spanish]{babel}
\usepackage{amsmath}
\usepackage {xcolor}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{multicol}
\usepackage{xcolor}
\usepackage{tikz}
\usetikzlibrary{automata,positioning,arrows}
\usepackage[compat=1.1.0]{tikz-feynman}
\usepackage{listings} %Paquete para agregar codigo
\lstloadlanguages{Matlab} %use listings with Matlab for Pseudocode
\lstnewenvironment{PseudoCode}[1][]
{\lstset{language=Matlab,basicstyle=\scriptsize, keywordstyle=\color{darkblue},numbers=left,xleftmargin=.04\textwidth,#1}}
{}
\usepackage{appendixnumberbeamer}
%\setbeamerfont{page number in head}{size=\large}
%\setbeamertemplate{footline}{Diapositiva}
\setbeamertemplate{footline}[frame number]
\newcommand{\backupbegin}{
\newcounter{finalframe}
\setcounter{finalframe}{\value{framenumber}}
}
\newcommand{\backupend}{
\setcounter{framenumber}{\value{finalframe}}
}
\author{Lógica computacional}
\title{Una (h)ojeada a Haskell para la programación lógica}
%\setbeamercovered{transparent}
%\setbeamertemplate{navigation symbols}{}
%\logo{}
%\institute{}
%\date{}
%\subject{}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\begin{frame}{Mutación de los datos}
\lstinputlisting[firstline=1,lastline=5]{muta.py}
\end{frame}
\begin{frame}{Definiendo funciones en Haskell}
\begin{itemize}
\item Funciones \emph{curriadas} o \emph{no curriadas} (\emph{curried, non-curried})
\item Podemos pasar de una definición a la otra
\item Nos ahorra teclear y trabajamos en una idea más básica
\end{itemize}
\end{frame}
\begin{frame}{Haskell con curry y sin curry}
\begin{multicols}{2}
\lstinputlisting[firstline=1,lastline=3]{inc.hs}
\vspace{1 cm}
\lstinputlisting[firstline=1,lastline=4]{incurry.hs}
\end{multicols}
\end{frame}
\begin{frame}{Cálculo $\lambda$}
\begin{figure}[ht!]
%\begin{center}
\centering
\begin{subfigure}[b]{0.2\linewidth}
\includegraphics[width=\linewidth]{Alonzo_Church.jpeg}
\label{f:Alonzo Church}
\caption{Alonzo Church}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\label{f:Emil Leon Post}
\caption{Emi Leon Post}
\includegraphics[width=\linewidth]{Emil_Leon_Post.jpeg}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\includegraphics[width=\linewidth]{haskell_curry.jpg}
\label{f:Haskell Curry}
\caption{Haskell Curry}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\label{f:Alan Turing}
\caption{Alan Turing}
\includegraphics[width=\linewidth]{alan_turing.jpg}
\end{subfigure}
\caption{Aportaron al cálculo $\lambda$, entre muchas personas más. Algunas de estas imágenes cuentan con derechos de autor, son usada con fines educativos.}
\label{fig:Church}
%\end{center}
\end{figure}
\end{frame}
\begin{frame}{$\lambda$-términos en Haskell}
\begin{align*}
suma\ x=& \setminus y -> x+y \\
suma =& \setminus x -> (\setminus y -> x+y) \\
suma =& \setminus x -> \setminus y -> x+y
\end{align*}
¿Cuál es el chiste de eso?
\begin{align*}
(+=) =& \setminus x -> \setminus y -> x+y\\
(+=) =& \setminus x\ y -> x+y \\
3\ +=\ 5
\end{align*}
\end{frame}
\begin{frame}{Listas}
\begin{itemize}
\item Conjunto nordenado de objetos no necesariamente del mismo tipo
\item Versátiles y base de otro tipo de estructuras
\item Los arreglos tienen un nombre y un apuntador
\item Listas tienen dos apuntadores
\end{itemize}
\end{frame}
\begin{frame}{Sumando en una lista}
\begin{equation*}
sum\ [1..100]
\end{equation*}
\lstinputlisting[firstline=1,lastline=3]{sumalista.hs}
Prueben $a=[1,2,3,4]$ y $b=['a','b','c','d']$
\end{frame}
\begin{frame}{Aplicación de funciones en Haskell}
\begin{center}
\begin{tabular}{||c|c||}
\hline
Matemática & Haskell \\ [0.5ex]
\hline\hline
$f(x)$ & $f\ x$ \\
\hline
$f(x,y)$ & $f\ x\ y$ \\
\hline
$f(g(x))$ & $f\ (g\ x)$ \\
\hline
$f(x,g(y))$ & $f\ x\ (g\ y)$ \\
\hline
$f(x)g(y)$ & $f\ x\ *\ g\ y$ \\ [1ex]
\hline
\end{tabular}
\end{center}
\end{frame}
\begin{frame}{Comandos para scripts}
\begin{center}
\begin{tabular}{||p{3cm} | p{4cm}||}
\hline
Comando & Accion \\ [0.5ex]
\hline\hline
$:load\ nombre$ & Cargar $script$ \\
\hline
$:reload$ & Recargar script \\
\hline
$:edit\ nombre$ & Cambiar nombre del $script$ \\
\hline
$:edit$ & Editar el $script$ \\
\hline
$:type\ expr$ & Mostrar el tipo de la expresión \\
\hline
$:?$ & Mostrar los comandos \\
\hline
$:q$ & Salir de $GHCi$ \\
\hline
\end{tabular}
\end{center}
\end{frame}
\begin{frame}{Cadenas especiales y comentarios}
\textbf{case class data default deriving do else if import in infix infixl infixr instance let module newtype of then type where}
\begin{itemize}
\item Comentarios ordinarios (máximo una línea), empiezan con $--$.
\item Comentarios anidados (multilínea), empiezan con $\{-$ y terminan con $-\}$
\end{itemize}
\end{frame}
\begin{frame}{Ordenar una lista}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=1,lastline=6,language=haskell]{ordenar.hs}
Prueben $a=[1,2,3,4]$ y $b=['a','b','c','d']$
\end{frame}
\begin{frame}{Operaciones sobre listas}
\begin{multicols}{2}
\begin{align*}
a\ =&\ [1,2,3,4,5]\\
head\ a&\\
tail\ a&\\
init\ a&\\
last\ a&\\
a!!2&\\
take\ 3\ a& \\
filter\ odd\ a&
\end{align*}
\begin{align*}
drop\ 3\ a&\\
length\ a&\\
sum\ a&\\
product\ a&\\
[1,2,3]++[4,5]&\\
reverse\ a&\\
null\ a&\\
minimum\ a\\
head\ []&\text{ (¿?)}
\end{align*}
\end{multicols}
\end{frame}
\begin{frame}{Expresiones condicionales}
\begin{itemize}
\item Expresiones condicionales
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=10,lastline=12,language=haskell]{fun.hs}
\item Expresiones condicionales anidadas
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=13,lastline=16,language=haskell]{fun.hs}
\end{itemize}
\end{frame}
\begin{frame}{Guardas}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=17,lastline=21,language=haskell]{fun.hs}
\end{frame}
\begin{frame}{Números primos}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=48,lastline=56,language=haskell]{fun.hs}
\end{frame}
\begin{frame}{Verificador de tautologíoas}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=1,lastline=8,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Declarando la sustitución}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=48,lastline=62,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Las variables en una proposición}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=63,lastline=71,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Las posibles combinaciones en una sustitución}
\begin{itemize}
\item Pensando en $veradero=1$ y $falso=0$ es equivalente a contar en binario.
\item O se puede hacer de otra forma viendo las regularidades
\begin{center}
\begin{tabular}{c|cc}
F & F & F \\
F & F & T \\
F & T & F \\
F & T & T \\
\hline
T & F & F \\
T & F & T \\
T & T & F \\
T & T & T \\
\end{tabular}
\end{center}
\end{itemize}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=72,lastline=76,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Ahora sí a definir todas las posibles sustituciones}
\begin{itemize}
\item Remover duplicados de la lista de variables
\item Generar los posibles valores con $bools$
\item Emparejar las lista $zip$
\end{itemize}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=77,lastline=84,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{La fase final, el que decide}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=85,lastline=90,language=haskell]{taut.hs}
Armamos una proposición:
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=30,lastline=32,language=haskell]{taut.hs}
\end{frame}
\end{document}

286
pres_haskell.tex~ Normal file
View File

@ -0,0 +1,286 @@
\documentclass[12pt]{beamer}
\usetheme{Copenhagen}
\usepackage[utf8]{inputenc}
\usepackage[spanish]{babel}
\usepackage{amsmath}
\usepackage {xcolor}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{multicol}
\usepackage{xcolor}
\usepackage{tikz}
\usetikzlibrary{automata,positioning,arrows}
\usepackage[compat=1.1.0]{tikz-feynman}
\usepackage{listings} %Paquete para agregar codigo
\lstloadlanguages{Matlab} %use listings with Matlab for Pseudocode
\lstnewenvironment{PseudoCode}[1][]
{\lstset{language=Matlab,basicstyle=\scriptsize, keywordstyle=\color{darkblue},numbers=left,xleftmargin=.04\textwidth,#1}}
{}
\usepackage{appendixnumberbeamer}
%\setbeamerfont{page number in head}{size=\large}
%\setbeamertemplate{footline}{Diapositiva}
\setbeamertemplate{footline}[frame number]
\newcommand{\backupbegin}{
\newcounter{finalframe}
\setcounter{finalframe}{\value{framenumber}}
}
\newcommand{\backupend}{
\setcounter{framenumber}{\value{finalframe}}
}
\author{Lógica computacional}
\title{Una (h)ojeada a Haskell para la programación lógica}
%\setbeamercovered{transparent}
%\setbeamertemplate{navigation symbols}{}
%\logo{}
%\institute{}
%\date{}
%\subject{}
\begin{document}
\begin{frame}
\titlepage
\end{frame}
\begin{frame}{Mutación de los datos}
\lstinputlisting[firstline=1,lastline=5]{muta.py}
\end{frame}
\begin{frame}{Definiendo funciones en Haskell}
\begin{itemize}
\item Funciones \emph{curriadas} o \emph{no curriadas} (\emph{curried, non-curried})
\item Podemos pasar de una definición a la otra
\item Nos ahorra teclear y trabajamos en una idea más básica
\end{itemize}
\end{frame}
\begin{frame}{Haskell con curry y sin curry}
\begin{multicols}{2}
\lstinputlisting[firstline=1,lastline=3]{inc.hs}
\vspace{1 cm}
\lstinputlisting[firstline=1,lastline=4]{incurry.hs}
\end{multicols}
\end{frame}
\begin{frame}{Cálculo $\lambda$}
\begin{figure}[ht!]
%\begin{center}
\centering
\begin{subfigure}[b]{0.2\linewidth}
\includegraphics[width=\linewidth]{Alonzo_Church.jpeg}
\label{f:Alonzo Church}
\caption{Alonzo Church}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\label{f:Emil Leon Post}
\caption{Emi Leon Post}
\includegraphics[width=\linewidth]{Emil_Leon_Post.jpeg}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\includegraphics[width=\linewidth]{haskell_curry.jpg}
\label{f:Haskell Curry}
\caption{Haskell Curry}
\end{subfigure}
\begin{subfigure}[b]{0.2\linewidth}
\label{f:Alan Turing}
\caption{Alan Turing}
\includegraphics[width=\linewidth]{alan_turing.jpg}
\end{subfigure}
\caption{Aportaron al cálculo $\lambda$, entre muchas personas más. Algunas de estas imágenes cuentan con derechos de autor, son usada con fines educativos.}
\label{fig:Church}
%\end{center}
\end{figure}
\end{frame}
\begin{frame}{$\lambda$-términos en Haskell}
\begin{align*}
suma\ x=& \setminus y -> x+y \\
suma =& \setminus x -> (\setminus y -> x+y) \\
suma =& \setminus x -> \setminus y -> x+y
\end{align*}
¿Cuál es el chiste de eso?
\begin{align*}
(+=) =& \setminus x -> \setminus y -> x+y\\
(+=) =& \setminus x\ y -> x+y \\
3\ +=\ 5
\end{align*}
\end{frame}
\begin{frame}{Listas}
\begin{itemize}
\item Conjunto nordenado de objetos no necesariamente del mismo tipo
\item Versátiles y base de otro tipo de estructuras
\item Los arreglos tienen un nombre y un apuntador
\item Listas tienen dos apuntadores
\end{itemize}
\end{frame}
\begin{frame}{Sumando en una lista}
\begin{equation*}
sum\ [1..100]
\end{equation*}
\lstinputlisting[firstline=1,lastline=3]{sumalista.hs}
Prueben $a=[1,2,3,4]$ y $b=['a','b','c','d']$
\end{frame}
\begin{frame}{Aplicación de funciones en Haskell}
\begin{center}
\begin{tabular}{||c|c||}
\hline
Matemática & Haskell \\ [0.5ex]
\hline\hline
$f(x)$ & $f\ x$ \\
\hline
$f(x,y)$ & $f\ x\ y$ \\
\hline
$f(g(x))$ & $f\ (g\ x)$ \\
\hline
$f(x,g(y))$ & $f\ x\ (g\ y)$ \\
\hline
$f(x)g(y)$ & $f\ x\ *\ g\ y$ \\ [1ex]
\hline
\end{tabular}
\end{center}
\end{frame}
\begin{frame}{Comandos para scripts}
\begin{center}
\begin{tabular}{||p{3cm} | p{4cm}||}
\hline
Comando & Accion \\ [0.5ex]
\hline\hline
$:load\ nombre$ & Cargar $script$ \\
\hline
$:reload$ & Recargar script \\
\hline
$:edit\ nombre$ & Cambiar nombre del $script$ \\
\hline
$:edit$ & Editar el $script$ \\
\hline
$:type\ expr$ & Mostrar el tipo de la expresión \\
\hline
$:?$ & Mostrar los comandos \\
\hline
$:q$ & Salir de $GHCi$ \\
\hline
\end{tabular}
\end{center}
\end{frame}
\begin{frame}{Cadenas especiales y comentarios}
\textbf{case class data default deriving do else if import in infix infixl infixr instance let module newtype of then type where}
\begin{itemize}
\item Comentarios ordinarios (máximo una línea), empiezan con $--$.
\item Comentarios anidados (multilínea), empiezan con $\{-$ y terminan con $-\}$
\end{itemize}
\end{frame}
\begin{frame}{Ordenar una lista}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=1,lastline=6,language=haskell]{ordenar.hs}
Prueben $a=[1,2,3,4]$ y $b=['a','b','c','d']$
\end{frame}
\begin{frame}{Operaciones sobre listas}
\begin{multicols}{2}
\begin{align*}
a\ =&\ [1,2,3,4,5]\\
head\ a&\\
tail\ a&\\
init\ a&\\
last\ a&\\
a!!2&\\
take\ 3\ a& \\
filter\ odd\ a&
\end{align*}
\begin{align*}
drop\ 3\ a&\\
length\ a&\\
sum\ a&\\
product\ a&\\
[1,2,3]++[4,5]&\\
reverse\ a&\\
null\ a&\\
minimum\ a\\
head\ []&\text{ (¿?)}
\end{align*}
\end{multicols}
\end{frame}
\begin{frame}{Expresiones condicionales}
\begin{itemize}
\item Expresiones condicionales
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=10,lastline=12,language=haskell]{fun.hs}
\item Expresiones condicionales anidadas
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=13,lastline=16,language=haskell]{fun.hs}
\end{itemize}
\end{frame}
\begin{frame}{Guardas}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=17,lastline=21,language=haskell]{fun.hs}
\end{frame}
\begin{frame}{Números primos}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=48,lastline=56,language=haskell]{fun.hs}
\end{frame}
\begin{frame}{Verificador de tautologíoas}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=1,lastline=8,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Declarando la sustitución}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=48,lastline=62,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Las variables en una proposición}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=63,lastline=71,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Las posibles combinaciones en una sustitución}
\begin{itemize}
\item Pensando en $veradero=1$ y $falso=0$ es equivalente a contar en binario.
\item O se puede hacer de otra forma viendo las regularidades
\begin{center}
\begin{tabular}{c|cc}
F & F & F \\
F & F & T \\
F & T & F \\
F & T & T \\
\hline
T & F & F \\
T & F & T \\
T & T & F \\
T & T & T \\
\end{tabular}
\end{center}
\end{itemize}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=72,lastline=76,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{Ahora sí a definir todas las posibles sustituciones}
\begin{itemize}
\item Remover duplicados de la lista de variables
\item Generar los posibles valores con $bools$
\item Emparejar las lista $zip$
\end{itemize}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=77,lastline=84,language=haskell]{taut.hs}
\end{frame}
\begin{frame}{La fase final, el que decide}
\lstinputlisting[basicstyle=\ttfamily\scriptsize,firstline=85,lastline=90,language=haskell]{taut.hs}
\end{frame}
\end{document}

2
sumalista.hs Executable file
View File

@ -0,0 +1,2 @@
sumalista [] = 0
sumalista (n:ns) = n + sumalista ns

89
taut.hs Executable file
View File

@ -0,0 +1,89 @@
data Prop = Const Bool
| Var Char
| Not Prop
| And Prop Prop
| Or Prop Prop
| Imply Prop Prop
| Iff Prop Prop
p1 :: Prop
p1 = And (Var 'A') (Not (Var 'A'))
p2 :: Prop
p2 = Imply (And (Var 'A') (Var 'B')) (Var 'A')
p3 :: Prop
p3 = Imply (Var 'A') (And (Var 'A') (Var 'B'))
p4 :: Prop
p4 = Imply (And (Var 'A') (Imply (Var 'A') (Var 'B'))) (Var 'B')
p5 :: Prop
p5 = Iff (Imply (Var 'B') (Imply (Var 'A') (Var 'C'))) (Imply (And (Var 'B') (Var 'A')) (Var 'C'))
p6 :: Prop
p6 = Iff (Or (Var 'A') (And (Var 'B') (Var 'C'))) (And (Or (Var 'A') (Var 'B')) (Or (Var 'A') (Var 'C')))
p7 :: Prop
p7 = Imply (Imply (Imply (Var 'P') (Var 'Q')) (Var 'P')) (Var 'P')
p8 :: Prop
p8 = Iff (Var 'P') (Or (Var 'P') (Var 'Q'))
p9 :: Prop
p9 = Imply (Var 'P') (Or (Var 'P') (Var 'Q'))
p10 :: Prop
p10 = Not (Imply (Imply (Var 'P') (Var 'Q')) (Imply (And (Var 'P') (Var 'R')) (And (Var 'Q') (Var 'R'))))
p11 :: Prop
p11 = Iff (And (Var 'P') (Or (Var 'Q') (Var 'R'))) (Or (And (Var 'P') (Var 'Q')) (And (Var 'P') (Var 'R')))
p12 :: Prop
p12 = Iff (Or (Not (Or (Var 'P') (Var 'Q'))) (Not (And (Var 'R') (Var 'Q')))) (Or (Not (Var 'Q')) (Not (Var 'R')))
p13 :: Prop
p13 = Iff (Iff (Var 'P') (Var 'Q')) (Or (Not (Or (Not (Var 'P')) (Not (Var 'Q')))) (Not (Or (Var 'P') (Var 'Q'))))
type Assoc k v = [(k,v)]
find :: Eq k => k -> Assoc k v -> v
find k t = head [v | (k',v) <- t, k==k']
type Sust = Assoc Char Bool
eval :: Sust -> Prop -> Bool
eval _ (Const b) = b
eval s (Var x) = find x s
eval s (Not p) = not (eval s p)
eval s (And p q) = eval s p && eval s q
eval s (Or p q) = eval s p || eval s q
eval s (Imply p q) = eval s p <= eval s q
eval s (Iff p q) = (eval s p <= eval s q) && (eval s q <= eval s p)
vars :: Prop -> [Char]
vars (Const _) = []
vars (Var x) = [x]
vars (Not p) = vars p
vars (And p q) = vars p ++ vars q
vars (Or p q) = vars p ++ vars q
vars (Imply p q) = vars p ++ vars q
vars (Iff p q) = vars p ++ vars q
bools :: Int -> [[Bool]]
bools 0 = [[]]
bools n = map (False:) bss ++ map (True:) bss
where bss = bools (n-1)
rmdumps :: Eq a => [a] -> [a]
rmdumps [] = []
rmdumps (x:xs) = x : filter (/= x) (rmdumps xs)
susts :: Prop -> [Sust]
susts p = map (zip vs) (bools (length vs))
where vs = rmdumps (vars p)
esTaut :: Prop -> Bool
esTaut p = and [eval s p | s <- susts p]
esCont :: Prop -> Bool
esCont p = not (or [eval s p | s <- susts p])