[TYPES] Some questions on logical and prelogical relations

[Malcolm Tyrrell]

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

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

Thanks for any help,

Malcolm

OBSERVATIONS:

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

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

QUESTIONS:

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
relations?

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

REFERENCES:

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

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