Re: Logical Relations

• To: types@theory.lcs.mit.edu
• Subject: Re: Logical Relations
• From: jcm@ra.stanford.edu (John Mitchell)
• Date: Thu, 26 May 88 19:29:41 PDT
• Cc: gtl@electron.lcs.mit.edu

I was hoping someone else would volunteer some info
on why logical relations are "logical." I think that logical
relations are precisely the relations defionable in 
Church's type theory with equality, or something like this,
but (to my embarassment) I have never been exactly clear
on this.

At any rate, I strongly recommend against "homomorphic
relation" as an alternative terminology, since homomorphisms
always compose, but logical relations do not. Something
like "comprehension relations" might make sense, since 
membership in a logical relation is defined using the same 
comprehension formula as type membership, but I suspect this
is at least as obscure a name as "logical relation" in the 
first place.

• Prev: type inference in ML+
• Next: complexity of ML typing
• Index(es):
  • Main
  • Thread