🚀 go-pugleaf

I'm looking for a paper I skimmed a few months ago but failed to take
a proper note of its location. I thought it was published in a recent
volume of LNCS but checking likely candidates for the last five years
failed to refind it.

The paper suggested a slightly different definition of "valuations."

  The usual definition of a valuation is something like:

    A valuation v:X->A is a family of indexed functions v_s : X_s -> A_s
    which assign a value from A_s (the set of values of sort s in an
    algebra A) to variable symbols taken from X_s.

  If A_s is empty, no value can be assigned to variables from X_s and
  (assuming X_s to be non-empty), no valuation exists.

  From memory, the definition in the paper differed as follows:

    Instead of requiring that v_s(x) (the value assigned to a variable
    x of sort s by a valuation v : X -> A) must always be defined, the
    paper required that:

      v_s(x) is undefined,  if A_s is empty; and
      v_s(x) \in A_s,       if A_s is non-empty.

  This second definition ensures that valuations v : X -> A exist even
  if A does have empty carrier sets and avoids the need for a lot of
  shenanigans in the definition of evaluation of a term, satisfaction
  of a formula and observational equivalence wrt a set of free
  variables.

Any help in finding this paper would be greatly appreciated.

--
Alastair Reid, Computing Science Department, Glasgow University, rm G091,
17 Lilybank Gardens, Glasgow G12 8QQ, SCOTLAND. Work:no phone;home:041 334 3048
JANET: areid@dcs.glasgow.ac.uk   BANG!net: via mcsun and ukc  FAX: 041 330 4913
INTERNET: via nsfnet-relay.ac.uk  BITNET: via UKACRL   UUCP: areid@glasgow.uucp
-- 
Alastair Reid, Computing Science Department, Glasgow University, rm G091,
17 Lilybank Gardens, Glasgow G12 8QQ, SCOTLAND. Work:no phone;home:041 334 3048
JANET: areid@dcs.glasgow.ac.uk   BANG!net: via mcsun and ukc  FAX: 041 330 4913