Bestfitting simplified

With the simplification of contexts, bestfitting becomes simpler as well, as does the semantics for identifiers in expressions.

An equation q is, conceptually, a triple (xq, Kq, Eq), where xq is the variable being defined, Kq is the set of contexts where the equation is valid, and Eq is the defining expression.

Given two equations q and q’, we write q ⊂ q’ if xq = xq’ and Kq ⊃ Kq’.

If we have a set of equations σ, then best(σ) consists of the bestfit equations in σ , i.e.,

best(σ) = {q ∊ σ | ∄ q' ∊ σ. q ⊂ q'}

The restriction of a set of equations σ to an identifier x and a context κ is written

σ|xκ = {q ∊ σ | x = xq and κ ∊ Kq}

We can now write the semantics for identifiers in equations.

⟦x⟧σκ =
let {q1, ..., qn} = best(σ|xκ) in
let vi = ⟦Eqi⟧σκ in
v1 ⊕ ⋯ ⊕ vn

where ⊕ is the combining operator. The simplest combining operator checks that all of its arguments are identical, and returns that value. In the general language, each identifier could have its own combining operator, which could be any commutative, associative operator.

Advertisement