☰

*ON THIS PAGE*# Term checking utilities

**Author(s):** The Ciao Development Team.## Usage and interface

## Documentation on exports

`variant(Term1,Term2)`
`ask(Term1,Term2)`
`most_specific_generalization(Term1,Term2,Term)`
`most_general_instance(Term1,Term2,Term)`
## Documentation on internals

## Documentation on imports

This module has the following direct dependencies:## Other information

Currently, `ask/2` and `instance/2` are exactly the same. However, `ask/2` is intended to be more general, since it is also applicable to constraint domains (although not yet implemented): i.e., for the particular case of Herbrand terms, `ask/2` is just `instance/2`.

This module implements a basic set of term checking utilities.

**Library usage:**`:- use_module(library(terms_check)).`**Exports:***Predicates:*`variant/2`,`ask/2`,`subsumes_term/2`,`most_specific_generalization/3`,`most_general_instance/3`,`unifiable/3`.*Properties:*`instance/2`.*Regular Types:*`unifier/1`.

PREDICATEvariant/2

Term1 and Term2 are identical up to renaming.

PREDICATEask/2

Term1 and Term2 unify without producing bindings for the variables of Term1. I.e., `instance(Term1,Term2)` holds.

PROPERTYinstance/2

Usage:`instance(Term1,Term2)`

Term1 is an instance of Term2.

*The following properties hold globally:*

(`basic_props:native/1`)This predicate is understood natively by CiaoPP.

PREDICATEsubsumes_term/2

Usage:ISO`subsumes_term(Term1,Term2)`

Term2 is an instance of Term1.

PREDICATEmost_specific_generalization/3

Term satisfies `instance(Term1,Term)` and `instance(Term2,Term)` and there is no term less general than Term (modulo variants) that satisfies it.

PREDICATEmost_general_instance/3

Term satisfies `instance(Term,Term1)` and `instance(Term,Term2)` and there is no term more general than Term (modulo variants) that satisfies it.

REGTYPEunifier/1

unifier(Unifier) :- list(unifier_elem,Unifier).

Usage:`unifier(X)`

X is a unifier.

PREDICATEunifiable/3

Usage:`unifiable(X,Y,Unifier)`

Unifies Unifier with the most general unifier between the terms X and Y. Fails if such unifier does not exit.

*The following properties should hold at call time:*

(`basic_props:term/1`)X is any term.

(`basic_props:term/1`)Y is any term.*The following properties hold upon exit:*

(`terms_check:unifier/1`)Unifier is a unifier.

REGTYPEunifier_elem/1

A regular type, defined as follows:

unifier_elem(X=Term) :- var(X), term(Term).

*Packages:*`noprelude`,`initial`,`condcomp`,`assertions`,`assertions/assertions_basic`,`regtypes`,`nortchecks`.

Generated with LPdoc using Ciao