declaration `...` contains universe level metavariables...

Stream: new members

[Henning Dieterichs]

I'm trying to formalize realtime cellular automata with 1D neighborhood as language deciders (akin to turing machines). I got quite far, even proving some nice closure properties, until I wanted to instantiate my structures with concrete types and lean complained about universe variables. After I fixed that, hell broke loose and lean started to give me "Failed to infer universe levels" or "declaration ... contains universe level metavariables at the expression" everywhere.

I have my problematic definitions here.

This definition does not work (but it looks nice):

def Advice.rt_closed_problematic {α: Type u} {Γ: Type v} [Alphabet α] [Alphabet Γ] (f: Advice α Γ) :=
    ℒ (CA_rt (α × Γ) + f) = ℒ (CA_rt α)

...whereas this definition works, but looks ugly and I hope lean doesn't force me to do that everywhere (especially since the literature on cellular automata doesn't have to restrict their statements to some universes):

def Advice.rt_closed.{u, v, x} {α: Type u} {Γ: Type v} [Alphabet α] [Alphabet Γ] (f: Advice α Γ) :=
  ℒ (CA_rt.{max u v, x} (α × Γ) + f) = ℒ (CA_rt.{u, x} α)

(it states that an advice is real-time closed, if the language family recognized by real time cellular automata with access to that advice equals the language family recognized by real time cellular automata without that advice)

Is there a way to avoid these universe issues?
One practical idea I had was to describe the alphabet and state set Q of an automaton just as Fin k, instead of Q: Type* and [Fintype Q], to make everything Type 0. But this would make construction quite unergonomic.
Is the underlying problem that I would get a logical problem if I could talk about "the set of languages that can be recognized by a cellular automaton in an arbitrary type universe"? (Compared to "of a given type universe")

Thanks for your time :heart:

[Kyle Miller]

The general problem you're running into is that in the signature of LCellAutomaton is LCellAutomaton.{u_1, u_2} (α : Type u_1) : Type (max u_1 (u_2 + 1)). The parameter u_2 can't really be inferred from this.

Letting Q be universe polymorphic is fine, but then you have to treat its universe level as being an "explicit" universe parameter, and just feel lucky in the cases that Lean decides it can infer it.

To be clear, this is not a logical problem, but rather an ergonomics problem from letting things be universe polymorphic and not giving a way for Lean to figure out the universe levels automatically.

One solution is to work more carefully on the orders of universe parameters. For example

  structure LCellAutomaton.{u} (α: Type*) extends CellAutomaton.{u} where
    embed: α → Q
    border: Q

will put the uninferrable u first. The other parameter can always be inferred from the α argument. That way, later, you can write LCellAutomaton.{u}. (Notation note: you can give prefixes of the universe parameters like this. Also, you can use _ for parameters you want Lean to infer.)

Somehow this change is enough to get Lean to accept your rt_closed_problematic... I'm suspicious of this being robust, but :shrug:

[Kyle Miller]

You could also decide that Q must live in the same universe as α. That's probably not going to really restrict you — there's always ULift to bring types like Fin n up to the universe for α. Adding this universe restriction would make things inferrable.

[Kyle Miller]

Consider adding @[pp_with_univ] to CellAutomaton, given that the universe level is necessary to understand it.

[Aaron Liu]

it's because you bundled the type in CellAutomation

[Henning Dieterichs]

@Kyle Miller Thanks! Didn't know about ULift, will try to use it :)

[Henning Dieterichs]

it's because you bundled the type in CellAutomation

I was wondering about that. But later I have to deal with a structure which has two alphabets and a cellular automaton over Q1 and a finite state machine over Q2. I was trying to avoid having to mention all four types every time I deal with an instance of it.

[Kyle Miller]

@Aaron Liu What do you mean precisely? What is "it" that is because the type's bundled?

There's nothing wrong in principle with bundling a type in CellAutomaton. There are consequences — what I mentioned about needing to treat the universe level as explicit — but it's still workable.

[Aaron Liu]

Kyle Miller said:

Aaron Liu What do you mean precisely? What is "it" that is because the type's bundled?

There's nothing wrong in principle with bundling a type in CellAutomaton.

yeah but what this means is that every time you write CellAutomaton you have to make sure you have a new universe level, and this doesn't happen if it's unbundled because Type* takes care of that

[Henning Dieterichs]

You could also decide that Q must live in the same universe as α. That's probably not going to really restrict you — there's always ULift to bring types like Fin n up to the universe for α. Adding this universe restriction would make things inferrable.

This would be a problem though if I need an automaton where its state type Q is α -> α, no?
For some examples, my alphabet is e.g. Bool (which I think I shouldn't convert to ULift Bool)

[Kyle Miller]

(Basically, I can't tell whether you're giving design advice @Aaron Liu, or just expanding on why there's an uninferable universe parameter in the first place.)

[Kyle Miller]

@Henning Dieterichs The type α -> α lives in Type u still, so it shouldn't be a problem.

[Aaron Liu]

Kyle Miller said:

(Basically, I can't tell whether you're giving design advice Aaron Liu, or just expanding on why there's an uninferable universe parameter in the first place.)

I feel like it's a bit of both? Because this causes an uninferrable universe parameter, and also because of some other reasons, bundling types feels like a bad idea to me.

[Kyle Miller]

(@Henning Dieterichs I didn't analyze the meaning of your universe levels — I didn't even get as far as thinking about what alpha represented — so it could be bad advice!)

[Henning Dieterichs]

will I regret it if I just remove universe polymorphism and require Type 0 for states to simplify the problem?
I saw that quite some effort went into dealing with universes when regular languages were defined here in mathlib.
There, the state type is not in the DFA, but outside and can be from any universe. A DFA doesn't even come with [Fintype σ], which I find quite misleading...

[Aaron Liu]

I would prefer everything to be universe polymorphic

[Kyle Miller]

@Henning Dieterichs You don't have to be universe polymorphic, but the deal is that it can be a pain if later you discover that your formalization needs a type from a higher universe. Notice that if you include the state type as a field, even if you restrict it to Type 0, the type of the automaton itself is in Type 1. What if some construction wants to use a subset of automata as the states for another automaton? (Though this is probably surmountable on a case-by-case basis) That all said, if you don't have a lot of material, you could choose to defer universe polymorphism until you need it.

Re DFA not including finiteness, a mathlibism is to avoid typeclasses or hypotheses that aren't necessary for the definition itself. Since the state type is coming from outside the definition, it's up to you to provide the Fintype (or Finite) hypothesis. It can feel misleading, but definitions like Language.IsRegular just need to remember to include finiteness.

BTW, the theorem you point out about DFAs is not effort for dealing with universes per se. It's proving the technical result that it suffices to consider only those state types in Type 0. (Maybe it's also worth pointing out that the type of the general Language.isRegular_iff has the same annoying problem you're running into; if you use it for rewriting, the v parameter isn't determined by the LHS, so you have to specify it.)

One interesting design alternative to DFA is to use a universal σ that you'd use for multiple machines. The DFA contains a finite subset of its actual states. In practice, a construction might define an inductive that includes all the kinds of states you'd need. It's also possible to transfer a family of DFAs to the same state type this way.

structure MyDFA (α : Type u) (σ : Type v) where
  states : Set σ
  step : σ → α → σ
  start : σ
  accept : Set σ
  states_finite : states.Finite
  accept_subset : accept ⊆ states
  step_mem : ∀ s ∈ states, ∀ x : α, step s x ∈ states
  /-- For extensionality. The `step` function is equal to `start` outside the domain. -/
  step_not_mem : ∀ s ∉ states, ∀ x : α, step s x = start