Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

Fitch.Unification

Contents

Collecting Variables
- All variables
- Free variables
Substitution
Unification

Description

This module implements the ability to check a Term, Formula or Assumption against its TermSpec, FormulaSpec or AssumptionSpec.

Furthermore, implements a variant of the Martelli Montanari unification algorithm. where tFormulae or Terms are unified on a specific variable, meaning the variable must occur on the left-hand-side of the resulting unifier.

Synopsis

class AllVars a where
- allVars :: a -> Set Name
- makeFresh :: Name -> a -> Name
- isFresh :: Name -> a -> Bool
class FreeVars a where
- freeVars :: a -> Set Name
class Substitute a b where
- subst :: Subst b -> a -> a
unifyTermsOnVariable :: Name -> [(Term, Term)] -> Maybe [(Name, Term)]
unifyFormulaeOnVariable :: Name -> [(RawFormula, RawFormula)] -> Maybe (Map Name Term)
termMatchesSpec :: [(Term, TermSpec)] -> Bool
formulaMatchesSpec :: RawFormula -> FormulaSpec -> Bool
assumptionMatchesSpec :: RawAssumption -> AssumptionSpec -> Bool

Collecting Variables

All variables

class AllVars a where Source #

Type class for structures that have variables occuring in them.

Minimal complete definition

allVars

Methods

allVars :: a -> Set Name Source #

Returns all variables occuring in the structure.

makeFresh :: Name -> a -> Name Source #

Takes a name and a structure and makes it fresh w.r.t. all the variables occuring in the structure.

isFresh :: Name -> a -> Bool Source #

Checks if a variable is fresh in a structure.

Instances

Instances details

AllVars RawAssumption Source #
Instance details Defined in Fitch.Unification Methods allVars :: RawAssumption -> Set Name Source # makeFresh :: Name -> RawAssumption -> Name Source # isFresh :: Name -> RawAssumption -> Bool Source #
AllVars RawFormula Source #
Instance details Defined in Fitch.Unification Methods allVars :: RawFormula -> Set Name Source # makeFresh :: Name -> RawFormula -> Name Source # isFresh :: Name -> RawFormula -> Bool Source #
AllVars Term Source #
Instance details Defined in Fitch.Unification Methods allVars :: Term -> Set Name Source # makeFresh :: Name -> Term -> Name Source # isFresh :: Name -> Term -> Bool Source #

Free variables

class FreeVars a where Source #

Type class for structures that have variables occuring in them.

Methods

freeVars :: a -> Set Name Source #

Returns only the free (i.e. unbound) variables occuring in the structure.

Instances

Instances details

FreeVars RawAssumption Source #
Instance details Defined in Fitch.Unification Methods freeVars :: RawAssumption -> Set Name Source #
FreeVars RawFormula Source #
Instance details Defined in Fitch.Unification Methods freeVars :: RawFormula -> Set Name Source #
FreeVars Term Source #
Instance details Defined in Fitch.Unification Methods freeVars :: Term -> Set Name Source #

Substitution

class Substitute a b where Source #

Type class for substitution.

Methods

subst :: Subst b -> a -> a Source #

Takes a substitution and replaces variables occuring in the structure of type a with elements of type b. Of course this only makes sense if the type a also contains the type b.

Instances

Instances details

Substitute RawFormula Term Source #
Instance details Defined in Fitch.Unification Methods subst :: Subst Term -> RawFormula -> RawFormula Source #
Substitute Term Term Source #
Instance details Defined in Fitch.Unification Methods subst :: Subst Term -> Term -> Term Source #

Unification

unifyTermsOnVariable :: Name -> [(Term, Term)] -> Maybe [(Name, Term)] Source #

Unification on terms, this is the Martelli-Montanari unification algorithm with a twist: the unification happens on a variable x. Meaning the resulting unificator must have the variable x on the left hand side.

This is guaranteed by adding a new orient rule, which orients assignments of the form x := y, where y is also a variable.

unifyFormulaeOnVariable :: Name -> [(RawFormula, RawFormula)] -> Maybe (Map Name Term) Source #

Lifts unifyTermsOnVariable to formulae.

termMatchesSpec :: [(Term, TermSpec)] -> Bool Source #

Unify Term with TermSpec.

formulaMatchesSpec :: RawFormula -> FormulaSpec -> Bool Source #

Unify RawFormula with FormulaSpec.

assumptionMatchesSpec :: RawAssumption -> AssumptionSpec -> Bool Source #

Unify RawAssumption with AssumptionSpec.