[TYPES] Some questions on logical and prelogical relations

Malcolm Tyrrell Malcolm.Tyrrell at computing.dcu.ie
Wed Mar 28 06:40:53 EDT 2007

Hi all.

I'm trying gain an intuition for logical and prelogical relations. As
they've been discussed on this forum before, perhaps some of you can

I'll make some observations and then ask some questions. Please point
any mistakes in my observations.

Thanks for any help,



1. A logical relation is completely defined by its behaviour at the
bottom of the type hierarchy.

2. The term "algebraic relation" is used in [1] to describe a
weakening of the definition of logical relation. In an algebraic
relation, there is some flexibility for how the relation at a function
type corresponds to the relations at its domain and codomain types.

3. Given a relation for each base type, there may be many different
algebraic relations built over them, one of which is a logical

4. A prelogical relation is an algebraic relation with an additional
property about how lambda-abstractions are related.

5. A logical relation is not in general a prelogical relation (since
logical relations are not in general preserved by relational
composition but prelogical relations always are).


Q1. Is the notion "algebraic relation" coined by [1], or is it
standard?  If it's standard, can you suggest a reference?

Q2. Is a prelogical relation uniquely defined by its behaviour at base
types, or is there still some flexibility, as in the case of algebraic

Q3. Given a relation for each base type, must there always exist some
prelogical relation defined over the full type heirarchy?


[1] Prelogical Relations, Honsell & Sannella, Information and
Computation 178, 2002

Malcolm Tyrrell,
Lero - the Irish Software Engineering Research Centre
School of Computing, Dublin City University, Ireland.

More information about the Types-list mailing list