Logic.Judge.Formula.Substitution

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.

Documentation

type Substitution ext = Map String (Term ext)

A substitution maps identifiers to terms of a logic.

class Substitutable ext term where

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

Apply a substitution to a term.

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

pattern

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)

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

Instances

Substitutable Justification Justification

Methods

substitute :: Monad m => Substitution Justification -> Justification -> m Justification

pattern :: Monad m => Justification -> Justification -> m (Substitution Justification)

patternContinue :: Monad m => Substitution Justification -> Justification -> Justification -> m (Substitution Justification)

patternM :: Justification -> Justification -> StateFail (Substitution Justification) ()

(Eq ext, Substitutable ext ext) => Substitutable ext (Formula ext)

Methods

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

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

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

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

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

Methods

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

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

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

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

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

Methods

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

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

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

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)

Combine two substitutions, but fail if they are conflicting.

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