package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Substitutions

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Map
  - Pos
  - Seq
  - Set
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
    
    X
- LogtkFormula
  - FO
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Make
    
    Base
    
    Map
    
    MyT
    
    Seq
    
    Set
    
    TPTP
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - Map
    
    From
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    To
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - S
    
    Base
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
  - TERM
    
    Seq
    
    Set
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Map
  - Pos
  - Seq
  - Set
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    H
    
    X
  - S
    
    H
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
    
    X
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
    
    X
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
    
    X
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Map
  - Pos
  - Seq
  - Set
  - Tbl
- LogtkSignature
  - SMap
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Map
  - Seq
  - Set
  - TPTP
    
    Arith
  - Tbl
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Map
  - Seq
  - Set
  - TPTP
  - Tbl
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Map
  - Seq
  - Set
  - Subst
  - Tbl
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

Substitutions

Substitutions map variables to terms/types. They work on free variables (within a scope, so that the same variable can live within several scopes).

The concept of scope is to allow the same free variable to be used in several contexts without being renamed. A scope is kind of a namespace, where variables from distinct namespaces are always distinct.

type scope = int

A scope is an integer. Variables can only be bound in one scope, and variables from distinct scopes are distinct too.

type 'a scoped = 'a * scope

type term = LogtkScopedTerm.t

Renamings

A renaming is used to disambiguate variables that come from distinct scopes but have the same index. It is used to merge together several scopes, in a sound way, by ensuring variables from those scopes are mapped to distinct variables of the new scope. For instance, a given renaming applied to (X,0) and (X,1) will return two different variables, as if one of the X had been renamed prior to unification/binding.

module Renaming : sig ... end

Basics

type t

A substitution that binds term variables to other terms

type subst = t

val empty : t

The identity substitution

val is_empty : t -> bool

Is the substitution empty?

Operations on Substitutions

val lookup : t -> term -> scope -> term * scope

Lookup variable in substitution.

raises Not_found
if variable not bound.

val get_var : t -> term -> scope -> term * scope

Lookup recursively the var in the substitution, until it is not a variable anymore, or it is not bound

val mem : t -> term -> scope -> bool

Check whether the variable is bound by the substitution

exception KindError

val bind : t -> term -> scope -> term -> scope -> t

Add v -> t to the substitution. Both terms have a context. It is important that the bound term is De-Bruijn-closed (assert).

raises Invalid_argument
if v is already bound in the same context, to another term.

raises KindError
if a term of a given kind is bound to a term of another kind (see LogtkScopedTerm.Kind.t)

val append : t -> t -> t

append s1 s2 is the substitution that maps t to s2 (s1 t).

val remove : t -> term -> int -> t

Remove the given binding. No other variable should depend on it...

Set operations

val domain : t -> (term * scope) Sequence.t

Domain of substitution

val codomain : t -> (term * scope) Sequence.t

Codomain (image terms) of substitution

val introduced : t -> (term * scope) Sequence.t

Variables introduced by the substitution (ie vars of codomain)

val is_renaming : t -> bool

Check whether the substitution is a variable renaming

include LogtkInterfaces.PRINT with type t := t

val pp : Buffer.t -> t -> unit

val to_string : t -> string

val fmt : Format.formatter -> t -> unit

val fold : t -> 'a -> ('a -> term -> scope -> term -> scope -> 'a) -> 'a

val iter : t -> (term -> scope -> term -> scope -> unit) -> unit

val to_seq : t -> (term * scope * term * scope) Sequence.t

val to_list : t -> (term * scope * term * scope) list

val of_seq : ?init:t -> (term * scope * term * scope) Sequence.t -> t

val of_list : ?init:t -> (term * scope * term * scope) list -> t

Applying a substitution

val apply : t -> renaming:Renaming.t -> term -> scope -> term

Apply the substitution to the given term. This function assumes that all terms in the substitution are closed, and it will not perform De Bruijn indices shifting. For instance, applying {X -> f(db0)} (with db0 the De Bruijn index 0) to the term forall. p(X) will yield forall. p(f(db0)) (capturing) and not forall. p(f(db1)).

parameter renaming
used to desambiguate free variables from distinct scopes

val apply_no_renaming : t -> term -> scope -> term

Same as apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!

Specializations

module type SPECIALIZED = sig ... end

module Ty : SPECIALIZED with type term = LogtkType.t

module FO : SPECIALIZED with type term = LogtkFOTerm.t

module HO : SPECIALIZED with type term = LogtkHOTerm.t

module Form : SPECIALIZED with type term = LogtkFormula.FO.t