From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4365 Path: news.gmane.org!not-for-mail From: Philip Wadler Newsgroups: gmane.science.mathematics.categories Subject: Equational correspondence and equational embedding Date: Tue, 15 Apr 2008 13:07:06 +0100 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019899 12928 80.91.229.2 (29 Apr 2009 15:44:59 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:44:59 +0000 (UTC) To: categories@mta.ca, types Original-X-From: rrosebru@mta.ca Tue Apr 15 10:17:29 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 15 Apr 2008 10:17:29 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JlkwI-0002pP-CJ for categories-list@mta.ca; Tue, 15 Apr 2008 10:11:10 -0300 Content-Disposition: inline Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 14 Original-Lines: 61 Xref: news.gmane.org gmane.science.mathematics.categories:4365 Archived-At: 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.