What is the usual name for this kind of relation?
Given an inductive data type like
foo = C1 of bool | C2 of foo list
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)
Condition 1 alone is obviously an equivalence relation.
I think Conditions 1 + 2 give you a "congruence relation".
Any standard name or theory about 1 + 2 + 3?
Or maybe 3 should be included for congruences?
(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...)
------------------------------------------------------------------------------
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
