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.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
