link to synth Tait computability and parametricity

]]>Some redirects and some other common terminology

]]>Hi Urs,

In the comments below the StackExchange discussion you refered to: *What are differences between logical relations and simulations?* there is a remark somewhere that “logical relations seem to capture just the existence of a simulation relation, rather than the relation itself”.

To me this sounds very familiar. I did not hear of logical relations before (maybe I’ll dig into it later) but in process algebra I’m certain the equivalence axioms between processes capture only the fact that there is a (bi)simulation relation between the processes, without specifying which bisimulation relation is actually meant. (One of my first category-theory related papers was actually about resolving a problem in process algebra, where they would like to talk about “approximation” but in my opinion cannot, because their equivalence “forgets” what the precise bisimulation relation is that is being considered. Non-determinism in the processes makes that multiple different bisimulation relations may be possible. By keeping the information which bisimulation relation is meant, the notion of limit just becomes the category theoretic one, is nicely defined, and gives intuitive outcomes. If you drop that information there are some counterexamples that point out problems in defining a limit. You actually put in the reference on *my personal page* ;-)… the EPTCS paper.

Adds two more references

Piotr Jander

]]>Added an introductory text:

- Lau Skorstengaard,
*An Introduction to Logical Relations: Proving Program Properties Using Logical Relations*, (pdf)

I see see

- StackExchange discussion,
*What are differences between logical relations and simulations?*

with a contribution by one of the authors of the above article.

Not sure what to make of it all…

]]>Maybe to make this less mysterious you might state the definition that you think is right and which citations it is extracted from.

]]>Huh. I wonder whether other people would agree with that definition.

]]>It’s all there cited in the entry: section 2 of http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf

]]>Where did you get this explanation/definition? It’s not how I would have defined the notion.

]]>The term is apparently due to Reynolds in 1983.

]]>Never heard of that term before. (Doesn’t seem particularly well-chosen; I think I’d just call it an algebraic relation or an internal relation, i.e., a relation interpreted internally in the regular category of algebras. Wonder where Ghani had heard it.)

]]>added an actual explanation to *logical relation*:

]]>A

logical relationbetween sets/types equipped with extra (algebraic) structure is a relation that preserves this structure in the appropropriate way. Hence logical relations are to relations as homomorphisms between (algebraic) structures are to functions of the underlying sets/types. See for instance (Hermida 13, section 2) for a quick survey.

I gave the entry *logical relation* an Idea-section, blindly stolen from a pdf by Ghani that I found on the web. Please improve, I still don’t know what a “logical relation” in this sense actually is.

Also, I cross-linked with *polymorphism*. I hope its right that “parametricity” may redirect there?