Infinitary type theory

[Michael Shulman]

Since the problem of defining infinite structures has come up in
another thread, it may be a good time to bring up this idea, which has
been kicking around in my head for a while. I know that something
similar has occurred to others as well.

Logicians study infinitary logics in addition to finitary ones. Why
can't we have an infinitary type theory?

An infinitary type theory would include type-forming operations which
take infinitely many inputs ("infinite" in the sense of the
metatheory). The most obvious would be, say, the cartesian product of
infinitely many types, e.g. given types A0, A1, A2, ... (with the
indexing being by external natural numbers), we would have a type
Prod_i(Ai), and so on. Semantically, this would correspond to a
category having infinite products.

More useful than this would be a category having limits of towers of
fibrations. I think this can be represented as a type former in an
infinitary type theory as well, with a rule like

Gamma |- A0 : Type
Gamma, a0:A0 |- A1(a0) : Type
Gamma, a0:A0, a1:A1 |- A2(a0,a1) : Type
Gamma, a0:A0, a1:A1, a2:A2 |- A3(a0,a1,a2) : Type
...
----------------------------------------
Gamma |- lim_i A_i : Type

Then we would have a corresponding introduction form, like

Gamma |- x0 : A0
Gamma |- x1 : A1(x0)
Gamma |- x2 : A1(x0,x1)
...
-------------------------------------
Gamma |- lam_i xi : lim_i A_i

with elimination and computation rules. We might also need an
"infinitary extensionality" axiom.

It seems that in such a type theory, we ought to have no trouble
defining (say) semisimplicial types, as the limit of the appropriate
externally-defined tower of fibrations.

Has anyone studied infinitary type theories before? Of course, they
probably won't have all the good properties of finitary ones. For
instance, I think judgmental equality isn't going to be decidable,
since there's no way to algorithmically test the infinitely many terms
that go into a lam_i for equality. But other proposals like HTS are
also giving up decidability. Are there other more serious problems
with an infinitary type theory?

Mike

[Joyal, André]

Dear Mike,

I thought a bit about infinitary type theory.
In categorical terms, the "meta-theory" is the base of a Grothendieck fibration
whose fibers are categories of "external" families.
It might be worth describing the axioms.

André
________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Michael Shulman [shu...@sandiego.edu]
Sent: Sunday, June 22, 2014 2:05 AM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Infinitary type theory

Mike

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Amr Sabry (عمرو صبري)‎]

A possible starting point might be the various papers on the "infinitary lambda calculus". The classic reference is Kennaway , Klop , Sleep , and de Vries (1996 or 1997). More recent approaches seem to be coalgebraic which might be more directly relevant. --Amr

[Paolo Capriotti]

On Sun, Jun 22, 2014 at 7:05 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> [...]

> Then we would have a corresponding introduction form, like
>
> Gamma |- x0 : A0
> Gamma |- x1 : A1(x0)
> Gamma |- x2 : A1(x0,x1)
> ...
> -------------------------------------
> Gamma |- lam_i xi : lim_i A_i
>
> with elimination and computation rules. We might also need an
> "infinitary extensionality" axiom.
>
> It seems that in such a type theory, we ought to have no trouble
> defining (say) semisimplicial types, as the limit of the appropriate
> externally-defined tower of fibrations.
>
> Has anyone studied infinitary type theories before? Of course, they
> probably won't have all the good properties of finitary ones. For
> instance, I think judgmental equality isn't going to be decidable,
> since there's no way to algorithmically test the infinitely many terms
> that go into a lam_i for equality. But other proposals like HTS are
> also giving up decidability. Are there other more serious problems
> with an infinitary type theory?

It seems to me that not having finitary descriptions of judgements is
itself a "serious" problem. The moment you give up on this property,
you might as well give up on the idea of having a "theory" altogether,
and just study the corresponding collection of models directly. For
instance, you can never really implement a type checker for such a
thing. The problem is more than undecidability: there is just no
syntax to express what goes in place of the dots in your examples
above. If you do come up with a syntax to encode the infinite sequence
of judgements into a finite string, then you have essentially replaced
your infinitary theory with an equivalent finitary one, and there's no
point in keeping the original infinitary presentation.

Paolo

[Vladimir Voevodsky]

> If you do come up with a syntax to encode the infinite sequence
> of judgements into a finite string, then you have essentially replaced
> your infinitary theory with an equivalent finitary one, and there's no
> point in keeping the original infinitary presentation.

You make a two-layered theory where the "object logic" (infinatry in this sense) is embedded into some system where there is already induction (inductive types?).

V.

[Michael Shulman]

On Sat, Jun 21, 2014 at 11:24 PM, Joyal, André <joyal...@uqam.ca> wrote:
> In categorical terms, the "meta-theory" is the base of a Grothendieck fibration
> whose fibers are categories of "external" families.

I guess... but it seems to me that such an extra layer of abstraction
would only be necessary if we want to hop out one more level into a
metametatheory. If we're just working *in* the metatheory, then we
can just treat it as a set theory or type theory, with the ordinary
corresponding notion of "family".

[Michael Shulman]

On Sun, Jun 22, 2014 at 1:43 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:
> It seems to me that not having finitary descriptions of judgements is
> itself a "serious" problem. The moment you give up on this property,
> you might as well give up on the idea of having a "theory" altogether,
> and just study the corresponding collection of models directly.

I think the fact I mentioned, that logicians study infinitary logic,
means that this is not true.

> For instance, you can never really implement a type checker for such
> a thing. The problem is more than undecidability: there is just no
> syntax to express what goes in place of the dots in your examples
> above.

That's not clear to me. Already when working in a proof assistant
like Coq, we do some amount of "coding in the metatheory", namely
writing tactic scripts. Ordinary programming languages also often
allow some coding in the metatheory, like template languages and
preprocessors and macros. Why not use a similar sort of "coding in
the metatheory" for this?

> If you do come up with a syntax to encode the infinite sequence
> of judgements into a finite string, then you have essentially replaced
> your infinitary theory with an equivalent finitary one, and there's no
> point in keeping the original infinitary presentation.

It's true, as Vladimir said, that once you fix a metatheory, you could
then treat the infinitary object-theory and the meta-theory as a
single system. If you'd prefer that equivalent formulation, I don't
really mind, although in principle I'd rather not have to fix a
particular metatheory (except, of course, when implementing it in a
computer).

Mike

[Michael Shulman]

On Sun, Jun 22, 2014 at 1:23 AM, Amr Sabry (عمرو صبري)
<amr....@gmail.com> wrote:
> A possible starting point might be the various papers on the "infinitary
> lambda calculus". The classic reference is Kennaway , Klop , Sleep , and de
> Vries (1996 or 1997). More recent approaches seem to be coalgebraic which
> might be more directly relevant. --Amr

Thanks for this reference! However, from glancing at the paper cited
it seems that their notion of "infinitary term" arises by interpreting
the standard inductive presentation of syntax as coinductive instead,
so that a syntax tree can have infinite branches. I'm suggesting
instead to keep the presentation inductive, so that all branches of
the syntax tree are finite, but allow infinitary constructors, so that
nodes in the syntax tree can have infinitely many children. Do you
know of a reference for something like this?

Mike

[Martin Escardo]

On 27/06/14 03:58, Michael Shulman wrote:
> I'm suggesting instead to keep the presentation inductive, so that
> all branches of the syntax tree are finite, but allow infinitary
> constructors, so that nodes in the syntax tree can have infinitely
> many children. Do you know of a reference for something like this?

Some old references are:

Tait, W. W. Infinitely long terms of transfinite type. 1965 Formal
Systems and Recursive Functions (Proc. Eighth Logic Colloq., Oxford
pp. 176–185 North-Holland, Amsterdam.

Martin-Löf, Per. Infinite terms and a system of natural deduction.
Compositio Math. 24 (1972), 93–103.

But many more people wrote in the past and more recently about
infinite terms. If you search for "infinite terms" in the "anywhere"
box of MathSciNet you will get lots of results.

M.

[Neelakantan Krishnaswami]

On 27/06/14 03:58, Michael Shulman wrote:> On Sun, Jun 22, 2014 at 1:23

Hello,

This kind of rule has been studied in the context of proof
theory -- the phrase to Google for is "Buchholz's Omega-rule".
Hilbert (IIRC) originally suggested looking at infinitary rules
for induction of the form:

Γ ⊢ P(0)
Γ ⊢ P(1)
Γ ⊢ P(2)
...
————————————
Γ ⊢ ∀n. P(n)

The idea is that you can have a "rule" for induction with
has infinitely many premises, establishing that P holds for
every n. Buchholz, when studying systems of inductive definitions,
realized that infinitary rules can also be viewed as having
a metalogical *function* as a premise. So instead
of having an infinite number of premises, you can imagine that
there is a computable function in your metalogic that produces
those premises on demand.

Recently, Noam Zeilberger has looked at the relation between the
Omega rule and Andreoli's notion of focusing (popularized by Girard)
in his paper "Focusing and Higher-Order Abstract Syntax". Then,
in his paper "Defunctionalizing Focusing Proofs", he shows how
to get back to a first-order representation of proofs.

Regards,
Neel

[Erik Palmgren]

I think one approximation of what you are looking for is already
available in type theory. The W-type (Wx:A)B(x) of a family can be
regarded as the free algebra of infinitary terms, where x:A varies over
function symbols and B(x) is the arity-set of the function symbol of x.
A type universe contains similarly infinitary types. It should be
possible to axiomatize new infinitary type constructions in terms of
these, at least in extensional type theory where one can switch freely
between judgmental equality and propositional equality.


--- Erik

[Michael Shulman]

On Fri, Jun 27, 2014 at 3:26 AM, Erik Palmgren <palm...@math.su.se> wrote:
> I think one approximation of what you are looking for is already available
> in type theory. The W-type (Wx:A)B(x) of a family can be regarded as the
> free algebra of infinitary terms, where x:A varies over function symbols and
> B(x) is the arity-set of the function symbol of x.

Actually, that's exactly *not* what I'm looking for, because it's only
*internally* infinitary. I'm thinking about rules that are
*externally* infinitary.

Thanks everyone else for the references, I'll need to read up on them.
The omega-rule is indeed the sort of infinitary rule I was thinking
of, although of course it's an introduction rule for an existing type
rather than a formation rule for a new one.

Mike

[Jason Gross]

(Resurrecting this thread because I stumbled upon it while rereading A Formalized Interpreter, and I believe I have something new to add.)

As I understand it, using `□A` to mean "syntax for A", an infinitary type theory has rules like `(A → □B) → □(A → B)`.  (Note that this is exactly what HOAS does, which explains why it's so easy to write an interpreter for HOAS without running into the semisimplicial types coherence issues.)

> Are there other more serious problems with an infinitary type theory?

I think the answer to this is "it depends".  In "An Order-Theoretic Analysis of Universe Polymorphism", Favonia, Carlo Angiuli, and Reed Mullanix have a consistency proof for a system with rational-indexed universes (and no explicit universe level quantification).  However, infinitary rules give access to internal universe quantification (consider the function `λ i. "Type"ᵢ`).  I believe HOAS-like internal-level quantification rules out any "fractal-like" scheme of universes (such as the rationals), because we can write an interpreter for "terms using universes i with 0 <= i <= 1" into terms that use universes between 0 and 2 (because we have enough universes to do that), and then we can embed terms with universes between 0 and 2 back into terms with universes between 0 and 1 (divide universe indices by 2), and this loop gives inconsistency by Gödel / Löb.

So at the very least, having infinitary limits rules out some of the more exotic universe level structures.

Best,

Jason

[Nicolai Kraus]

That's an interesting observation! However, I think the question of universe hierarchies is orthogonal to the question of infinitary type constructors.

I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe.

Agda actually *does* allow something like "λ i. Type i". While I view constructions using it more as proof schemes than as single proofs ("book HoTT" wouldn't allow it, you'll have to fix an index), I occasionally found it very useful. Without something like this, I don't see how we could have formalised the statement that "Universe Un is not an n-type in a hierarchy U0, U1, U2, ... of univalent universes (without HITs)" [2]. But I would *not* regard the formalisation [3] as a single proof. I see it as an externally indexed family of Nat-many proofs, and it's only a lucky accident (using a feature of Agda that isn't even part of the considered type theory) that it can be implemented.

[1] https://arxiv.org/abs/1705.03307

[2] https://arxiv.org/abs/1311.4002

[3] https://www.cs.nott.ac.uk/~psznk/docs/thesisagda_nicolai/HHHUU-ComplicatedTypes.html

Best wishes,

Nicolai

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCarzP9wE1t2Y8M7Yi0i1ChYb8PrP_2RpKY9tcEZbkB9QKQ%40mail.gmail.com.

[Michael Shulman]

Also, apparently Agda's Set-omega breaks subject reduction:
https://github.com/agda/agda/issues/5810

[Jason Gross]

> I don't think access to internal universe quantifications is an inherent consequence of infinitary constructors. I'd rather say that it's an accidental side effect of Mike's formulation from 2014 that something like "λ i. Type i" is possible, and it can easily be ruled out. In Section 2.4, strengthening A1-3 of the 2LTT paper [1], a type theory with such infinitary type constructors is specified without allowing internal universe quantification. This is essentially because the externally indexed sequence of types still has to live in a single fixed universe.

As I understand it, this just rules out universe qualification that is not bounded above by a fixed universe, right?  It seems to me that you still get internal quantization over levels less than a fixed level.  And this is enough to make the construction generating inconsistency with Q-indexed universes go through.

[András Kovács]

Jason: I agree that externally indexed products imply bounded universe polymorphism, but I don't understand how we can derive inconsistency from that together with rational levels. The operation that scales rational levels can only be defined externally so it doesn't really affect the possible internal constructions. 

To be clear, by external products I mean e.g. the following for i : ℚ

Product : (ℕ → Tyᵢ Γ) → Tyᵢ Γ
lam     : ((n : ℕ) → Tmᵢ Γ (A n)) → Tmᵢ Γ (Product A)
app     : Tmᵢ Γ (Product A) → (n : ℕ) → Tmᵢ Γ (A n)

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaoJMQhY5upSKXTM%3DLHE72FUH3r0ji-Maf7%3DqmFD%2Bde3QA%40mail.gmail.com.

[Jason Gross]

Ah, you're right, sorry.  I was confusing "being able to name particular universes as function outputs" with "bounded universe polymorphism".  I retract my claim.

Best,

Jason