env: Variable

This is a class that defines instances of logical variables. It is one of the major parts of the unification process and logical solvers.

Variable is based on Unifier and provides a useful helpers to deal with environments (see Env for more details).

It is defined in env and can be accessed like that:

import {Variable} from 'deep6/env.js';

Usually a helper factory function is used to create instances of Variable: variable().

Introduction

Let's redo the example from Env:

const env = new Env(),
  a = new Variable('a'), // can be accessed as 'a'
  b = new Variable(),    // anonymous
  c = new Variable();    // anonymous

a.isBound(env); // false
b.isBound(env); // false
c.isBound(env); // false

// push a generation frame
env.push();

env.bindVal(a.name, 1);

a.isBound(env); // true
b.isBound(env); // false
c.isBound(env); // false

a.get(get);     // 1

// push a generation frame
env.push();

a.isBound(env); // true
b.isBound(env); // false
c.isBound(env); // false

env.bindVar(c.name, b.name);

a.isBound(env); // true
b.isBound(env); // false
c.isBound(env); // false

env.isAlias(a, b); // false
env.isAlias(b, c); // true
env.isAlias(c, a); // false

a.isAlias(b, env); // false
b.isAlias(c, env); // true
c.isAlias(a, env); // false

env.bindVal(b.name, 2);

a.isBound(env); // true
b.isBound(env); // true
c.isBound(env); // true

a.get(env);     // 1
b.get(env);     // 2
c.get(env);     // 2

// drop a generation frame
env.pop();

a.isBound(env); // true
b.isBound(env); // false
c.isBound(env); // false

All attributes (bound, aliased) are recorded in an environment, not in a variable itself. It allows using the same variable object with different environments at the same time.

const x = new Variable(),
  env1 = new Env(),
  env2 = new Env();

x.isBound(env1); // false
x.isBound(env2); // false

env1.bindVal(x.name, 1);

x.isBound(env1); // true
x.isBound(env2); // false

x.get(env1); // 1

env2.bindVal(x.name, 'two');

x.isBound(env1); // true
x.isBound(env2); // true

x.get(env1); // 1
x.get(env2); // 'two'

Class Variable

This class defines objects with the following properties:

• name — a string or a symbol that is unique for this logical variable.
  • It is possible to create several instances of Variable with the same name. In this case, logically it will be the same logical variable.

The class defines the following methods:

constructor([name])

The constructor creates a logical variable with a given name. It takes the following arguments:

• name — an optional string or a symbol value that is unique for this logical variable. If it is not supplied or falsy (an empty string), a unique symbol value is generated.
  • This value is stored as name property so it can be accessed later.

isBound(env)

It is a convenience method that corresponds to env.isBound(name). The method returns a truthy value if a variable is already bound to a value. Computationally it is very cheap (O(1)). It takes the following arguments:

• env — an environment object (see Env).

The current implementation:

isBound(env) {
  return this.name in env.values;
}

isAlias(name, env)

It is a convenience method that corresponds to env.isAlias(name1, name2). The method returns a truthy value if variables are already aliased to each other. Computationally it is very cheap (O(1)). It takes the following arguments:

• name — a variable name as a string or a symbol or a Variable object.
• env — an environment object (see Env).

The procedure is completely symmetric:

const x = new Variable(),
  y = new Variable(),
  env = new Env();

env.bindVar(x.name, y.name);

x.isAlias(y, env); // true
y.isAlias(x, env); // true

The current implementation:

isAlias(name, env) {
  const u = env.variables[this.name];
  return u && u[name instanceof Variable ? name.name : name] === 1;
}

get(env)

It is a convenience method that corresponds to env.get(name). The method returns a value bound to a variable. Computationally it is very cheap (O(1)). It takes the following arguments:

• env — an environment object (see Env).

No checks are done that the variable is bound. Correctness checks should be done externally before calling the method. If a variable is not bound in the environment, get() will return undefined.

Example:

const a = new Variable();
const value = 1; // some arbitrary value
env.bindVal(a.name, value);
a.get(env) === value; // true

The current implementation:

get(env) {
  return env.values[this.name];
}

unify(val, ls, rs, env)

This method is required by Unifier and used internally.

The unification algorithm for a variable:

1. If the variable is bound, we unify its value with val, by pushing them to the ls-rs pair.
2. If val is any, it is unified unconditionally.
3. If val is another variable:
   1. If it is bound, we bind the variable to that value.
   2. Otherwise, we bind these two variables making them aliased.
4. Bind the variable to val.

In all cases, the actual unification is delegated through the ls-rs pair, and the method returns true.