Term hierarchy

The :core module defines 2P-Kt's representation of logic data: Terms. This page is a precise, per-type description of that API, grounded in core/src/commonMain/kotlin/it/unibo/tuprolog/core/. See Term model for the design rationale (why terms are immutable, identity vs. structural equality, and so on) — this page sticks to what the API is.

Logic terms can be defined by the following context-free grammar (non-terminals in upper case):

Term	:=	Constant \| Var \| Struct
Constant	:=	Atom \| Numeric
Numeric	:=	Integer \| Real
Struct	:=	Functor(Argument, ...)
Var	:=	strings matching [A-Z_][A-Za-z_0-9]*
Atom	:=	strings matching [a-z][A-Za-z_0-9]*, or quoted strings
Functor	:=	a (non-quoted) atom, or an operator symbol

For example, f(X, y, g(1, 2.3), h(_, 'j k')) is a Struct with functor f and 4 arguments: the variable X, the atom y, the structure g(1, 2.3) (functor g, arguments the integer 1 and the real 2.3), and the structure h(_, 'j k') (arguments the anonymous variable _ and the quoted atom 'j k').

Diagram note

This diagram (migrated from 2P-Kt's older documentation) still labels the {}-functored term type Set / EmptySet. In current core, that type is named Block/EmptyBlock instead — see the Blocks section below. Every other type shown is up to date.

Term

 *
 * [Term]s are immutable tree-like data structures: there is no public API mutating a [Term] in place, only
 * ones (like [freshCopy] and [Applicable.apply]) that return a new [Term]. This is what lets terms be shared
 * freely between larger terms, knowledge bases, and concurrent computations without any risk of aliasing.
 *
 * [Term] also defines three, deliberately distinct, notions of equality — [equals] (identity-like, comparing

Term is the root of the hierarchy. It is Comparable<Term> (a total, implementation-defined standard order of terms, via TermComparator.DefaultComparator), Taggable<Term> (attach arbitrary tags: Map<String, Any> to a term, preserved across most transformations), Castable<Term> (as<T>() / castTo<T>() fluent down-casts) and Variabled (variables: Sequence<Var>, isGround: Boolean).

Terms are immutable: no subtype exposes a var property or a side-effecting method. All apparent "mutators" (e.g. Struct.setArgs, Clause.setBody) instead return a new term, leaving the receiver untouched.

Key members:

• variables: Sequence<Var> / isGround: Boolean — from Variabled.
• freshCopy(): Term / freshCopy(scope: Scope): Term — from Applicable<Term>; returns a structurally-equal term with all contained variables consistently renamed (same variable name ⇒ same renaming), reusing scope's variables when one is given.
• apply(substitution: Substitution): Term (and the term[substitution] operator alias) — from Applicable<Term>; replaces variables according to a Substitution.
• equals(other: Term, useVarCompleteName: Boolean): Boolean — identity check for which the caller decides whether two Vars are compared by completeName (default equals(Any?) behavior) or just by name.
• structurallyEquals(other: Term): Boolean — a looser equivalence: all variables are mutually equal, and numbers compare by value (1 structurallyEquals 1.0).
• accept(visitor: TermVisitor<T>): T — double-dispatch entry point for the visitor pattern (TermVisitor<T>).
• A family of isXxx: Boolean flags (isVar, isStruct, isAtom, isNumber, isList, isTuple, isBlock, isClause, isRule, isFact, isDirective, isIndicator, isTrue, isFail, ...), each guaranteed true iff the term is an instance of the corresponding subtype.
• A matching family of asXxx(): Xxx? (nullable down-cast) and castToXxx(): Xxx (throwing down-cast) methods, one per subtype, e.g. asAtom()/castToAtom(), asStruct()/castToStruct(), asRule()/castToRule().

    /**
     * Helper method aimed at down-casting [Term]s using a fluent style
     * @param T must be a subtype of [Term]
     * @return the current term, cast'd into type [T]
     * @throws ClassCastException if the current term is not of type [T]
     */
    @Suppress("RedundantOverride")
    override fun <T : Term> castTo(): T = super.castTo<T>()

    /**
     * Compares this term to the provided one, returning a positive integer if this term _precedes_ [other],
     * a negative integer if [other] precedes this term, or `0` otherwise
     * @param other is the term to be compared against this term
     * @return an [Int] indicating whether this term precedes [other] or not
     */
    override fun compareTo(other: Term): Int = TermComparator.DefaultComparator.compare(this, other)

    /**
     * Checks whether an[other] term is _equals_ to the current one or not,
     * by explicitly letting the client decide whether to rely or not on [Var]riables
     * complete names for checking equality among two [Var]iables.
     * If [useVarCompleteName] is `true`, [Var]iables are compared through their
     * [Var.completeName] property. Otherwise, they are compared through their
     * [Var.name] property. Other sorts of terms are compared as `Term.equals(Any?)`.
     *
     * For example, if [useVarCompleteName] is `true` the following comparison should fail:
     * ```
     * Var.of("X") == Var.of("X")
     * ```
     * otherwise, it should succeed.
     *
     * @param other is the [Term] the current [Term] should be compared with
     * @param useVarCompleteName indicates whether [Var] should be compared through their
     * [Var.completeName] property or through their [Var.name] property
     *
     * @return `true` if the two terms are equal, or `false`, otherwise
     */
    @JsName("equalsUsingVarCompleteNames")
    fun equals(
        other: Term,
        useVarCompleteName: Boolean,
    ): Boolean

    /**

There is no way to instantiate a bare Term: only its subtypes have public factory methods (documented below), or terms are built via a Scope, which also lets several terms share Var instances.

Term.toString() produces a raw, debug-oriented representation (not meant for end-user display): compound terms in canonical functor(arg1, ..., argN) form (quoting the functor when necessary), except lists ([a, b]), blocks ({a, b}), tuples ((a, b)), and clauses (Head :- Body, or :- Body for directives).

Var

/**
 * A logic variable, i.e. a placeholder for a [Term] that is yet to be determined.
 *
 * A [Var] is created out of a simple, human-readable [name] (e.g. `X`), but its real identity is its
 * [completeName], which pairs [name] with a hidden, per-name sequential [id]. This is why, perhaps
 * surprisingly, `Var.of("X") == Var.of("X")` is always `false`: each call mints a genuinely new variable, and
 * relying on the [name] alone for equality would make every clause containing a variable called `X`
 * accidentally alias every other clause using that same name. See the "Variables and Scoping" explanation
 * page in the project documentation for the full rationale.
 *
 * Because of this, code that needs to refer to *the same* variable more than once while building a term
 * (e.g. `member(H, [_|T]) :- member(H, T).`, where `H` and `T` each occur twice) should not call [Var.of]
 * repeatedly with the same name: doing so creates unrelated variables. Instead, either keep a single [Var]
 * reference around and reuse it, or use a [Scope], which caches variables by [name] and hands back the same
 * instance on repeated requests:
 * ```
 * Scope.of("H", "T") {
 *     ruleOf(structOf("member", varOf("H"), consOf(anonymous(), varOf("T"))), structOf("member", varOf("H"), varOf("T")))
 * }
 * ```
 *
 * The [anonymous] variable (conventionally named `_`) is the deliberate exception to variable reuse: every
 * call to [anonymous] (or [Var.anonymous]) produces a fresh, unrelated variable, matching Prolog's convention
 * that `_` never binds to anything meaningful shared across occurrences.
 *
 * @see Scope

Vars are placeholders for other terms. Each has a complete name <name>_<id>, where name is the (simple, user-facing) name: String and id: String is an implementation-chosen suffix guaranteed to make completeName globally unique; two variables are equals() only if their complete names match.

• isAnonymous: Boolean — true iff name == "_".
• isNameWellFormed: Boolean — true iff name matches [A-Z_][A-Za-z_0-9]* (Var.NAME_PATTERN). Non-well-formed names can still be instantiated; they are printed back-quoted (`name`_id).
• Var.of(name: String): Var and Var.anonymous(): Var are the only two factories; both always mint a fresh, never-before-seen variable — callers have no control over id. To reuse a variable, hold on to the Var instance, or use a Scope.

Constant

/**
 * Base type for [Term]s that carry a single, immutable, ground [value] and no sub-terms: [Atom]s (a [String]
 * value) and [Numeric]s (an [Integer]/[Real] value). Constants are always ground, since they contain no
 * [Var]iables.
 */
interface Constant : Term {
    override val isConstant: Boolean get() = true

    /** The (platform-native) value wrapped by this constant, e.g. a [String] for [Atom]s. */
    @JsName("value")
    val value: Any

Constants are ground, non-compound terms characterized by a value: Any. They cannot be instantiated directly — only through the Atom/Numeric factories below.

Numeric

/**
 * Base type for numeric [Constant]s, i.e. Prolog numbers.
 *
 * [Numeric] splits into two disjoint sub-types, [Integer] and [Real], because Prolog itself distinguishes
 * integers from floating-point numbers both syntactically (`1` vs `1.0`) and semantically (arithmetic
 * built-ins like `//` vs `/` behave differently depending on the operand types, and ISO term ordering treats
 * "value-equal" integers and reals as distinct terms unless [structurallyEquals][Term.structurallyEquals] is
 * used). Client code that only cares about "some number" can program against [Numeric] and use [decimalValue]
 * / [intValue] / [compareValueTo] to compare or convert regardless of which concrete sub-type is involved;
 * code that must preserve or check Prolog's integer/float distinction should use [Integer] or [Real] directly.
 *
 * New [Numeric] instances are best created through the factory methods in this companion (which pick the
 * most appropriate sub-type automatically), or directly via [Integer.of] / [Real.of] when the desired
 * sub-type is already known.
 */
interface Numeric : Constant {
    override val isNumber: Boolean
        get() = true

    override val variables: Sequence<Var>
        get() = emptySequence()

Numeric is either an Integer or a Real. Numbers are backed by the arbitrary-precision, Kotlin-multiplatform org.gciatto.kt.math.BigInteger/BigDecimal (not java.math, so the same code runs on JVM and JS): intValue and decimalValue expose both views regardless of the concrete subtype, and compareValueTo(other) compares by numeric value (so Numeric also gets <, <=, >, >= via Kotlin operator overloading). value: Any returns whichever of BigInteger/BigDecimal is the natural representation.

Factories: Numeric.of(value: Number), Numeric.of(value: String) (tries Integer.of first, falls back to Real.of), plus the type-specific Integer.of(...) (from Int/Long/Short/Byte/BigInteger/BigDecimal, or String with an optional radix) and Real.of(...) (from Float/Double/BigDecimal/String).

Struct

    @JsName("insertAt")
    fun insertAt(
        index: Int,
        argument: Term,
    ): Struct

    /**
     * Creates a novel [Struct] which is a copy of the current one, expect that is has a different functor.
     * @param functor is a [String] representing the new functor
     * @return a new [Struct], whose functor is [functor], and whose [arity] and arguments list are equal
     * to the current one
     */
    @JsName("setFunctor")
    fun setFunctor(functor: String): Struct

    /**
     * The functor of this [Struct].
     */
    @JsName("functor")
    val functor: String

    /**
     * Returns `true` if and only if [functor] matches [Struct.WELL_FORMED_FUNCTOR_PATTERN].
     */
    @JsName("isFunctorWellFormed")
    val isFunctorWellFormed: Boolean

    /**
     * The total amount of arguments of this [Struct].
     * This is equal to the length of [args].
     */
    @JsName("arity")
    val arity: Int
        get() = args.size

    /**
     * The indicator corresponding to this [Struct], i.e. [functor]/[arity].
     */
    @JsName("indicator")
    val indicator: Indicator
        get() = Indicator.of(functor, arity)

    /**
     * List of arguments of this [Struct].
     */
    @JsName("argsList")
    val args: KtList<Term>

    /**
     * Sequence of arguments of this [Struct].
     */
    @JsName("argsSequence")
    val argsSequence: Sequence<Term>
        get() = args.asSequence()

    /**
     * Gets the [index]-th argument if this [Struct].
     * @param index is the index the argument which should be retrieved
     * @throws IndexOutOfBoundsException if [index] is lower than 0 or greater or equal to [arity]
     * @return the [Term] having position [index] in [args]
     */
    @JsName("getArgAt")
    fun getArgAt(index: Int): Term = args[index]

    /**
     * Creates a novel [Struct] which is a copy of the current one, except that its [args] are replaced by [args].
     * @return a new [Struct], whose [functor] equals the current one, and whose arguments are [args]

Structs are compound terms: a functor: String plus an ordered list of args: List<Term> (arity: Int of them). Every non-Var, non-Numeric term in 2P-Kt — atoms, lists, tuples, blocks, indicators, clauses — is ultimately a Struct. Besides setArgs/setFunctor (which, like every "setter" in the hierarchy, return a new Struct rather than mutating), Struct also has append/addFirst/addLast/insertAt to build a new Struct with one extra argument. indicator: Indicator is a shorthand for Indicator.of(functor, arity). Construct one with Struct.of(functor: String, vararg args: Term).

Atom

Atoms are Structs of arity 0 that are simultaneously Constants: value: String and functor always coincide. They are how bare strings/symbols are represented. Atom.of(value: String) is the factory — note that it interns a few well-known values to specific subtypes ("[]" → EmptyList, "{}" → EmptyBlock, "true" / "fail" / "false" → Truth).

Truth

/**
 * An [Atom] representing one of Prolog's canonical boolean values: `true`, `fail`, or `false`.
 *
 * [Truth] exists mostly so that resolution/solving code (in downstream modules) can recognize and construct
 * these three atoms without comparing raw strings; [TRUE], [FAIL], and [FALSE] are the only three [Truth]
 * instances, and [Atom.of] automatically returns one of them whenever its argument matches one of the three
 * corresponding functors, so most client code never needs to reach for [Truth] directly.
 */
interface Truth : Atom {
    /** `true` for [TRUE], `false` for both [FAIL] and [FALSE]. */
    override val isTrue: Boolean

    override val isFail: Boolean
        get() = !isTrue

Truth is the Atom subtype for the three boolean-ish atoms ISO Prolog treats specially: Truth.TRUE ("true"), Truth.FAIL ("fail"), and Truth.FALSE ("false") — the latter two both count as isFail. Truth.of(Boolean) maps true/false to TRUE/FALSE.

Indicator

interface Indicator : Struct {
    override val isIndicator: Boolean
        get() = true

    override val functor: String
        get() = INDICATOR_FUNCTOR

    override val arity: Int
        get() = 2

    /** The indicated functor name Term */
    @JsName("nameTerm")
    val nameTerm: Term

    /** The indicated functor arity Term */
    @JsName("arityTerm")
    val arityTerm: Term

    /**
     * Whether this Indicator is well-formed
     *
     * An indicator is well-formed when:
     * - its [nameTerm] is an [Atom]
     * - its [arityTerm] is a non-negative [Integer]
     */
    @JsName("isWellFormed")
    val isWellFormed: Boolean
        get() = nameTerm.isAtom && arityTerm.let { it.isInteger && it.castToInteger().intValue.signum >= 0 }

An Indicator denotes a predicate/functor by name and arity, e.g. foo/2: a Struct with functor / and two arguments, nameTerm/arityTerm (kept as generic Terms so a partially-instantiated indicator can exist). isWellFormed holds when nameTerm is an Atom and arityTerm a non-negative Integer, in which case indicatedName: String?/indicatedArity: Int? extract the concrete values. Build one via Indicator.of(name: String, arity: Int) or the generic Indicator.of(name: Term, arity: Term).

Collections

List, Tuple, and Block are the three "collection-like" Structs. All three implement Recursive, which gives them a uniform way to view their elements:

/**
 * Base type for [Struct]s that conventionally represent a (possibly improper) sequence of [Term]s folded
 * into nested binary structures: [List] (functor `.`), [Tuple] (functor `, `), and [Block] (functor `{}`).
 * [Recursive] exposes that sequence uniformly, regardless of which folding convention the concrete sub-type
 * uses, via [unfold]/[unfoldedSequence]/[toList]/[toArray].
 */
interface Recursive : Struct {
    override val isRecursive: Boolean
        get() = true

    override fun asRecursive(): Recursive = this

    /** The elements of this structure, unfolded lazily, in order. Same as [unfold]. */
    @JsName("unfoldedSequence")
    val unfoldedSequence: Sequence<Term>

    /** The elements of this structure, unfolded eagerly into a [List]. */
    @JsName("unfoldedList")
    val unfoldedList: List<Term>

    /** The elements of this structure, unfolded eagerly into an [Array]. */
    @JsName("unfoldedArray")
    val unfoldedArray: Array<Term>

    /** The number of elements in this structure, once unfolded. */
    @JsName("size")
    val size: Int

    /** Alias for [unfoldedSequence], exposed as an [Iterable]. */
    @JsName("items")
    val items: Iterable<Term>

    /** Eagerly unfolds this structure's elements into an [Array]. Same as [unfoldedArray]. */
    @JsName("toArray")
    fun toArray(): Array<Term>

Lists

A List is either an EmptyList (the atom []) or a Cons — a Struct with functor . and 2 arguments, head: Term and tail: Term, usually written [Head | Tail]. A List is isWellFormed when it is []- terminated (a well-formed, Cons-chained list prints without a |, e.g. [1, b, 3]; a non-well-formed one prints [1, b | T]). Factories: List.of(vararg items), List.of(items: Iterable<Term>), List.from(items, last) (to build an explicitly last-terminated, possibly non-well-formed list), Cons.of(head, tail), Cons.singleton(head), and List.empty() / Empty.list().

Tuples

A Tuple is a Struct with functor , and 2 arguments, left/right, usually written (Left, Right). When right is itself a Tuple, the whole chain prints as one comma-separated, parenthesized sequence, e.g. (a, 2, c) for ','(a, ','(2, c)). Tuples always have 2 or more elements — there is no empty or singleton tuple. Build one with Tuple.of(left, right), Tuple.of(items: Iterable<Term>) (requires at least 2), or Tuple.wrapIfNeeded(...), which collapses to the single element itself (or a caller-supplied fallback) when fewer than 2 items are given.

Blocks

A Block is a Struct with functor {} and either 0 arguments (EmptyBlock, the atom {}) or exactly 1 argument (usually itself a Tuple, when the block groups several terms), usually written {Argument}. This is 2P-Kt's representation of Prolog's curly-brace term ('{}'/1), e.g. {a, 2, c} for '{}'(','(a, ','(2, c))). Build one with Block.of(vararg terms) / Block.of(terms: Iterable<Term>) (collapsing to EmptyBlock for zero terms, or wrapping 2+ terms in a Tuple), or Block.empty() / Empty.block().

Note

Earlier versions of this documentation (and the overview diagram near the top of this page) call this type Set/EmptySet. It is not set-semantics (no deduplication) — it is a generic curly-brace grouping term, and the current source names it Block/EmptyBlock (it.unibo.tuprolog.core.Block).

Clauses

Clause, Rule, Fact, and Directive represent Horn clauses. All share functor :-:

/**
 * A logic clause, i.e. a [Struct] with functor `:-`, representing either a [Rule] (`head :- body`, [head]
 * non-`null`) or a [Directive] (`:- body`, [head] `null`). A theory (see `:theory`) is, at its core, a
 * sequence of [Clause]s.
 *
 * [Clause.of] is the general entry point for building either kind, dispatching on whether [head] is `null`;
 * reach for [Rule.of], [Fact.of], or [Directive.of] directly when the desired kind is already known.
 */
interface Clause : Struct {
    override val functor: String
        get() = CLAUSE_FUNCTOR

    /** The head of this clause, or `null` if this is a [Directive]. */
    @JsName("head")
    val head: Struct?

    /** The body of this clause: a single goal, or a right-nested [Tuple] of goals if there is more than one. */
    @JsName("body")
    val body: Term

    /**
     * Checks whether this [Clause] is well-formed.
     *
     * A [Clause] is well-formed if and only if:
     * - its [head] is neither a [Numeric] nor a [Var] (when non-`null`);
     * - its [body] is not a [Numeric], nor does it contain one as a direct argument of a `, `/2, `;`/2, or
     *   `->`/2 structure (see [notableFunctors]).
     */
    @JsName("isWellFormed")
    val isWellFormed: Boolean

    override val arity: Int
        get() = (if (head === null) 1 else 2)

    override val isClause: Boolean
        get() = true

    override val isRule: Boolean

• A Directive has no head: ':-'(Body) (head == null, arity 1), printed :- Body.

• A Rule has a head: ':-'(Head, Body) (arity 2), printed Head :- Body. head: Struct is non-nullable on Rule (narrowing Clause.head: Struct?).

• A Fact is a Rule whose body is true: ':-'(Head, true), printed just as Head. Fact.of(head: Struct) is the factory; body is fixed to Truth.TRUE.

Clause.isWellFormed additionally checks that neither the head nor the body (nor its ,/;/->-connected sub-terms) contain a bare Numeric where a goal/argument is expected. Beyond head/body, Clause (and its Rule/Fact narrowings) expose a family of head/body "wither" methods that return a new clause rather than mutating — setHead/setBody, setHeadArgs/setBodyItems, insertHeadArg/insertBodyItem, add{First,Last}HeadArg/add{First,Last}BodyItem — plus bodyItems/bodySize/bodyAsTuple/getBodyItem(index) to navigate a (possibly Tuple-shaped) body without manual unwrapping. Build clauses with Clause.of(head?, vararg body), Rule.of(head, vararg body), or Directive.of(vararg body).