# `ShotDs.Data.Term`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/data/term.ex#L1)

Represents a Hol term as directed acyclic graph (DAG).

All terms contain a deterministic ID assigned by `ShotDs.Stt.TermFactory`.
Note that terms are in βη-normal form, i.e., fully β-reduced and η-expanded.

Besides the obvious fields `:head`, `:args` and `:type`, two accessor fields
are implemented for efficiency: `:fvars` contains all free variables
occurring in the term, `:max_num` represents the index of the highest bound
variable. Abstractions are identified by the `:bvars` field.

# `dummy_term_id`

```elixir
@type dummy_term_id() :: 0
```

Preliminary or dummy term IDs are assigned 0 as their ID. Those are never
present in an ETS table.

# `global_term_id`

```elixir
@type global_term_id() :: pos_integer()
```

Term IDs present in the global ETS table managed by `ShotDs.Stt.TermFactory`
are represented as positive integers.

# `local_term_id`

```elixir
@type local_term_id() :: neg_integer()
```

Term IDs that are only created and consumed locally and managed in a local
"scratchpad" ETS table are represented as negative integers.

# `t`

```elixir
@type t() :: %ShotDs.Data.Term{
  args: [term_id()],
  bvars: [ShotDs.Data.Declaration.t()],
  fvars: [ShotDs.Data.Declaration.t()],
  head: ShotDs.Data.Declaration.t(),
  id: term_id(),
  max_num: non_neg_integer(),
  type: ShotDs.Data.Type.t()
}
```

The type of a term. The fields `:id`, `:head` and `:type` are required.

# `term_id`

```elixir
@type term_id() :: global_term_id() | local_term_id() | dummy_term_id()
```

A term's id is given by an atomic positive (global) or negative (local)
integer where 0 denotes a dummy.

---

*Consult [api-reference.md](api-reference.md) for complete listing*