Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

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

    diff, v9, current

  1. Adds two more references

    Piotr Jander

    diff, v11, current

    • CommentRowNumber12.
    • CommentAuthorPieter
    • CommentTimeFeb 13th 2019
    • (edited Feb 13th 2019)

    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.

    • CommentRowNumber13.
    • CommentAuthormaxsnew
    • CommentTimeMay 19th 2022

    Some redirects and some other common terminology

    diff, v12, current

    • CommentRowNumber14.
    • CommentAuthormaxsnew
    • CommentTimeMay 19th 2022

    link to synth Tait computability and parametricity

    diff, v13, current