{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-} {- | A powerful system for /propositional logic/. Defines an abstract concept of a /propositional algebra/ and provides both default and fast instances. Emphasizes the use of /(canonic) normalizations/ in general and so-called /Prime Normal Forms/ in particular. <http://www.bucephalus.org/PropLogic/> is the homepage with additional information for a variety of users, including short and thorough introductions to the use of "PropLogic" and the mathematical background of the whole design. -} module PropLogic ( -- * Start -- | The whole package is very modular in itself, according to the different perspectives we take to approach the subject -- (as explained below). It is possible to be more specific in an application and to import only certain parts. But the -- easiest and recommended way is the import of just this "PropLogic" module, which is just the summary of its main parts. -- -- This package uses certain extensions to the Haskell 98 standard. -- In particular, the /propositional algebra/ concept is implemented as a two-parameter type class 'PropAlg'. -- The package is developed with GHC (the Glasgow Haskell Compiler) and that works fine. -- Hugs works fine as well, but it requires to be started with @hugs -98@. -- * The composition and modules -- ** Introduction -- | /Propositional logic/ (also called /sentential logic/) is a very standard and relatively uncomplicated system in itself. -- -- The (binary) /boolean value algebra/ is one of the simplest structures at all and a standard in almost every programming language. -- (Recall, that it is in Haskell given by the type @Bool@, made of @True@ and @False@, the -- order @<=@ and the boolean junctors @not@, @&&@ and @||@.) -- A /propositional algebra/ is then essentially defined as the extension of this boolean value algebra with free variables, -- commonly called /atoms/. -- -- But however dense an abstract characterization of a propositional algebra may be, most traditional introductions are more complex and -- start with a syntax, i.e. some choice of what /propositional formulas/ should cover, a more or less diverse semantics, together -- with some calculus for semantically sound and complete manipulation of formulas. -- ** The four main modules -- | In this Haskell version of propositional logic, one design principle is the separation of the different aspects in four -- main modules. -- -- > -- > -- > PropLogicCore -- > / \ -- > / \ -- > / \ -- > / \ -- > DefaultPropLogic FastPropLogic -- > \ / -- > \ / -- > \ / -- > \ / -- > PropLogicTest -- > -- ** The abstract /core/ concepts module PropLogicCore, -- | This module comprises the abstract definition of two core concepts of propositional logic: -- -- * The data type @('PropForm' a)@ of /propositional formulas/, based on a given /atom/ type @a@. -- -- * The two-parameter type class @('PropAlg' a p)@ of a /propositional algebra/, where @a@ is the /atom/ type and @p@ the type of -- /propositions/. Operations of such a structure include a decision if two propositions are 'equivalent', if a given proposition is -- 'satisfiable', a converter 'toPropForm' and the inverse 'fromPropForm', which turns a propositional formula into a proposition. -- -- "PropLogicCore" provides the interface for the toolbox most users would need in most real circumstances. -- The actual 'PropAlg' instances are implemented in the following two modules. -- ** Propositional logic the /default/ style and the descriptive introduction of (canonic) normalizations module DefaultPropLogic, -- | "DefaultPropLogic" on the other hand provides one (actually more than one) instance of 'PropAlg', along with a whole range of -- additional functionalities. For example, it introduces the concepts of /valuators/ and a /truth tables/. -- The title /default/ indicates the very straight forward, intuitive, and naive approach. -- For example, the implementation for the satisfiability -- function applies the naive test, if the truth table has at least one /true/ in the result column. -- In fact, in "DefaultPropLogic", the semantics of propositional algebra is thoroughly reconstructed and that makes this -- module suitable as an interactive tutorial for propositional logic itself and all the concepts of the abstract level. -- (There is an according introduction available online.) -- | The "DefaultPropLogic" introduces something else, namely a non-traditional idea of what the standard operations are. -- We don't bother with the introduction of a certain rule system or calculus and we don't reconstruct propositional logic as -- a proof system. -- Our approach is based on /(canonic) normalizations/ instead. -- In particular, we use special kinds of /DNF/s and /CNF/s (/disjunctive/ or /conjunctive normal forms/), namely -- /prime normal forms/, and all traditional problems come down to a single normalization. -- For example, a formula φ is satisfiable iff the prime DNF is not the empty disjunction, -- i.e. iff the call of @primeDNF φ@ returns another result than @(∨)@. -- All traditional problems can be solved with one single canonization such as 'primeDNF' or 'primeCNF', respectively. -- ** Instances of propositional algebras with /fast/ implementations module FastPropLogic, -- | Prime Normal Forms are indeed distinguished and reasonably compact semantic canonizations of propositional formulas. -- However, for all cases with more than just a trivial amount of atoms involved, the default implementations are not feasible, -- because of the exponential cost explosing of these default methods. -- In "FastPropLogic" we provide a complete new implementation, based on a /fast/ system of algorithms. -- Main goal is the construction of fast instances of the 'PropAlg' type class. -- ** Additional functions module PropLogicTest, -- | The independent implementations of the default and the fast approach allows us to use one as a test for the other, because -- they should produce the same results. To do that systematically, "PropLogicTest" has random formula generators and test for -- correctness. -- Another goal is the investigation of the actual performance of the /fast/ methods. -- Finally, this module contains some useful functions which use functions from both "DefaultPropLogic" and "FastPropLogic". -- ** Hidden modules -- | "TextDisplay" implements some methods for the two-dimensional treatment of plain text output. This is a useful tool, for -- example for the display of truth tables in interpreter sessions. It provides the 'display' function which can be applied to -- all the main concepts (formulas, truth tables, normal forms), for more intuitive and graphical layout than calling 'print'. -- -- "Olist" has methods for treating ordered lists as finite sets. -- -- "Costack" is the implementation of a /concatenable stack/, i.e. it re-defines the standard Haskell functions -- @(:)@, @(null)@, @head@, @tail@, and @(++)@. The concatenation @(++)@ is not a primitive function in Haskell, and a /costack/ -- is a data structure, where all these functions are primitive. -- The "Costack" module is only used in the implementations of the "FastPropLogic" functions. -- * Propositional algebras -- | As mentioned already, the two core concepts in the implementation of our version of propositional logic are -- /propositional formulas/, given as the data type @'PropForm' a@, and the two-parameter type class @'PropAlg' a p@ -- for the abstract notion of a /propositional algebra/. -- These two notions are described in more detail in the "PropLogicCore" module. -- ** The different instances -- | The actual implementation of 'PropAlg' instances is done in two other modules and in two different ways: -- -- (I) In the "DefaultPropLogic" module, we implement three different propositional algebras in a standard, intuitive and straight -- forward way. -- -- (1) @(PropAlg a ('PropForm' a))@, is the standard propositional algebra, where the propositions are actually the propositional -- formulas. -- -- (2) @(PropAlg a ('TruthTable' a))@ is a less common, but nevertheless very intuitive propositional algebra, which is based on -- /truth tables/. -- -- (3) @(PropAlg 'Void' 'Bool')@ instantiates the predefined algebra @Bool@ of boolean values as a propositional algebra, the -- one with the empty atom type @Void@. Actually, all other instances of propositional algebras are equally powerful in the -- sense that they can all be based on an arbitrary type @a@ of atoms. But the propositional algebra on @Bool@ is just the -- trivial algebra with the empty atom type and we neglect it in the comparison of the different instances below. -- -- (II) In the "FastPropLogic" module defines a small variety of propositional algebras where the propositions are certain kinds of -- /normal forms/. -- -- (1) @(PropAlg a ('XPDNF' a))@ is the algebra, where each proposition is an /indexed prime disjunctive normal form/. -- One distinctive feature of these forms is that they are /canonic/ in the sense that two propositions are equivalent if and only -- if they are equal. -- -- (2) @(PropAlg a ('XPCNF' a))@ is the /dual/ version of the previous algebra, elements are /indexed prime conjunctive normal forms/. -- -- (3) @(PropAlg a ('MixForm' a))@ is a variation and mix of the previous two algebras. The normal forms here may be either -- /conjunctive/ or /disjunctive normal forms/, they are not necessarily /prime/ normal forms, but may only be /pairwise minimal/. -- So in this algebra, the propositions are no longer canonic. But the advantage is that all the junctions, i.e. the boolean -- operations such as negation, conjunction etc. are of polynomial complexity. And in applications, where predominanty junctions -- are used, this implementation of a propositional algebra is faster than the previous two. -- ** Feasibility and performance of the fast implementations -- | The default instances of 'PropAlg' (i.e. on formulas and truth tables) are not feasible for other than small problems, and -- that is why we implemented some fast instances as well. -- One example for a cost explosing is the call of 'satisfiable' applied to a formula φ. If φ has say @n@ different atoms, -- then there are @2^n@ different valuations of these atoms and in the worst case, we need to test for all these valuations, if -- they make φ true or false. /Not feasible/ means /exponential in the worst input cases/. -- Not all functions of the algebra on formulas are not feasible in this sense. -- But compare to the default instances, the fast instances are called /fast/, because none of their functions is exponential. -- -- In fact, we cannot claim really, that this is actually true. We don't have a proof for the non-exponentiality of the fast functions. -- The only criterion for the feasibility of our implementations is empirical. -- For more detail and empirical data about the performance of the involved functions, we refer to the home page. ) where import TextDisplay import Olist import Costack import PropLogicCore import DefaultPropLogic import FastPropLogic import PropLogicTest