Not signed in (Sign In)

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

  • 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

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)