package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.SubstSource

Substitutions

Substitutions map (scoped) 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.

Sourcetype term = InnerTerm.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.

Sourcemodule Renaming : sig ... end

Basics

Sourcetype t

A substitution that binds term variables to other terms

Sourcetype subst = t
Sourceval empty : t

The identity substitution

Sourceval is_empty : t -> bool

Is the substitution empty?

Operations on Substitutions

Sourceval find_exn : t -> var Scoped.t -> term Scoped.t

Lookup variable in substitution.

Sourceval find : t -> var Scoped.t -> term Scoped.t option
Sourceval deref : t -> term Scoped.t -> term Scoped.t

deref t s_t dereferences t as long as t is a variable bound in subst

Sourceval get_var : t -> var Scoped.t -> term Scoped.t option

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

  • returns

    None if the variable is not bound, Some (deref (t, sc_t)) if v is bound to t, sc_t

Sourceval mem : t -> var Scoped.t -> bool

Check whether the variable is bound by the substitution

Sourceexception InconsistentBinding of var Scoped.t * term Scoped.t * term Scoped.t
Sourceval bind : t -> var Scoped.t -> term Scoped.t -> t

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

Sourceval update : t -> var Scoped.t -> term Scoped.t -> t

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

Sourceval merge : t -> t -> t

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

Sourceval remove : t -> var Scoped.t -> t

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

Sourceval filter_scope : t -> Scoped.scope -> t

Only keep bindings from this scope

Set operations

Sourceval domain : t -> var Scoped.t Iter.t

Domain of substitution

Sourceval codomain : t -> term Scoped.t Iter.t

Codomain (image terms) of substitution

Sourceval introduced : t -> var Scoped.t Iter.t

Variables introduced by the substitution (ie vars of codomain)

Sourceval normalize : t -> t

Normalize bindings that are in the same scope. E.g. x0 -> f(y0), y0 -> g(z0), z0->a becomes x0->f(g(a))0, y0->g(a)0, z0->g(z0)

Sourceval map : (term -> term) -> t -> t

Map on term

Sourceval filter : (var Scoped.t -> term Scoped.t -> bool) -> t -> t

Filter bindings

Sourceval is_renaming : t -> bool

Check whether the substitution is a variable renaming

Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
Sourceval pp_bindings : t CCFormat.printer

Only print the bindings, no box

Sourceval fold : ('a -> var Scoped.t -> term Scoped.t -> 'a) -> 'a -> t -> 'a
Sourceval iter : (var Scoped.t -> term Scoped.t -> unit) -> t -> unit
Sourceval to_seq : t -> (var Scoped.t * term Scoped.t) Iter.t
Sourceval to_list : t -> (var Scoped.t * term Scoped.t) list
Sourceval of_seq : ?init:t -> (var Scoped.t * term Scoped.t) Iter.t -> t
Sourceval of_list : ?init:t -> (var Scoped.t * term Scoped.t) list -> t

Applying a substitution

Sourceval apply : Renaming.t -> t -> term Scoped.t -> 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

Specializations

Sourcemodule type SPECIALIZED = sig ... end
Sourcemodule Ty : SPECIALIZED with type term = Type.t
Sourcemodule FO : sig ... end

Projections for proofs

Sourcemodule Projection : sig ... end