IBAFLang/IBAF-cbs/Funcons-beta/Computations/Normal/Generating/index.md

layout, title, parent, ancestor

layout	title	parent	ancestor
default	Generating	Normal	Funcons-beta

Funcons-beta : Generating.cbs

Generating

[
  Type   atoms
  Entity used-atom-set
  Funcon initialise-generating
  Funcon fresh-atom
  Funcon use-atom-not-in
]

Meta-variables
  T <: values

Built-in Type
  atoms

atoms is the type of values used as distinguishable tags. Notation for individual atoms is not provided.

Entity
  < _ , used-atom-set(_:sets(atoms)) > ---> < _ , used-atom-set(_:sets(atoms)) >

Built-in Funcon
  initialise-generating(_:=>T) : =>T

The initial value of the used-atom-set(SA) entity is unspecified. It could contains atoms that are reserved for internal use.

Funcon
  fresh-atom : =>atoms

fresh-atom computes an atom distinct from all previously computed atoms.

Rule
  element-not-in(atoms, SA) ~> A
  -----------------------------------------------
  < fresh-atom , used-atom-set(SA) > 
    ---> < A , used-atom-set(set-insert(A, SA)) >

Funcon
  use-atom-not-in(_:sets(atoms)) : =>atoms

use-atom-not-in(SA) computes an atom not in the set SA, and inserts it in the used-atom-set(SA′) entity, in case it was not previously used.

Rule
  element-not-in(atoms, SA) ~> A
  --------------------------------------------------------
  < use-atom-not-in(SA:sets(atoms)) , used-atom-set(SA′) >
    ---> < A , used-atom-set(set-insert(A, SA′)) >

---

From the PLanCompS Project | CBS-beta issues... | Suggest an improvement...