7
$\begingroup$

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus:

  1. via a plain relation $t_1 = t_2$,
  2. via an indexed relation $\Gamma \vdash t_1 = t_2 : T$.

Barendregt [1] e.g. uses the simpler former style, while other sources often seem to be preferring the latter.

I have only seen the first style being used for the case of simple beta equivalence (as in Barendregt). Is it possible to use this style even in the presence of an eta-rule, esp considering that eta-expansion does not necessarily preserve well-formedness?

More specifically, I'm interested in the (simple?) case of eta-equivalence for F-omega types. Any pointers are welcome.

[1] H. Barendregt, Lambda Calculi With Types. In: Handbook of Logic in Computer Science, Vol 2. Oxford University Press 1992

Improve this question
$\endgroup$
3
  • $\begingroup$ I'd consider 1 "old style" and 2 "new style". Or to put it another way, one should always put free variables in context, therefore 2 is the preferred way, even in a uni-typed setting (where the variables are then just listed). $\endgroup$
    – Andrej Bauer
    Jan 10, 2012 at 7:07
  • $\begingroup$ @Andreas: Tangential question: has it been investigated what the semantic consequences of adding/omitting $\eta$ in F$\omega$ are? A few years back I looked for work in that direction, but could not find much. Maybe I didn't search hard enough. $\endgroup$
    – Martin Berger
    Jan 10, 2012 at 12:13
  • 1
    $\begingroup$ @MartinBerger: I don't have a real answer for that in general. But I need it in the context of module systems for programming languages, where you typically want a type name to equate its $\eta$-expansion, and certain encoding techniques are simplified in its presence. Building that into the semantics of your internal language then is a natural and highly convenient thing to do. $\endgroup$
    – Andreas Rossberg
    Jan 10, 2012 at 15:00

1 Answer 1

Reset to default
4
$\begingroup$

The first approach is subsumed by the second, sort of (because the first approach is slightly broken).

One should never consider expressions with free variables without explicitly specifying a context in which they appear (this is a lesson one learns as soon as one wants to formalize $\forall$ and $\exists$ that are allowed to range over possibly empty types or sets).

In a single-sorted theory, equations without context $t_1 = t_2$ can always be equipped with a context $\Gamma \vdash t_1 = t_2 : S$ where $S$ is the single sort and $\Gamma = x_1 : S, \ldots, x_n : S$, with $x_i$ being the free variables in $t_1$ and $t_2$.

Leaving the context implicit like that is not quite right. For example, what if I want to write down an equation that involves $x_1$ and $x_2$ in a context which also mentions $x_3$? You might think that sort of thing is going to be useless, but it isn't, not if $x_3$ could come from an empty type.

Also, as soon as you think about categorical semantics you will see that it makes little sense to have bare equations without contexts.

So I would advise you to put your equations in contexts, and then use the shorter form as an abbreviation. One reference where everything is done explicitly in a context all the time is Bart Jacob's "Categorical Logic and Type Theory", Chapter 8 is about polymorphic type theory and might be of particular interest to you.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ yes, clearly the old style does not scale to more pathological types (e.g. eta for unit) or more interesting types (like, say, singletons). However, none of these occur for the type equivalence of vanilla F-omega, where the only kinds are $\Omega$ and $\kappa_1\to\kappa_2$. I wonder if it is at least possible in that context to use the old style. I expect it is, given that beta-eta is consistent, but have never seen it used. $\endgroup$
    – Andreas Rossberg
    Jan 10, 2012 at 8:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.