# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeSep 16th 2013

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?

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeFeb 28th 2014
• (edited Feb 28th 2014)

added an actual explanation to logical relation:

A logical relation between 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.

• CommentRowNumber3.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 28th 2014

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.)

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeFeb 28th 2014

The term is apparently due to Reynolds in 1983.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeFeb 28th 2014

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

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeFeb 28th 2014

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

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeFeb 28th 2014

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

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeFeb 28th 2014

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

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMar 1st 2014
• (edited Mar 1st 2014)

I see see

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

Not sure what to make of it all…

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeSep 6th 2018

Added an introductory text:

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