RE: [Agda] Universes à la Tarski and induction-recursion

Wed Feb 2 10:00:12 CET 2011

Yes, you are quite right about "the informal metatheoretic definitions of strong computability predicates in normalization proofs" being an earlier appearance (1972) of induction-recursion than the universe a la Tarski. The difference is that the former were given in an informal metalanguage used by Martin-Löf, whereas the universe a la Tarski is given with formal rules, where in the latter the inductive-recursive nature is completely explicit. One of the benefits of having a general notion of induction-recursion is that one can formalize the computability predicates in a strong type theory and see that the rules are instances of a general schema which also captures the universe a la Tarski. It is clear from Martin-Löf's writings in the 1970s that he considered these computability predicates as constructively valid, but no further explanations for the reasons were given. The general understanding of such definitions and their "semantics" came gradually with important contributions of Aczel, Allen, and Mendler.

Peter

________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of James Chapman [james at cs.ioc.ee]
Sent: Tuesday, February 01, 2011 8:24 PM
To: agda at lists.chalmers.se
Subject: Re: [Agda] Universes à la Tarski and induction-recursion

I was under the impression that one could trace back the first uses of
induction-recursion by Martin-Löf to the informal metatheoretic
definitions of strong computability predicates in normalization proofs
such as the one reprinted in "Twenty Five Years of Constructive Type
Theory". A book I used to have until I made the fatal error of lending
it to a certain Professor Ghani.

The below citation taken from P. Dybjer, and A. Setzer:
Induction-Recursion and initial algebras:

P. Martin-Löf. An intuitionistic theoy of types. In G. Sambin and J. Smith,
editors, Twenty-Five Years of Constructive Type Theory, pages 127–172. Ox-
ford University Press, 1998. Reprinted version of an unpublished report from
1972.

Best wishes,

James

On Wed, Feb 2, 2011 at 9:11 AM, Peter Dybjer <peterd at chalmers.se> wrote:
> Hi Dan,
>
> Let me just tell you my recollection of discussions with Martin-Löf and colleagues here in Gothenburg in the 1980s.
>
> The universe a la Tarski appeared for the first time, I believe, in the book Intuitionistic Type Theory (Bibliopolis) from 1984. It was based on lectures in Padova given in 1980. Previously, universes were a la Russell. Aczel had a universe a la Tarski in his 1974/1977 paper about the Interpretation of Martin-Löf Type Theory in a First Order Theory of Combinators.
>
> You are quite right that in Bibliopolis and Martin-Löf's papers from the 1970s there is no universe elimination rule. But I recall discussions with him at the time (early and mid 1980s) where he entertained the possibility. I believe universe elimination is included in the book by Bengt Nordström, Kent Petersson, and Jan Smith.
>
> The discussion revolved around the issue whether a universe should be considered to be open, in the sense that a new type former could be added whenever there is a need for it. And as soon as you have universe elimination you close the universe, there is no longer a possibility of adding new type formers.
>
> Martin-Löf has also expressed the view that the decoding in a universe a la Tarski is the proper elimination rule. One should not consider an eliminatin rule beyond that.
>
> The basic idea of induction-recursion is that constructions such as the universe a la Tarski and similar things, are indeed to be viewed as closed, and an inductive-recursive definition comes with an elimination rule, so that you can define functions on U after simultaneously having defined U and T.
>
> Personally, I have a position on the "closed vs open universe" issue, but I don't have time at the moment to expand on it. Anyway, it's philosophy.
>
> Peter
> ________________________________________
> From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Dan Doel [dan.doel at gmail.com]
> Sent: Tuesday, February 01, 2011 8:07 AM
> To: agda at lists.chalmers.se
> Subject: [Agda] Universes à la Tarski and       induction-recursion
>
> Greetings,
>
> Not long ago, I was gearing up to explain induction-recursion somewhere, and I
> happened upon an (I think) interesting observation, so I thought I'd share it
> here.
>
> It's common (I think) to suggest that the prototypical example of induction-
> recursion is Martin-Löf's universe à la Tarski. And indeed, we can define a
> universe with the same codes. In Agda, it looks like:
>
>  mutual
>    data U : Set where
>      n     : U
>      fin   : ℕ → U
>      _+_   : U → U → U
>      i     : (s : U) → T s → T s → U
>      π σ w : (s : U) → (T s → U) → U
>
>    T : U → Set
>    T n         = ℕ
>    T (fin k)   = Fin k
>    T (s + t)   = T s ⊎ T t
>    T (i s x y) = x ≡ y
>    T (π s f)   = (x : T s) → T (f x)
>    T (σ s f)   = Σ (T s) (\x → T (f x))
>    T (w s f)   = W (T s) (\x → T (f x))
>
> However, I happened to look back at a set of Martin-Löf's lecture notes from
> the 80s, and I noticed the following: there are no elimination rules given for
> U. And in this sense, the above inductive-recursive universe diverges from the
> original formulation.
>
> Without the elimination rule, the universe behaves much like the built-in
> universes in Agda. For instance, we know that if:
>
>  f : (A : Set) → A → A
>
> then f must be the identity function. We don't know this, however, for:
>
>  f : (a : U) → T a → T a
>
> for the above inductive-recursive universe. f could inspect its first
> argument, and do different things based on its value. However, with the
> original U given by Martin-Löf, we again know that f must be the identity
> function, because no inspection of U is possible. In other words, functions
> (other than T) must be parametric in arguments of type U.
>
> I don't really have any moral to end this up with. I just thought it was
> interesting that the prototypical example of induction-recursion doesn't
> actually appear to match up precisely with actual i-r.
>
> Thoughts?
>
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda