# Term representations¶

## Rationale¶

The new version of Logtk attemps to reduce code duplication by using a single
core representation for scoped terms, which is `ScopedTerm`

. A second representation,
`PrologTerm`

, is used for simple AST representation and manipulation, and
is a bit the dual of `ScopedTerm`

.

`ScopedTerm`

‘s goal is to centralize all hashconsing, comparison, De Bruijn
indices manipulations, etc. in a single representation. As a consequence,
substitutions (`Substs`

) and unification (`Unif`

) are defined only once,
and work on scoped terms.

## Specialized Representations¶

`ScopedTerm`

is nice, but it hardly represents any usual structure, because
it is too general. To enforce structural invariants, check types, and provide
a more specific view of an algebraic structure, we use a nice feature of
OCaml called **private aliases**.

For instance, `Type`

is a representation of polymorphic simple types.
The type `Type.t`

is declared as

```
type t = private ScopedTerm.t
```

which means that a `Type.t`

is a subtype of `ScopedTerm.t`

. Then, functions
like `Type.view : Type.t -> Type.view`

(a specific variant) or
`Type.of_term : ScopedTerm.t -> Type.t option`

can be used. Special
constructors like `var : int -> Type.t`

are also provided and directly
provide instances of `Type.t`

that have some structural constraints enforced.

Every specialized representation has its own `kind`

, a tag that allows to
check in constant-time whether a `ScopedTerm.t`

actually is a `Type.t`

or not.

## Hierarchy¶

`ScopedTerm`

hashconsed terms with scoping and De Bruijn indices for bound variables. Almost every term has a “type”, that is itself a term (theoretically it should be possible to use this representation for calculus of construction)`FOTerm`

first-order terms, as usual. No binder, no magic.`HOTerm`

higher-order terms with lambdas, multisets and records.`Type`

polymorphic types.`Formula`

formulas parametrized on the terms that represent atoms.`Formula.FO`

is an instance that has`FOTerm.t`

as terms

`PrologTerm`

terms with named variables, no hashconsing, and not much typing.