Talk:Respects lemma

From The Twelf Project
Jump to: navigation, search

Not general enough

I don't know if we are defining congruence lemma or if we're taking the definition from somewhere else, but I think that this definition is perhaps needlessly specialized. In almost any system these lemmas must concern more than just a single relation R. For instance:

exp : type.
val : type.


pair : val -> val -> val.
% values are expressions
value : val -> exp.
lam : (val -> exp) -> val.
let : exp -> (val -> exp) -> exp.

eq-val : val -> val -> type.
eq-val/ : eq-val V V.

eq-exp : exp -> exp -> type.
eq-exp/ : eq-exp M M.

pair-cong : eq-val V1 V1' -> eq-val V2 V2' -> eq-val (pair V1 V2) (pair V1' V2') -> type.
let-cong  : eq-exp M M' -> ({v} eq-exp (N v) (N' v)) -> eq-exp (let M N) (let M' N') -> type.
value-cong : eq-val V V' -> eq-exp (value V) (value V') -> type.
lam-cong  : ({v} eq-exp (M v) (M' v)) -> eq-val (lam M) (lam M') -> type.

pair-cong is a congruence lemma as you defined. But the others are not: let-cong, uses only eq-exp but the statement of the lemma needs to quantify over values ("for all v, if R(N v) and R(N' v) ...") so it doesn't fit the form. val-cong's premise is a different relation. lam-cong has both problems.

Moreover, all of these are instances of what Karl and Tom and probably others call "respects" lemmas. Do we have an article about that, or should this article be about that instead? I think it would be a more useful subject. If "congruence lemma" is already taken by other mathematicians, we need a new name for such "respects" lemmas.  — Tom 7 10:13, 20 October 2006 (EDT)

This was another one of those "I had a conversation with Dan Licata and then wrote things on the wiki" moments (like shallow equality versus identity) - I don't see a problem with calling all of your lemmas above congruence lemmas or respects lemmas, and I don't understand your objection - if the component parts of an expression value V are equal (in this case as defined by a different relation) then the entire expression is equal. However, I realize now that while I think drl used the word "congruence," I recognized it because it's exactly the word we used for this "respects" property in FPCC HOL. Now googling things I find that it is from Leibniz dealing with geometry, and I can't find any use of the word the way I think of it. I'll ask drl if he remembers what it was I actually meant today, and if I can't come up with a good argument I'll move it to respects lemma. — Rob (and his talk) 10:45, 20 October 2006 (EDT)
My objection is simply that there is not a single relation R in question, so your definition is not general enough to account for several of the lemmas above. It's a minor technical quibble, but if we're going to define something mathematically, it should cover the cases we're interested in. (I actually think examples of the technique will be plenty in this case.)  — Tom 7 14:48, 20 October 2006 (EDT)
Is this statment closer to what you're looking for, and does the distinction between the two definitions make sense? Should I change the to a for the respects lemma comment? — Rob (and his talk) 03:00, 21 October 2006 (EDT)
I'm being bold and rewriting it.  — Tom 7 10:53, 1 November 2006 (EST)

Why is compatibility a respects lemma?

I don't understand why compatibility is a respects lemma? What relation is being shown to respect bin-eq in

1-compat : bin-eq M M' -> bin-eq (1 M) (1 M') -> type.

?

Or, in what sense is 1 a relation?

I would reserve "respects" for the sense in which you use it in the first part of the article, namely showing that a type family respects particular relations on its indices. I don't think of congruence/compat as being an instance of that.

  • I guess the definition of a "respects" lemma should also say term constructors, or else you're right that it doesn't fit. I'll fix it. The reason for lumping them all together is that people like Karl and myself and DKLee use -resp in our code for compatibility lemmas as well.  — Tom 7 13:38, 3 November 2006 (EST)

Also, I'm not convinced that it makes sense to define this terminology in general for arbitrary relations. E.g., is showing that if M:A and A<:B then M:B a "respects" lemma, assuming I'm working in a system where this is only admissible? What relations, other than identity, do we need to use this terminology for?

I've seen it for inequality, for instance (see division over the natural numbers).  — Tom 7 13:38, 3 November 2006 (EST)

The way I'd tell the overall story is this:

  • Often, we need to internalize LF equality---which, by adequacy, corresponds to equality of informal object-language entities---as a judgement. Usually this is so that we can state and prove metatheorems that involve equality (e.g., that a judgement's outputs are unique).
  • There are several ways of doing this:
    • Identity (least relation containing reflexivity)
    • Compatibility rules for each constructor
    • Compatibility rules for each airity of constructor (Tom's trick)
    • Compatibility rules plus explicit refl, sym, trans rules
All of these define the same relation. However, it turns out that identity is the easiest definition to work with: it gives you the most information when reasoning from equality and it's almost as easy to show that the remaining rules (compitibility, S and T) are admissible as it is to write them as explicit rules.
  • You often need to show that a type family's indices respect equality---that you can replace equals with equals. When you've defined equality to be identity, these respects lemmas are always trivial to prove because...

Drl 18:01, 2 November 2006 (EST)

I think you should look at the equality page to incorporate that story, but this page isn't about equality... (?)  — Tom 7 13:38, 3 November 2006 (EST)

Fixing this, uniqueness, etc.

Most of these ... lemma articles don't hold together. I've grepped through a lot of the TALT code, and Tom is right that code (at least in iequalities.thm) supports the idea that value-cont above is a "respects lemma".

That said,

  • the vast majority of theorems in TALT with the token resp, as well as
  • all the theorems with the token respects in DRL's exp-evaluation, lc-height, and list-append-assoc

encode the idea of referential transparency as Stephen Brookes explains it. Every online source on referential transparency is crap, as far as I can find; according to Brooks the term embodies the idea of Frege: The meaning of a sentence must remain unchanged when a part of the sentence is replaced by an expression having the same meaning. Your example of equals-for-equals for and embodies this fact, so does this theorem from TALT:

elab_operand_resp_same : same_operands O O' -> elab_operand LI N O OE -> elab_operand LI N O' OE -> type.

The inputs are always a bunch of type families saying "things are equivalent in some way", plus one relation that isn't considered "equivalence" (and in your example, elab_operand in the above example)). The output is that same relation, but with equals replaced for equals. This, I think, is a great way to explain what we mean by "respects lemmas" - in this formulation, "respects lemmas" have something very fundamental to do with equality/equivalence.

Another example from TALT doesn't have precisely this form, but still fits into the idea of substutiting equals for equals, becuase it is implicitly operates based on the idea that N*M and N*M' are the same thing.

binary_size_resp3 : product N M N*M -> product N M N*M' -> binary_int E V (B : binary N*M) -> binary_int E V (B' : binary N*M') -> type.
%mode binary_size_resp3 +X1 +X2 +X3 -X4.

On the other hand, TALT also has this theorem:

ii_add_resp : eaddress_eq E E' -> oper_eq O O' -> iinst_eq (ii_add N E O) (ii_add N E' O') -> type.

This describes what I wanted to call "congruence" early on and which you disagreed with. However, think about if, instead of ii_add being a function,

ii_add : {Nsz:nat} eaddress Nsz -> oper Nsz -> iinst.

it was a total relation with three inputs and an output.

ii_add : {Nsz:nat} eaddress Nsz -> oper Nsz -> iinst -> type.

Then the theorem above would be

ii_add_resp : eaddress_eq E E' -> oper_eq O O' -> ii_add N E O II -> ii_add N E' O' II' -> iinst_eq II II' -> type.
%mode ii_add_resp +Eq1 +Eq2 +OP2 +OP1 -Eq3.

This is the form of a uniqueness lemma, and not a statement about referential transparency as the vast majority of resp-proofs in TALT are; the same goes for every one of the cong lemmas that Tom mentions at the top.

Here is what I propose we either write (or else write something similar), or else delete all three of these confusing crazy articles and start over.

  • Respects lemmas are lemmas that embody referential transparency. They deal with a relation respecting an equivalence relation by permitting the substitution of equals for equals. Part and parcel of this is that the relation that respect equivalence (and or binary_int or elab_operand) don't need to be thought of as having "inputs" and "outputs."
  • Congruence lemmas show that if A and A' are related in some way (equality, inequality, whatever), and a transformation (specifically adding or removing a function symbol like pair, s, let, or value) transforms A to B and A' to B', then B and B' are related in some way (equality, inequality, whatever).
  • Uniqueness lemmas show that if A and A' are equivalent, and F maps A to B, and F maps A' to B', then

Congruence lemmas and uniqueness lemmas, then, are a more general case of something that seems to look like this (Noam helped me with the category theory, though I'm obviously going to botch it here):

A ------> B
|     f   |
| R       | R'
|     f   |
A' -----> B'

where in congruence we say f is a function symbol, not a relation, and in uniqueness we say f is a relation, not a function symbol and R and R' are both some sort of equivalence relation. We write articles for these two things rather than all the other generalzations, because they show up alot, awesome.

Sorry for writing so much — Rob (and his talk) 23:30, 8 March 2007 (EST)

I'm mostly okay with this terminology, since it's close to what I've been advocating from the start. Here's how I use the words:
* Respects: a relation respects the equivalence of its subjects: R(...,M,...) and M = M' implies R(...,M',...).
* Uniqueness: a relation determines some positions uniquely: R(...,M,...) and R(...,M',...) implies M = M'.
* Congruence: an equivalence relation commutes with the term formers. M = M' implies f M = f M'. Since we have different notions of equivalence at different types, the relation in the premise will not always be the same as the relation in the conclusion.
It might be better to call these "compatibility" rather than "congruence", if we want the same terminology for non-equivalence-relations. Congruence and compatibility are "already taken" in math, so we shouldn't break with their established meanings. A congruence is an equivalence relation that commutes with term formers; a compatible relation does not have to be an equivalence relation.
Also, I don't think it's right to call an "upside-down congruence lemma" a congruence lemma, since I can write down a congruence that doesn't satisfy such inversion properties. I call them inversions.
Someone at some point (Tom?) made an argument for why a congruence lemma was a respects lemma, but I don't remember what that argument was.
Drl 11:44, 9 March 2007 (EST)
I figured this well might be what you were always trying to say; I've just been lost in the woods about this and needed to work it out for myself. Do I understand you correctly when you say that "compatibility" does fit the meaning you say it has in mathland? If so, great; maybe we should just have the page "Congruence lemma" and mention that "Compatibility lemma" is a generalized case of this? I think the original point of these techniques were that they were specific and showed up all the time; therefore it would be nice to be as specific as is reasonable. — Rob (and his talk) 10:53, 9 March 2007 (EST)
I think I have the definition of compatibility right. William is the one who corrected my use of congruence on non-equiv relations, so ask him. I'm thinking that it would be most clear if we just have one page on identity types that introduces this terminology in that specific context, with subsections for respects, congruence, ... . Then we can say that we use the terminology analogously for other equiv rels and relations in general. That will be less abstract than defining the terms in the context of a general discussion of equiv rels. Drl 11:44, 9 March 2007 (EST)