Re: [Hol-info] data-respecting relation

[Rob A. <rd...@le...>]

On 5 Sep 2012, at 15:50, Ramana Kumar wrote:

> What is the usual name for this kind of relation?
> 
> Given an inductive data type like
> foo = C1 of bool | C2 of foo list
> 

So foo is a type of trees with arbitrary finite branching and with Boolean labels on the leaves.

> I want to classify relations R:foo -> foo -> bool that satisfy:
> 1. equivalence R
> 2. EVERY2 R vs1 vs2 ==> R (C2 vs1) (C2 vs2)
> 3. ( R (C1 _) v ==> ?b. v = (C1 b) )  /\ ( R (C2 _) v ==> ?vs. v = (C2 vs) )
> 
As I think 3 is supposed to a conjunction of two implications, I have inserted the opening brackets before the two Rs and the matching closing brackets. If you didn't want the brackets, then I must completely misunderstand your question.

> Condition 1 alone is obviously an equivalence relation.

Indeed! That is a good start :-)

> I think Conditions 1 + 2 give you a "congruence relation".

Yes, assuming that EVERY2 R vs1 vs2 means that vs1 and vs2 are lists of the same length such that for each element v1 of vs1, R v1 v2 holds for the corresponding element of v2. I.e., in universal algebra jargon, EVERY2 R is the congruence on lists generated by the relation that holds between singleton lists [v1] [v2] iff R v1 v2 holds. (Here the congruence A generated by a relation B is the smallest congruence A such that A relates every pair that B relates).

> Any standard name or theory about 1 + 2 + 3?
> Or maybe 3 should be included for congruences?

No. Congruences have properties 1 & 2 but need not have (the analogue of) property 3. E.g., one wants the relation "equivalent modulo 2" to be a congruence on the natural numbers, but it relates SUC(SUC 0) to 0.

I don't know of a snappy name for congruences with properties 1, 2 & 3. I would describe them as "congruences that refine the congruence whose congruence classes are the ranges of the constructors". I.e., in your example, 1, 2 & 3 mean that R refines the congruence Theta, such that, for f, g in {C1, C2}, Theta (f x) (g y) holds iff f = g. (Equivalence relation A refines equivalence relation B if every pair that A relates is also related by B).

> 
> (Context: I'm trying to generalise a theorem that says some operation preserves values up to a suitable equivalence of values, but equivalence is subtle because my values include closures that contain code and other (environment) values, and all I really care about in the end is that they behave the same. In full generality this is a contextual equivalence problem, which I don't want to solve; and indeed the approach above would still require the code to be identical (since it's a different type). But it might be useful to prove the theorem for a class of congruence relations, rather than a specific one, and/or it might make the proof slightly simpler...
> And I could allow the code to vary by defining "congruence" for both the value and code types together...)

I can think of two more properties that might be relevant.

4. R (C2 vs1) (C2 vs2) ==> EVERY2 R vs1 vs2
5. R (C1 x) (C1 y)

So 4 is the converse of 2. 1 + 2 + 3 + 4 together say that R is generated by its restriction to the range of C1. I.e., there is an equivalence relation S on the leaf labels, such that two trees are related by R iff (i) they are identical modulo leaf labels and (ii) the labels on corresponding leaves are related by S. Finally 1 + 2 + 3 + 4 + 5 says that R is the relation "identical modulo leaf labels".

Regards,

Rob.