🚀 go-pugleaf

In article <BtyBLw.42q@dcs.glasgow.ac.uk> areid@dcs.glasgow.ac.uk (Alastair
Reid) writes:
>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.
>

I don't know the particular paper either.

The constructivists have confronted the problem of empty carriers, and I
believe the solution suggested here would not satisfy them because of the way
the definition relies on knowing whether A_s is empty or not. (Remember that
constructively you don't have excluded middle. Also, there are questions of
whether "A non-empty" means that you can explicitly give an element of A, or
you can prove that one exists, or merely that it is impossible for A not to
have any elements.)

The problems associated with empty carriers are not essentially ones of
constructivity, but all the same the constructivist solution is worth knowing
about.

They drop the idea that a valuation should try to assign values to _all_
variables; after all, any particular axiom (equation or sequent) whose
satisfaction is being checked only uses finitely many. They explicitly label
each axiom with a finite set of variables, including all those free in the
axiom but possibly also some extra unused variables, and require that the axiom
should hold for every valuation _defined on that set_.

The trick comes in the way the proof rules handle these variable sets. You are
allowed to expand the set as much as you like, but you can't in general drop
variables from the set even if some logical reasoning has lost them from the
axiom - they are then considered unused but still present.

Here is an example that I got from Harry Simmons via John Tucker.

Consider a theory with two sorts, s and t, two constants a and b of sort t, and
a unary operator f: s -> t. Consider also two axioms

  a = f(x)
  f(x) = b

A simple application of transitivity gives a = b, but this is false in the
initial model M (which has empty carrier for s and a doubleton {a,b} for t).

With the labels, however, we must write

  f(x) =_{x} a
  f(x) =_{x} b

from which transitivity gives

  a =_{x} b

You can read this as "a = b in the presence of x". In the initial model it is
vacuously true that for every valuation on {x} (there are none) we have a = b.
Unrestricted equality between a and b would be a =_{} b, which - fortunately -
we can't deduce.

I wish I had a reference for this idea, but I'm afraid I've forgotten where I
saw it - perhaps someone can help me.

Steve Vickers.

In article <BtyBLw.42q@dcs.glasgow.ac.uk> areid@dcs.glasgow.ac.uk (Alastair
Reid) described an idea for avoiding the paradoxes associated with empty
carriers for many-sorted algebras, and I posted a reply describing the
constructivists' technique of attaching finite sets of variables to equations
or sequents.

I said that I didn't know of a reference for the technique, but I've now found
that it is described quite straightforwardly in Lambek and Scott's book
"Introduction to Higher Order Categorical Logic", section II.1. In their
historical comments, they attribute it to Mostowski (1951).

Steve Vickers

In article <BtyBLw.42q@dcs.glasgow.ac.uk> areid@dcs.glasgow.ac.uk
(Alastair Reid) writes:

   [Problem: with the usual definition of valuation, there are no
   valuations if a carrier of a many-sorted algebra is empty]

This problem can be solved quite elegantly by requiring a valuation to
be defined on the free variables of a term or formula, rather than on
all variables.

In a recent paper (available by FTP, see below), I used the following
definitions:

   (The notation ``\dom f'' denotes the domain, ``\ran f'' the range
   of a function, ``FV(t)'' the set of freee variables of a term or
   formula.  By convention, S is the set of sorts of a signature
   \Sigma)

   Definition (assignment)

   Let a signature \Sigma and a \Sigma-algebra A be given.  An
   \em{assignment} into A is an S-sorted mapping a that satisfies 
   \ran a_s \subset A_s for all s \in S.  If X is an S-sorted set such
   that X_s \subset \dom a_s for all s \in S, we write ``a: X ~~> A''.
 
   Definition (evaluation of terms)

   Let \Sigma be a signature and let A be a \Sigma-algebra.  By
   induction on \Sigma-terms, we define for each term t an
   \df{evaluation function}

      t_A: { a: FV(t) ~~> A } --> A_s,   where s is the sort of t:

   (follows the usual definition)

   Definition (satisfaction of formulas)

   Let \Sigma be a signature and let M be a \Sigma-algebra.  The
   notation ``M \sat \phi[a]'' will mean that M \em{satisfies} the
   formula \phi under the assignment a: FV(\phi) ~~> M.  The
   satisfaction relation is defined inductively:

   (follows the usual definition)

This way, closed formulas get the right semantics, even if they
involve quantification over empty carriers.  I have not thought about
proof systems.  My feeling is that empty carriers should be accepted
as natural and not be shied away from.

The paper from which this is taken does not deal specifically with
empty carriers, but shows that first-order logic cannot specify
behavioural equivalence classes of algebras:

  ``Two Impossibility Theorems on Behaviour Specification of Abstract
  Data Types''

  (to appear in Acta Informatica)

  available by anonymous FTP from 
  flop.informatik.tu-muenchen.de (131.159.8.35)

        798  Aug 28 15:01  /pub/theory/schoett/README
      67393  Aug 21 11:35  /pub/theory/schoett/imposs.dvi.Z
     120179  Aug 21 11:39  /pub/theory/schoett/imposs.ps.Z


Oliver Schoett     Inst. f. Informatik (H2), Technische Univ. M"unchen
                   Postfach 20 24 20,     8000 M"unchen 2,     Germany
schoett@informatik.tu-muenchen.de    phone +49 89 2105-2399  fax -8207