Equational correspondence and equational embedding

Equational correspondence and equational embedding

[Philip Wadler]

The notion of *equational correspondence* was defined by Sabry and
Felleisen in their paper:

    Amr Sabry and Matthias Felleisen
    Reasoning about programs in continuation-passing style
    LISP and Symbolic Computation, 6(3--4):289--360, November 1993.

We lay out below the definition, along with a related notion of
*equational embedding*.  We've seen relatively little about equational
correspondence in the literature, and nothing about equational
embedding.  Given that these seem to be fundamental concepts, we
suspect we've been looking in the wrong places.  Any pointers to
relevant literature would be greatly apprectiated.

An *equational theory* T is a set of terms t of T, and a set of equations
t =_T t' (where t, t' are terms of T).

Let S, T be equational theories.  We say that f : S -> T and g : T -> S
constitute an *equational correspondence* between S and T if

   1.  g(f(s)) =_S s,  for all terms s in S
   2.  f(g(t)) =_T t,  for all terms t in T
   3.  s =_S s'  implies  f(s) =_T f(s'),  for all terms s, s' in S
   4.  t =_T t'  implies  g(t) =_S g(t'),  for all terms t, t' in T

Let S, T be equational theories.  We say that f : S -> T and
g : f(S) -> S (where f(S) is the image of S under f, a subset of T)
constitute an *equational embedding* between S and T if

   1.  g(f(s)) =_S s,  for all s in S
   2.  s =_S s'  implies  f(s) =_T f(s'),  for all s, s' in S

It is easy to see that there is an equational embedding of S into T if
and only if there is a function from S to T that preserves and
reflects equations.

Clearly, f and g constitute an equational correspondence between S and
T if f and g constitute an equational embedding of S into T and g and
f constitute an equational embedding of T into S.

We conjecture that whenever there is an equational embedding of S into
T and of T into S that there is an equational correspondence between S
and T.  This is not immediate, because one equational embedding might
be given by f and g and the other by h and k, with no obvious relation
between the two.

As I said, any pointers to relevant literature would be greatly
appreciated!

Yours,  -- Sam Lindley, Philip Wadler, Jeremy Yallop

-- 
  \ Philip Wadler, Professor of Theoretical Computer Science
  /\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: Equational correspondence and equational embedding

[Janus]

Dear Prof. Waddler,

   I don't know if the following proof is correct, please, let me know
if I made any mistake:

   By hypothesis there exists k:S->T and h:k(S)->S such that h(k(S))
=_S s for all s in S and s =_S s' implies k(s) =_T k(s') for all s, s'
in S
   On the other hand, there exists f:T->S and g:f(T)->S such that
g(f(t)) =_T t for all t in T and t=_T t' implies f(t) =_S f(t') for
all t, t' in T

   Assume that there exists t in T\k(S) => |T| > |S| because k is
injective and S = dom(k). Hence, there exists t' not equal to t such
that f(t) =_S f(t') which is absurdum.

   So, there not exists t in T\k(S), then T = k(S). So, k and k^-1
constitutes an equational correspondence.

   Yours,
     Alejandro

-- 
Alejandro Díaz-Caro
Homepage: http://www.fceia.unr.edu.ar/~diazcaro
Weblog: http://computacioncuantica.exactas.org

Re: Equational correspondence and equational embedding

[Robin Houston]

To my category-infected mind, it seems that what you really need
is a little category theory. :-)

I take it that your equations should define an equivalence relation?
(It seems strange to call them 'equations' if not.) If that's right,
then an "equational theory" is the same thing as an essentially-discrete
category, i.e. a category that is equivalent to a discrete one, and
an "equational correspondence" is an equivalence of categories.

With the definition of "equational embedding" you give, your
conjecture is false. For example, let the equational theories
S and T each have two terms x and y, with equations

 x =_S x     y =_S y    x =_S y
 x =_T x     y =_T y

We can define an equational embedding S -> T by mapping both
terms to x, and we can define an equational embedding T -> S
by mapping x to x and y to y, but there can be no equational
correspondence between S and T (since 1 != 2).

It would seem more natural, at least from a categorical point
of view, to define an equational embedding to be a full functor,
i.e. a function f: S -> T such that

   s =_S s'  iff  f(s) =_T f(s').

With that definition, your conjecture is true by the
Schröder-Bernstein theorem.

Robin

Re: Equational correspondence and equational embedding

[Matthias Felleisen]

Phil, Amr responded with the bare facts. Here is my path of
discovery, with two additional lit ptrs:

John Gately was an MS student at IU working in Indiana. I suggested
to him that he work out a cbv theory of combinators in the spirit of
Gordon Plotkin's CBN/CBV paper in TCS(1974). I also suggested that he
read Barendregt (chapter 7, with an overview in chapter 2) because it
summarizes the equational correspondence I was after. John dropped
out from IU but rejoined me at Rice and published a paper on his CBV
CL ~ lambda_v correspondence paper at some workshop (mathematical
foundations of programming languages?).

Around the same time, I started Eric Crank on a correspondence
between cps(\lambda_v) and lambda with the hope that a reduction rule
Bruce Duba and I had played with since 1985: (\x.E[x]) M  = E[M] for
x not in fv(E) [beta_Omega]. While Eric preferred to switch to
equational characterizations of imperative parameter passing, Amr
came along and solved this puzzle.

As Amr said, we tried to stay as close as possible to the source
(Curry) with our write-up for LFP 1992.

-- Matthias


On Apr 15, 2008, at 8:07 AM, Philip Wadler wrote:
> The notion of *equational correspondence* was defined by Sabry and
> Felleisen in their paper:
>
>    Amr Sabry and Matthias Felleisen
>    Reasoning about programs in continuation-passing style
>    LISP and Symbolic Computation, 6(3--4):289--360, November 1993.
>
> We lay out below the definition, along with a related notion of
> *equational embedding*.  We've seen relatively little about equational
> correspondence in the literature, and nothing about equational
> embedding.  Given that these seem to be fundamental concepts, we
> suspect we've been looking in the wrong places.  Any pointers to
> relevant literature would be greatly apprectiated.
>
> An *equational theory* T is a set of terms t of T, and a set of
> equations
> t =_T t' (where t, t' are terms of T).
>
> Let S, T be equational theories.  We say that f : S -> T and g : T -
> > S
> constitute an *equational correspondence* between S and T if
>
>   1.  g(f(s)) =_S s,  for all terms s in S
>   2.  f(g(t)) =_T t,  for all terms t in T
>   3.  s =_S s'  implies  f(s) =_T f(s'),  for all terms s, s' in S
>   4.  t =_T t'  implies  g(t) =_S g(t'),  for all terms t, t' in T
>
> Let S, T be equational theories.  We say that f : S -> T and
> g : f(S) -> S (where f(S) is the image of S under f, a subset of T)
> constitute an *equational embedding* between S and T if
>
>   1.  g(f(s)) =_S s,  for all s in S
>   2.  s =_S s'  implies  f(s) =_T f(s'),  for all s, s' in S
>
> It is easy to see that there is an equational embedding of S into T if
> and only if there is a function from S to T that preserves and
> reflects equations.
>
> Clearly, f and g constitute an equational correspondence between S and
> T if f and g constitute an equational embedding of S into T and g and
> f constitute an equational embedding of T into S.
>
> We conjecture that whenever there is an equational embedding of S into
> T and of T into S that there is an equational correspondence between S
> and T.  This is not immediate, because one equational embedding might
> be given by f and g and the other by h and k, with no obvious relation
> between the two.
>
> As I said, any pointers to relevant literature would be greatly
> appreciated!
>
> Yours,  -- Sam Lindley, Philip Wadler, Jeremy Yallop
>
> --
>  \ Philip Wadler, Professor of Theoretical Computer Science
>  /\ School of Informatics, University of Edinburgh
> /  \ http://homepages.inf.ed.ac.uk/wadler/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>