judge-0.1.3.0: Tableau-based theorem prover for justification logic.

Copyright(c) 2017 2018 N Steenbergen
LicenseGPL-3
Maintainerns@slak.ws
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell2010

Logic.Judge.Formula.Substitution

Description

This module makes it possible to obtain variable assignments by comparing Formulas, and to apply substitutions based on them.

The idea is similar to, but not the same as unification. When we pattern x to y, the former is schematic and the latter is literal. Even though their variables can be structurally identical, they are really different, in that, for example, Var "x" may well pattern with Implication (Var "x") (Var "x"), resulting in the substitution [("x", Implication "x" "x")].

Nevertheless, see subsumes from Control.Unification. They are not related by code, but the purpose is similar.

Synopsis

Documentation

type Substitution ext = Map String (Term ext) Source #

A substitution maps identifiers to terms of a logic.

class Substitutable ext term where Source #

The Substitutable class represents a relation between terms based on an extension ext (that is, formulas or extensions of formulas) and subterms that may be substituted for variables inside those ext-terms.

Minimal complete definition

substitute, patternM

Methods

substitute :: Monad m => Substitution ext -> term -> m term Source #

Apply a substitution to a term.

Note that at the time of writing, there is no fundamental distinction between variables and schematic variables.

pattern Source #

Arguments

:: Monad m 
=> term

The pattern formula to be filled in.

-> term

The formula to fill in the pattern.

-> m (Substitution ext) 

a pattern b tries to find a substitution such that a matches b. The a formula is taken as a schematic formula, where variables represent gaps to be filled in, and b is a "normal" formula, in which variables represent literals.

For simplicity, this function assumes that the formulas have been simplifyed. The intention is to make this explicit via a newtype at some point.

patternContinue :: Monad m => Substitution ext -> term -> term -> m (Substitution ext) Source #

Same as pattern, but starts patterning from a given starting state.

Instances

Substitutable Justification Justification Source # 
(Eq ext, Substitutable ext ext) => Substitutable ext (Formula ext) Source # 

Methods

substitute :: Monad m => Substitution ext -> Formula ext -> m (Formula ext) Source #

pattern :: Monad m => Formula ext -> Formula ext -> m (Substitution ext) Source #

patternContinue :: Monad m => Substitution ext -> Formula ext -> Formula ext -> m (Substitution ext) Source #

patternM :: Formula ext -> Formula ext -> StateFail (Substitution ext) ()

(Eq ext, Substitutable ext ext) => Substitutable ext (Term ext) Source # 

Methods

substitute :: Monad m => Substitution ext -> Term ext -> m (Term ext) Source #

pattern :: Monad m => Term ext -> Term ext -> m (Substitution ext) Source #

patternContinue :: Monad m => Substitution ext -> Term ext -> Term ext -> m (Substitution ext) Source #

patternM :: Term ext -> Term ext -> StateFail (Substitution ext) ()

(Eq ext, Substitutable ext a) => Substitutable ext (Marked a) Source # 

Methods

substitute :: Monad m => Substitution ext -> Marked a -> m (Marked a) Source #

pattern :: Monad m => Marked a -> Marked a -> m (Substitution ext) Source #

patternContinue :: Monad m => Substitution ext -> Marked a -> Marked a -> m (Substitution ext) Source #

patternM :: Marked a -> Marked a -> StateFail (Substitution ext) ()

merge :: (Ord k, Eq v, Monad m) => Map k v -> Map k v -> m (Map k v) Source #

Combine two substitutions, but fail if they are conflicting.

Note: The union is more efficient if the biggest set is the first argument.