Automata

Stream: CSLib

[Fabrizio Montesi]

We should discuss a bit the pattern for defining different kinds of automata in CSlib. Preferably, this should be coherent with the way we do semantics (but that way can be updated as well, if we get any new insights here!).

One way of using what's already there is to define an automaton as a labelled transition system plus all the assumptions we're making about it. For example, a DFA could be defined as:

import Cslib.Foundations.Semantics.Lts.Basic

structure Dfa (State : Type _) (Label : Type _) where
  -- The transition system of the automaton
  lts : Lts State Label
  -- Start state
  start : State
  -- Accept states
  accept : Finset State
  -- The automaton is finite-state
  finite_state : lts.FiniteState
  -- The automaton is deterministic
  deterministic : lts.Deterministic

Pros:
This would automatically give the expected notions of traces, multi-step transitions, determinism, divergence, state equivalences, etc., coherent with the other languages in cslib. We have theorems about these things as well, which can be reused across the board. This might also facilitate translations between different structures like this (e.g., from DFA to NFA and vice versa).

Cons:
Going through the Ltstype might be weird, so maybe we just wanna put the transition relation in there and provide some magical macro/typeclass. (Not sure what that could be though.)

What other ways could we go for, in order to promote reuse?

[Snir Broshi]

lts.Deterministic only guarantees uniqueness but not existence, so it's different than a function State → Label → State if that's what you meant

[Snir Broshi]

I vote for having both, and providing a way to convert between them:
I think the structure Dfa should contain a function, and should have def toLts that converts it to an Lts, and theorems showing dfa.toLts.FiniteState and dfa.toLts.Deterministic.
Usually the variant with the function is easier to handle (e.g. we don't need the axiom of choice to get the next transition) but converting to an Lts is useful to access more theorems, and also to be able to define transitions as Prop which aren't easily definable as a function.
Similarly we should be able to convert a Dfa to an Nfa by forgetting the deterministic hypothesis and converting the start state to a singleton set.

[Fabrizio Montesi]

Snir said:

lts.Deterministic only guarantees uniqueness but not existence, so it's different than a function State → Label → State if that's what you meant

Oh, yes, I agree. Mine is just a quick sketch to give an idea.

[Fabrizio Montesi]

Snir said:

I vote for having both, and providing a way to convert between them:
I think the structure Dfa should contain a function, and should have def toLts that converts it to an Lts, and theorems showing dfa.toLts.FiniteState and dfa.toLts.Deterministic.
Usually the variant with the function is easier to handle (e.g. we don't need the axiom of choice to get the next transition) but converting to an Lts is useful to access more theorems, and also to be able to define transitions as Prop which aren't easily definable as a function.
Similarly we should be able to convert a Dfa to an Nfa by forgetting the deterministic hypothesis and converting the start state to a singleton set.

I'd like that. It's much like what I proposed a while ago (having conversion functions), and it'd allow people to Keep Definitions Simple (TM).

[Fabrizio Montesi]

Gave it a try, how's it looking?

https://github.com/leanprover/cslib/blob/automata/Cslib/Computability/Dfa/Basic.lean

[Snir Broshi]

Looking good, making toLts a coercion sounds great.

If I were to nitpick this as a reviewer (which I am not), I have some comments:

• toLts_deterministic can be proven as follows:

theorem toLts_deterministic (dfa : Dfa State Label) : dfa.toLts.Deterministic :=
  fun _ _ _ _ htr2 htr3 ↦ htr2 ▸ htr3

which can be even shorter, but I think it's too far for readability :sweat_smile::

theorem toLts_deterministic (dfa : Dfa State Label) : dfa.toLts.Deterministic :=
  fun _ _ _ _ ↦ (· ▸ ·)

• language uses a function to define a set, which is discouraged in Mathlib, as the fact that sets are functions is considered an implementation detail. Prefer using { μs | dfa.Accepts μs } instead.
• accepts_mem_language is solved by rfl:

theorem accepts_mem_language (dfa : Dfa State Label) (μs : List Label) :
  dfa.Accepts μs ↔ μs ∈ dfa.language := by rfl

• Why Type _ in Dfa and not Type*? I don't know the difference, but I think Mathlib prefers Type*
• Dfa/Basic.lean is missing a module docstring
• I'm not sure if it's possible to change the convention, but I much prefer the following: q₁ q₂ for states (q₀ for start), a for labels, w for List Label ("word"), δ for the transition function, δ̂ (delta hat) for MTr, Q for State, Σ for Label.
  I think those are the standard names used in the literature, at least that's what Wikipedia uses

[Fabrizio Montesi]

Ah, yes, some refinements definitely needed. Also, I don't recall by memory if the alphabet is supposed to be finite... (Edit: yes it is.)

[Fabrizio Montesi]

And yes, we should definitely use the notation for Set, thanks for reminding me. :-)

[Fabrizio Montesi]

(deleted)

[Fabrizio Montesi]

Re Type*: I don't know. Using either yields the same result, apparently, and Type _ is a bit clearer in what it does.

[Chris Henson]

Type*, defined here in Mathlib, just elaborates into fresh implicit universes. So yes I think they do the same thing, but with us being downstream of Mathlib, maybe is more idiomatic/readable? Also maybe prevents issues of accidentally sharing a universe for different types. There are several files where we don't care much about universes but specify them explicitly, this could be nicer to write for brevity.

[Fabrizio Montesi]

But Type _ reads like 'Type with whatever universe', whereas Type* reads like... '???' :-)
That's why I've stopped using the latter in favour of the former. But if it solves a problem, then we should consider it ofc. Not sure why it'd work better than Type _ though.

[Chris Henson]

I think it's used enough in Mathlib that many read it exactly the same way. It seems slightly nicer if you want to specify multiple (X Y ... Z : Type*), but otherwise I am ambivalent.

[Fabrizio Montesi]

Ahhh, that's why it's useful. (X Y ... Z : Type _) would use the same universe for all, wouldn't it? Type* would assign a different universe each.

[Chris Henson]

Yes, that's what I meant above by "accidentally sharing a universe".

[Fabrizio Montesi]

Re conventions: I went for plain-text names because I couldn't use Σ :\
Maybe some intermediate solution will come to mind... in the meantime I could call Label Symbol instead.

[Fabrizio Montesi]

I've updated Dfa slightly so that we use grind a bit more and added a few things, same branch.
I'm wondering about some other design choices, exemplified by choosing between the next two for the formalisation of δ̂:

1. Define it as function composition of δ/tr, and then prove it's consistent with toLts.MTr.
2. Define it directly as toLts.MTr.

I'm leaning towards 1 in general. That way, people accustomed to automata theory will find their usual definitions, and whenever they want to use results about lts, they can. But we're setting the convention here. Is that how we want things to be done?

[François G. Dorais]

Fabrizio Montesi said:

Ahhh, that's why it's useful. (X Y ... Z : Type _) would use the same universe for all, wouldn't it? Type* would assign a different universe each.

No: (X Y Z : Type _) assigns different universes for each variable.

[Fabrizio Montesi]

François G. Dorais said:

No: (X Y Z : Type _) assigns different universes for each variable.

Good to know, thanks!

[Fabrizio Montesi]

Tested a bit the first route and it looks pretty ok to me. :)

https://github.com/leanprover/cslib/blob/automata/Cslib/Computability/Dfa/Basic.lean

If we go down this route I could (should?) probably move the lts results to a dedicated Dfa/Lts.lean file.

[Atticus Kuhn]

Fabrizio Montesi said:

We should discuss a bit the pattern for defining different kinds of automata in CSlib. Preferably, this should be coherent with the way we do semantics (but that way can be updated as well, if we get any new insights here!).

(this is just an idea I had, not sure if it has been discussed before/elsewhere)
Could an automaton be defined as a homomorphism from a list to a category? For example, a DFA is a homomorphism from a list to the category of functions and an NFA is a homomorphism from a list to the category of relations. By homomorphism, I mean that list concatenation becomes arrow composition, so

f [] = id
forall (x y : List A), f (x ++ y) = (f y) . (f x)

[Fabrizio Montesi]

I'm not 100% sure about the construction, but one could maybe prove some correspondence results with the 'standard' definition of Dfa? Our current definition abstracts from the types of states and symbols.

[Malvin Gattinger]

I don't have anything to contribute myself, but do I understand correctly that the Automata in CSLib will be separate from those in mathlib already? And also separate from the project by @Ching-Tsun Chou, as both discussed in this thread #computer science > Automata theory in Lean4 :thinking:

[Fabrizio Montesi]

Yes, they're all a bit different. What I'm trying to do here is to see if we can reach a definition that is general and usable enough so that people could be happy to port their work to.

[Ching-Tsun Chou]

Sorry, I just saw this thread. I've not figured out how to keep track of what's going on on Zulip and I saw this thread only because @Malvin Gattinger mentioned me above.
Anyway, the following are the differences between the definition of automata in my project and the definition @Fabrizio Montesi gave above:
(1) My automata definition has the state type bundled in. This is natural for defining automata constructions (direct sum, product, concatenation, loop, etc), where the corresponding constructions on the state spaces will appear on the RHS (rather than the LHS) of the :=of the definition of the construction. But I have to admit that this gave me a lot of trouble in universe level inference and I ended up defining everything on Type rather than Type*. (For automata theory I don't think that's a big deal.)
(2) On the other hand, my automata definition does not include the accepting states or the finiteness assumption:
(2.a) The accepting states are not included because automata on infinite words have multiple types of accepting conditions (Büchi, Muller, Rabin, etc), but automata on finite and infinite words can share many automata constructions if the accepting condition is not included..
(2.b) The finite-state assumption is not included because many result just don't depend on the state spaces being finite. Note that this is also the approach taken by the automata theory in mathlib. When I need to assume the state space is finite, I just include an additional assumption [Finite M.State] in the theorem statement. Since the finite-state assumption is not included by default, I use Set instead of Finset throughout. (The same is true in mathlib.)
(3) I treat deterministic automata and nondeterministic automata separately and do not regard the former as a special case of the latter. Instead, I have a map Automata.DA.toNA to convert a DA into the corresponding NA. (With the dot-notation, one can just write M.toNA.). In fact, I started my project with DA being a special case of NA and found that it was quite painful to work with. Note that mathlib's automata theory also has separate NFA and DFA classes.
(4) Sometimes I wonder even whether the initial state(s) should be part of an "automaton". On more than one occasions the proof I was formalizing calls for reasoning about the set of inputs that can lead an automaton M to go from state s1 to state s2. So perhaps we should stick to a minimalist approach and have only the notions of a nondeterministic LTS and a deterministic LTS, rather than trying to come up with a universally applicable definition of an "automaton".

[Ching-Tsun Chou]

One more thing: we also need a better-named definition of an infinite sequence/word: #mathlib4 > Why is Stream' called Stream'?

[Ching-Tsun Chou]

A question: Why does the transition in cslib's LTS have type State → Lable → State → Prop, rather than State → Label → Set State? The latter is what is used by NFA in mathlib. Although it is easy to move between State → Prop and Set Prop, this difference does introduce some friction.

[Fabrizio Montesi]

The former is what people typically use when defining operational semantics, both on pen&paper and formalisations (inductive with that signature), and what is standard in Lean for relations. But if there are good reasons to switch we can discuss the definition, no problem. I'm trying to stick to 'define things as expected and then prove they're equivalent to other formulations' as a general rule. People could also want the coalgebraic and dialgebraic views, etc.

[Fabrizio Montesi]

I still need to go through it all, and you make lots of good comments, but these seem to be more appropriate for more powerful automata than Dfas. Having finiteness assumptions and a start state is part of the accepted definition of Dfa.

To generalise, I'd prefer having separate definitions and then either show conversion defs or instances for Dfas and the like. This is what I've explored with LTS as an example: https://github.com/leanprover/cslib/blob/3fe4da76a31b58c9f4372616020dc0f9e7e27665/Cslib/Computability/Dfa/Basic.lean#L67

[Fabrizio Montesi]

Re 3: I don't understand what you mean. We don't even have Nfa yet, and I fully agree with what you wrote. :⁠-⁠)

Re 4: as for 3? We have a definition of Lts, and then various predicates formalising their standard classes (image finite, deterministic, etc.).

Perhaps what's confusing here is what I meant by general definition. I don't wanna have a single definition for all kinds of automata (the most general ones are arguably Lts for discrete stuff and then even more general versions when going beyond); first, I'm trying to see if we could agree on a definition for Dfa that suits the different developments that people have done/are interested in.

[Fabrizio Montesi]

Re bundled vs unbundled: I'm trying to stick to unbundled State and Symbol/Label types because it's the standard approach and it does seem to work nicely. But I think I've encountered the problems you mention regarding union and other operations when working with LTS. I haven't played enough with those yet. In fact, Dfas might be a better/simpler place to understand the ergonomics of all of this.

[Ching-Tsun Chou]

If you just want to define DFA, what's wrong with the current DFA definition in mathlib?
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/DFA.html
Regarding finiteness assumptions: I never once needed to assume that the alphabet/symbols is finite in my automata theory project, while many (though by no means all) theorems depend on the state space being finite. This is not surprising if you think about it. Once the state space is finite, the automaton can only distinguish the symbols to a finite degree of "resolution" anyway.

[Ching-Tsun Chou]

Regarding bundled vs unbundled state space: an unbundled design is probably a good idea if you want to develop automata theory for all universe levels. My bundled design gave me endless troubles when I tried to use Type* instead of Type.

[Ching-Tsun Chou]

For the usual closure properties of regular languages under the boolean operations (union, intersection, and complementation), concatenation, and Kleene star, I don't think any of the corresponding automata constructions in the proofs actually needs to assume that the automata are finite-state. In fact, for union and intersection, one doesn't even need to assume that only finitely many automata are involved. It is actually in the case of ω-regular languages that one often needs to make finite-state assumptions.

[Fabrizio Montesi]

I agree on that, to show many common properties about Dfas, we don't need all the assumptions typically bundled (on pen&paper) in textbook presentations of Dfa.

The issue I'm concerned with is that this means we have to choose between (as far as I see now):

1. Formalise Dfa with fewer assumptions and call it a day.
2. Formalise Dfa as expected, and write all definitions and theorems that do not need the 'extra' assumptions for a more general structure or class. Code things such that those easily/directly apply to Dfa.
3. Formalise Dfa with fewer assumptions (this is like 2, but we're calling the more general structure Dfa), and then formalise a Dfafs (or something like that) which is the actual formalisation of Dfa (with all the standard assumptions). Explain why we have this in the documentation.

My current view is that 2 is a good compromise. 3 might also work (the acronym Dfa says nothing about finite alphabet, so we could consider challenging tradition).
1 seems a bit dangerous when I think about (a) somebody eventually trying to prove any reasonable theorem that requires a standard assumption that we decided to exclude (then we'll have to introduce the assumption) and (b) people learning CS through CSlib (though this can be ameliorated with good documentation).

I think we should be very explicit about what we're doing, since my experience is that even the tiniest question mark/deviation in the formalisation of an established concept can make people roll out yet another version. There should be space for the hierarchy of assumptions.

What do you think?

Btw, do you think that (a) is never gonna be an issue?

[Fabrizio Montesi]

Side comment: it is really great that something as simple as Dfa raises these questions, thanks for the good discussion so far.

[Ching-Tsun Chou]

In my automata theory project I took approach 1. I have a namespace Automata and define Automta.NA and Automata.DA classes for nondeterministic and deterministic automata, respectively. Automata.NA and Automata.DA include only the initial state(s) and the next state(s) function and nothing else. Finite-state assumptions are made in theorems only when needed. I think exposing the actual logic in the proofs is more important than agreeing with what the textbooks say.

[Ching-Tsun Chou]

As far as I can see, finite-alphabet assumptions will only be needed in the equivalence of finite automata and regular expressions. Like the finite-state assumption, it can be made only when needed.

[Ching-Tsun Chou]

I'm not concerned about (a). For a theorem to have a long list of assumptions is not uncommon in Lean. If someone can't prove a theorem because of a missing assumption, I expect he/she will soon realize that and add the necessary assumption (and only the necessary assumption).

[Ching-Tsun Chou]

Need to go to bed now. Talk to you tomorrow.

[Fabrizio Montesi]

Isn't what you're describing more akin to approach 2? Your code gives me the same impression: you have defined a more general structure than Dfa, given it another name (DA), and proven things about this more general structure.
My only addition in (2) is that the definition of Dfa should also be allowed to exist, and inherit somewhat all the stuff proven about the more general structure (in your case DA).

Approach (2) is in line also with this:

I think exposing the actual logic in the proofs is more important than agreeing with what the textbooks say.

Are we then discussing whether the 'standard' definition of Dfa (with the finite alphabet assumption) should even be formalised? That for me would depend on whether there is at least one interesting definition/theorem that can be given with the additional assumption. I was working under this hypothesis.
Are you saying that Dfa and DA cannot be distinguished in any meaningful way? (I don't think you are, judging from your last message.)

[Ching-Tsun Chou]

OK, I now understand you better. Yes, I think it would be a good idea to have a class Automata.DA for deterministic automata which has only fields for the initial state and the next state function and then extend Automata.DA to Automata.DFA with finite-state and perhaps also finite-alphabet assumptions. Similarly for Automata.NA, Automata.NFA, and Automata.EpsilonNFA. Regular languages will be defined as languages accepted by Automata.NFA, but accepted languages will be defined more generally for Automata.NA. There is no need to define accepted languages for the deterministic automata, because they can be easily converted to nondeterministic ones via Automata.DA.toNA.

I have put everything above in an Automata namespace, because that would give us more freedom in choosing names in that namespace.

[Fabrizio Montesi]

So let's see, we have..

Transition systems:

• Lts State Label: just a transition relation. Bisimulation, Trace Equivalence, etc. are defined on this.
• RootedLts State Label: extends Lts with a root (which in automata is the initial state).

Automata:

• Automaton State Symbol: start state and accept (Finset of accept states). If we required the user to give us a toLts function, we could define Accepts here, but it's probably excessive.
• DA: extends Automaton with a transition function State -> Symbol -> State. Offers .toNA, .toRootedLts, and proofs of correctness of these encodings.
• NA: extends Automaton with a transition function State -> Symbol -> Set State. Offers .toRootedLts.
• Dfa: extends DA with finite-state and finite-label assumptions. As this extends DA, it offers .toDA and inherits all the nice things from DA.
• Nfa: similar to above.

[Fabrizio Montesi]

Since the point of automata is accepting/rejecting strings, should we make accepts : List Symbol -> Bool(or Accepts : List Symbol -> Prop) a field of Automaton maybe? That way we can define the language of an automaton already at that level.

(Edit: mmmh, that'd make the rest kinda redundant, conflating this with what a Language is..)

[Alexandre Rademaker]

What about the question from @Ching-Tsun Chou about the motivation to define DFA in CsLib considering the definition in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/DFA.html? We also have turing machines and NFA in Mathlib.

[Ching-Tsun Chou]

My preferred design is described below. You can think of it as a refactoring of the relevant code in mathlib.
(1) Put everything in a new namespace Automata.
(2) Use an unbundled design, so that the state type (S below) and the alphabet type (A below) are parameters.
(3)Automata.NA (for nondeterministic automata) and Automata.DA (for deterministic automata) are the two root classes
(3.a) Automata.DA has the following fields:

start : S
step: S → A → S

(3.b) Automata.NA has the following two fields:

start : Set S
step : S → A → Set S

(3.c) Automata.εNA has the following fields:

start : Set S
step : S → Option A → Set S

(4) The DFA,NFA and εNFA in mathlib can be defined as extensions of Automata.NA and Automata.DA, respectively. I would like to put mathlib's DFA, NFA, and εNFA in the Automata namespace as well.
(5) Now that we have a separate (DA,NA,εNA) and (DFA,NFA,εNFA), the finite-state and perhaps also the finite-alphabet assumptions can be added to the latter.
(6) Separate extensions of (DA,NA) will be defined for Buchi automata, Muller automata, etc.

Comment: It is not a good idea to define NA to have a single initial state. First, technically, think about how you prove that the union of the languages of two NAs is again accepted by an NA. With the design given above, there is a straightforward sum construction on nondeterministic automata that even works over an arbitrary index set. If an NA can have only a single initial state, a more complicated construction is needed. Second, philosophically, why is nondeterminism allowed only on transitions but not on the choice of the initial state?

[Snir Broshi]

I like this design, though I still think S → Prop is preferable to Set S since that's how relations are usually defined in mathlib (see docs#SimpleGraph for example)
As for having a single initial state, we can add NA₀, εNA₀, NFA₀, εNFA₀ variants for those and define translations. I'm also in favor of having multiple start states as the canonical NFA.

Regarding acceptance conditions: How about having a very general repeated transition function which takes an LTS, a set of states, and a sequence Stream'.Seq Label, and returns Set (Stream'.Seq State)? Then DFA/NFA acceptance conditions will operate on .toList.getLast? (just the state reached), and we can define Buchi/Rabin/Miller/Strett on the infinite sequence

[Fabrizio Montesi]

@Ching-Tsun Chou So your design is like what I wrote, but without Automaton because of the difference in start states between DA and NA. I'm happy with that, because I agree with you that NA should have a set of initial states. There is also precedent for that choice in research papers (e.g., https://dl.acm.org/doi/abs/10.1145/2490818). We should mention this in the docs.

I have a few comments on style, I'll write a separate message about that.

[Ching-Tsun Chou]

Snir Broshi said:

I like this design, though I still think S → Prop is preferable to Set S since that's how relations are usually defined in mathlib (see docs#SimpleGraph for example)

The set option seems more common in textbooks (Hopcroft & Ullman, Kozen) and also supports a very natural expression of the powerset construction:
https://github.com/ctchou/AutomataTheory/blob/c75ca6877960a98adf88d2a1a9ff26be668f4fdc/AutomataTheory/Automata/PSet.lean#L32

As for having a single initial state, we can add NA₀, εNA₀, NFA₀, εNFA₀ variants for those and define translations. I'm also in favor of having multiple start states as the canonical NFA.

I don't think we need them, because they can be easily realized by instantiating start with a singleton set.

Regarding acceptance conditions: How about having a very general repeated transition function which takes an LTS, a set of states, and a sequence Stream'.Seq Label, and returns Set (Stream'.Seq State)? Then DFA/NFA acceptance conditions will operate on .toList.getLast? (just the state reached), and we can define Buchi/Rabin/Miller/Strett on the infinite sequence

In the automata literature I've seen, an automaton operates either on finite words or on infinite words, but never both.

[Fabrizio Montesi]

Style comments:

• I think we should write Symbol, not A (or Alphabet), for the type of symbols. x : Alphabet to say that x is a symbol is weird.
• Afaik, step is normally called 'transition function', so it should be called tr.
• I don't remember where/when, but I was told that LTS should be named Lts, which would mean that DFA should be Dfa. But I'm not convinced of this anymore, so I suggest I just revert Lts to being LTS and we keep all uppercase for the automaton names. ;-)

[Fabrizio Montesi]

Re εNA: I'd like to understand better the use of Option, as opposed to Sum with an epsilon type or something like that. Could you elaborate a bit? Is it just convenience?

[Ching-Tsun Chou]

I chose the names "start" and "step" simply because they are what automata in mathlib use. It seems to me a good idea to match mathlib so that what we do can become a drop-in replacement for the relevant parts of mathlib without too much trouble. The εNA also follows mathlib, where none gives you the ability of changing state without consuming a symbol.

Either Symbol or Alphabet is fine with me. I just don't want to use Greek letters for type names like in mathlib, because α and σ look awfully like each other in all the fonts I've played with.

Personally I prefer DFA over Dfa because this is an acronym every letter of which begins a word, but not itself a word. This is also what mathlib uses.

[Fabrizio Montesi]

The current rule of thumb in cslib is that Greek letters work fine only when they match what people are used to or one doesn't wanna be descriptive on purpose. Here being descriptive is good, so no Greek.

[Fabrizio Montesi]

As for step, that looks like it should really be tr, to match both pen&paper and the Tr in LTS. Some things from mathlib will need some adaptation if/when ported anyway.

[Fabrizio Montesi]

I'd like to give some thought to the signature of the transition function in NA (ending in Prop vs ending in Set State, as @Snir Broshi mentioned). There's some tension there as to what gets easier or harder. One advantage of Set is that we get membership notation and some constructions.

But choosing Tr : State -> Symbol -> State -> Prop has some advantages as well. For example, NA could be just an extension of LTS. As we're discussing things, an NA is actually just an LTS with some initial states. If that holds, we should consider making this formal. That way we'd inherit all definitions and theorems for LTSs directly, with no need for conversion functions.

(Note I'm not saying we should do this just yet, I'm just brainstorming.)

[Fabrizio Montesi]

(Keeping track of how some of these decisions would look like in code here: https://github.com/leanprover/cslib/tree/automata/Cslib/Computability/Automata.)

[Ching-Tsun Chou]

I would prefer sticking to the current names and conventions used in mathlib for automata theory. It takes efforts changing them and I don't see any point in spending that effort. In any case, Lean has good support for moving between sets and predicates: given s : Set X, (· ∈ s) is the corresponding predicate, and given p : X → Prop, {x | p x} is the corresponding set. So LTS theorems should be readily usable by automata theory even if the latter uses sets instead of predicates.

[Ching-Tsun Chou]

For example, suppose NA is defined using sets:

structure NA (Symbol : Type*) (State : Type*)  where
  start : Set State
  step : State → Symbol → Set State

We can define:

def NA.toLTS {State : Type*}  {Symbol : Type*} (M : NA Symbol State) where
  Tr := fun s a s' ↦ s' ∈ M.step s a

With the dot-notation, we can write M.toLTS which can then use the theorems about LTS.

[Fabrizio Montesi]

Well, one point is that we'd be able to (more directly) apply automata theory to studying the operational semantics of terms given in a language formulated languages given as LTS.

Another point is that we'll avoid a lot of boilerplate, since many definitions and theorems I see about NAs do not need the initial states, they can be formulated (and make good sense to have) for LTS. For example,

/-- The `μ`-image of a state `s` is the set of all `μ`-derivatives of `s`. -/
@[grind]
def LTS.image (s : State) (μ : Label) : Set State := { s' : State | lts.Tr s μ s' }

/-- The `μ`-image of a set of states `S` is the union of all `μ`-images of the states in `S`. -/
@[grind]
def LTS.setImage (S : Set State) (μ : Label) : Set State :=
  ⋃ s ∈ S, lts.image s μ

Edit: also this

/-- The set of outgoing labels of a state. -/
def LTS.outgoingLabels (s : State) := { μ | lts.HasOutLabel s μ }

[Ching-Tsun Chou]

I really don't want to deviate from how mathlib does things if possible. It is not easy or pleasant to make changes in mathlib (for example, see #mathlib4 > Why is Stream' called Stream'?). I'd rather write boilerplate code and prove adapter lemmas if I need to use results from LTS. The latter is under my control; mathlib isn't.

[Chris Henson]

Ching-Tsun Chou said:

It is not easy or pleasant to make changes in mathlib (for example, see #mathlib4 > Why is Stream' called Stream'?)... mathlib isn't [under my control]

I disagree. That thread seems receptive, just wanting to make sure to evaluate pros/cons. We have already made small upstreams to Mathlib, and will continue to do so.

[Ching-Tsun Chou]

Frankly, I now regret starting that thread about Stream'. In retrospect, I don't think that's a good way to spend my time. I don't want to repeat the experience.

[Fabrizio Montesi]

@Ching-Tsun Chou I understand the lack of enthusiasm for investing a lot of time discussing API design when you wanna get things done.
But I'd still like to understand what we're balancing here. Are you saying that (a) you think extending LTS from NA would be the better technical choice but your concern for mathlib compatibility makes you not want it anyway, or (b) you think even thinking about these design issues is a waste of time, because mathlib compatibility takes precedence anyway?

This is a cs concept, so we're the ones who should think about this carefully. We've already gained quite a bit from this discussion, I think.
(I'm also asking colleagues about how this will affect probabilistic models later on, since I remember similar boilerplate gets problematic there..)

Another reason for which I'd like to understand this well is that this would be the first place where we introduce using Set to model nondeterministic semantics. Both LTS and ReductionSystem use the standard relation to Prop instead.

[Ching-Tsun Chou]

Sorry for the late reply.

Yes, I think compatibility with mathlib should take precedence. Whether the transition part of an automaton is called step or Tr or next is of no real mathematical consequence. Personally I do not want to spend my time fighting it.

As to whether the transition part of an automaton should have the type State → Symbol → Set State or State → Symbol → State → Prop, I think both options are valid and both have long traditions, though I think the former has a longer tradition. Attached below is Rabin and Scott's seminal 1959 paper in which the notion of a nondeterministic automaton first appeared:
Rabin and Scott - Finite_Automata_and_Their_Decision_Problems.pdf
Take a look at Definition 9 on page 120, which uses the first option. As far as I can tell, most of the subsequent textbooks on automata theory also continued that tradition.

All the above is just a long way for me to say that there is nothing wrong with both options to exist in mathlib and I think it is even valuable to have definitions and theorems for going back and forth between them.

A personal rant: If Lean didn't have "sets" in the first place, we wouldn't need to discuss this topic at all. I once raised the topic of why does Lean have "sets" at all and was promptly shot down:

#new members > How do I prove this about Nat.nth? @ 💬

[Chris Henson]

How entrenched are the automata definitions in Mathlib? Loogle seems to indicate that docs#DFA and docs#NFA are used just in leaf files in Computability. How much more than that is there? What I'm getting at is that I am more open to deviating from the current definition if we feel it is a high benefit and not too onerous to upstream (or even downstream, but that's a different discussion).

[Shreyas Srinivas]

I recall that mathlib maintainers might be happy to see some of the computability stuff offloaded to CSlib since it is more on-topic here

[Chris Henson]

Shreyas Srinivas said:

I recall that mathlib maintainers might be happy to see some of the computability stuff offloaded to CSlib since it is more on-topic here

With this in mind, I think we are free pick the spellings we find most useful, then plan to migrate the Mathlib automata code to CSLib.

[Ching-Tsun Chou]

I posted a query in the mathlib4 channel to verify @Shreyas Srinivas 's claim:
#mathlib4 > Is there a plan to offload Mathlib.Computability to Cslib? @ 💬

[Shreyas Srinivas]

It has been a while but I believe you might be able to search some zulip conversations where this was mentioned

[Ching-Tsun Chou]

I want to see a clear policy statement from the community, not just (possibly personal) opinions expressed in a discussion thread.

[Shreyas Srinivas]

Sure. But I think “theoretical computer science is surely part of mathematics” is a highly non-obvious and disputed claim. Nevertheless, the separation is not always well-defined and the boundaries are fuzzy. So getting a clear statement on this will be difficult from a technical standpoint.

[Ching-Tsun Chou]

Strangely, one of the most eminent theoretical computer scientists/mathematicians wrote an entire book (which you can download for free):
https://www.math.ias.edu/avi/book
to express the opposite view. You may recall that Wigderson was awarded both the Abel Prize and the Turing Award (among many other awards).

[Shreyas Srinivas]

That's a book on computability and complexity. I don't see how it supports your claim

[Fabrizio Montesi]

Shreyas Srinivas said:

I recall that mathlib maintainers might be happy to see some of the computability stuff offloaded to CSlib since it is more on-topic here

ditto

[Fabrizio Montesi]

Anyway, in general, we're willing to maintain automata theory at cslib. I'm making some progress on how it could look like taking the discussion so far into consideration, will show some more soon.

[Ching-Tsun Chou]

A new question: Why is the field Tr of Lts capitablized? The field names of structures in mathlib seems consistently lowercase. Also, isn't Tr a bit too short and hence ambiguous? (There is "trace" in linear algebra, for example.). Wouldn't trans be a more informative name that's just slightly longer?

[Chris Henson]

Ching-Tsun Chou said:

A new question: Why is the field Tr of Lts capitablized? The field names of structures in mathlib seems consistently lowercase. Also, isn't Tr a bit too short and hence ambiguous? (There is "trace" in linear algebra, for example.). Wouldn't trans be a more informative name that's just slightly longer?

I believe the captialization correctly follows the Mathlib naming conventions for a non-Prop field? Please correct me if that's wrong. I'll otherwise defer to @Fabrizio Montesi on the matter of a more descriptive name.

[Ching-Tsun Chou]

Well, propositions like associativity seems to get lowercase names in algebraic structures; for example:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#Monoid

[Chris Henson]

It is possible I am wrong, or that is an example of "some fields of structures are currently wrongly lower-cased" the conventions page mentions.

[Ching-Tsun Chou]

[ I was writing the following when @Chris Henson 's message above appeared. It adds one more aesthetic argument. ]

It occurred to me that there is an aesthetic argument for why the next-state transition of a nondeterministic automaton should have the type (where S and A are the types of states and alphabet/symbols, respectively):

S → A → Set S

The argument is that the above type has a nice formal correspondence with the next-state transition of a deterministic automaton:

S → A → S

The naming convention discussion above gives one more argument: we can use the same field name in both NA and DA cases, rather than capitalizing the former but lowercasing the latter.

[Ching-Tsun Chou]

In any case, the above makes me think that perhaps we can extend the API of Lts:

def Lts.next {A : Type*} {S : Type*} (lts : Lts S A) : S → A → Set S := {s' | lts.Tr s a s'}

Then Lts.next provides an alternative, set-valued view of Lts.Tr and, with the dot-notation and suitable theorems, the two can be used interchangeably, depending on the user's preference. For example, there can be a set-valued counterpart of Lts.MTr.

[Fabrizio Montesi]

Re style of Tr etc.: I'm trying to follow mathlib's conventions, yes. I think they have some tech debt wrt notation, if I understand correctly. If you think I've interpreted something wrongly, please let me know.

[Fabrizio Montesi]

Ching-Tsun Chou said:

In any case, the above makes me think that perhaps we can extend the API of Lts:

def Lts.next {A : Type*} {S : Type*} (lts : Lts S A) : S → A → Set S := {s' | lts.Tr s a s'}

Then Lts.next provides an alternative, set-valued view of Lts.Tr and, with the dot-notation and suitable theorems, the two can be used interchangeably, depending on the user's preference. For example, there can be a set-valued counterpart of Lts.MTr.

That's exactly the road I've been following the past couple of days. Note LTS already has image (which is a standard concept and name there), which does almost that but starts from a single state. I extended it to setImage and multistep definitions as well, which have the signatures you want I think.

[Fabrizio Montesi]

Alright people, I think I'm ready to show a proposal in code, which I hope makes sense to you. Feedback is welcome. Explanation below. Current code at: https://github.com/leanprover/cslib/tree/automata/Cslib/Computability/Automata

Structure

We have the following components.

• LTS, modelling transition systems as a transition relation Tr : State → Label → State → Prop. Nothing else, no assumptions are made on Tr.
• NA (nondet automaton), which extends LTS with start and accept fields; both have type Set State. In all automata, I call the type of labels Symbol to be more familiar.
• DA (det automaton), which is independent. It has a start state, a set of accept states, and a transition function tr : State → Symbol → State.
• DFA, which extends DA with finiteness assumptions on state and symbol types.

This design worked out pretty nicely (see next section). It's the result of trying many things, so it's good to mention what didn't work well (hopefully not just because of me being clumsy). I'll report on that at the end.

Development

• I have extended LTS with plenty of definitions and results about 'image transitions'. In particular, I've built on the existing LTS.image definition (which returns the set of all states reachable by a state with a given label) to define LTS.imageMultistep (the set of all states reachable by a state through multistep transitions on a given list of labels) and their natural extensions to input sets of states instead of states, LTS.setImage (the union of all LTS.images of the states in an input set) and LTS.setImageMultistep (same, for LTS.imageMultistep). These definitions come with characterisation results that link set membership and equality to the existence of (multistep) transitions.
• Since an NA is an LTS, I can define the transition function in the subset construction NA.toDA as just tr : na.setImage.
• Thanks to the characterisation results for image transitions in LTS, I could easily prove that the standard multistep transition function (defined in DA) of NA.toDA is equal to LTS.setImageMultistep.
• From the above, correctness of the subset construction (na.language = na.toDA.language) is straightforward (https://github.com/leanprover/cslib/blob/898d941058f2cf49088122d612c60707c6ab622e/Cslib/Computability/Automata/DA.lean#L157).

Many of these proofs are just a single call grind, sometimes preceded by a simple line or two.

Alternatives that did not work well

• Making DA extend LTS. It's possible: I just had to add a default about the definition of the transition relation (from a transition function put in another field) and a propositions that enforces that default (that's standard in Lean). But I didn't like that something as simple as a DA ended up having so many fields and surprising internals. So I opted for providing a DA.toNA and an automatic coercion.
• Making a structure Automaton (tried both one that extends LTS and one that doesn't) that NA and DA extend. The only meaningful thing I could do in Automaton was requiring an Accepts : List Symbol → Prop field and then define language based on that. While this makes sense as a contract, it's not really what Lean structure extension/inheritance is useful for, as people could then override it. I found all of this clunky and discarded it.
• Making NA not an extension of LTS but rather an isolated structure. Outside of the notion of acceptance, which is the conceptual extension from LTS to automata, I repeatedly encountered the issue that, when defining something, I could either duplicate code from LTS (and prove it equivalent to the one in LTS) or make the definition use toLTS and invoke whatever I needed from LTS. The former means lots of boilerplate, the latter means giving indirect definitions. Both implied that I needed results about LTS anyway. When I tried extending LTS, this pushed me to extending LTS with lots of useful things that do not depend on the notion of acceptance, which I took as a positive sign.

[Notification Bot]

A message was moved from this topic to #CSLib > Project board by Fabrizio Montesi.

[Ching-Tsun Chou]

@Fabrizio Montesi I think what you have now is pretty good. I'll take a closer look and provide more concrete feedbacks later.

I think some of the constructions on NA actually make perfect sense on LTS. Examples include sum and product constructions:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Automata/Sum.lean
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Automata/Prod.lean
Do they already exist in the LTS literature?

Your experience with failed attempts accords with my own. I think there is actually a deeper mathematical reason behind this. In the usual automata theory textbooks, the closure properties of regular languages are all proved using construction on NA, except for the closure under complementation, which uses a construction on DA and a NA → DA conversion. Only recently did I learn from reading Choueka's paper that it is actually possible to prove all the closure properties using DA alone, including the constructions for concatenation and Kleene-star. So DA is very much its own thing and not really a special case of NA, as it superficially seems to be.

[Fabrizio Montesi]

That's good to hear!

As far as I know we typically deal with union for LTS (which might be Sum? I'll have a look), but the literature is vast and there might something similar.
I'm certainly finding it very nice to apply things I know are normally formulated for NFAs to LTS, so looking at what constructions we can generalise seems very good to me.

I've added to the branch an example of how epsilonNA could be formulated, keeping the Option design choice. I'm basically instantiating \tau-transitions as none-transitions, and then the transition relation is 'just' what we call saturated transitions in LTS. Hopefully this will yield a very easy proof of its correctness (theorem toNAWithoutEpsilon_language_eq, still have to try).

[Fabrizio Montesi]

Once we're done looking at these automata on finite words, I'd really like to look together into how your work on omega automata applies here. (There you're more of an expert, I think, so I'd suggest you create those files, if you're willing.)

[Ching-Tsun Chou]

Yes, I can work on creating those files.

[Ching-Tsun Chou]

I created a PR for a new datatype ωList to represent infinite words:
https://github.com/leanprover/cslib/pull/80
I assume that finite words will be represented by List.

[Snir Broshi]

1. ωList is a great name
2. Why not rename Mathlib's Stream' to ωList instead of diverging?

[Ching-Tsun Chou]

Snir Broshi said:

1. ωList is a great name
2. Why not rename Mathlib's Stream' to ωList instead of diverging?

Please read this thread: #mathlib4 > Why is Stream' called Stream'? . Renaming Stream' to something else was my original proposal. In particular, I think Mario wants to keep Stream' for coinductively defined streams that may become a reality in the future, at which point the implementation of Stream' will change completely. Also, he does make a good point about the disruptiveness of name change of existing API.

[Snir Broshi]

I thought that thread was actually going to rename Stream', did they decide against it?
I don't think that many things rely on Stream' for it to be disruptive.
Also you didn't suggest ωList there, which I think is the best name suggested so far.

[Ching-Tsun Chou]

Read the end part of the thread. The name ωList occurred to me only afterwards. Anyway, my PR is for cslib, not mathlib.

[Snir Broshi]

Oh well. How about defining aliases for it in CSLib then?
For example def drop (n : ℕ) (s : ωList α) := Stream'.drop n s
Then Stream' will be the source of truth, and CSLib will only contain the rename.
I'm against copying code, that usually creates problems.

[Ching-Tsun Chou]

@Snir Broshi , do you mind making your comments on ωList in the PR instead? Thanks!

[Ching-Tsun Chou]

@Fabrizio Montesi I have some comments about your automata code:

1. I would recommend moving the accepting condition from DA and NA to DFA and NFA. This is because NA and DA will also be used for automata on infinite words and those automata can have more complicated accepting conditions. For example, the accepting condition of a Muller automaton is a set of subsets of states and that of a Rabin automaton is a set of pairs of subsets of states. By removing the accepting condition from DA and NA, you will allow Muller and Rabin automata to be defined as extensions of DA and NA.
2. As part of the above, the definitions and theorems related to accepted languages should also be moved from DA/NA to DFA/NFA. But the NA section of DA (namely, the stuff related DA.toNA) can stay in DA.
3. I think the subset construction should be split into a separate file. Each automata construction should get its own file.
4. I wonder if the finite_symbol assumption is warranted in DFA, NFA, etc. As I mentioned before, this assumption is not needed in all the automata theory results I've seen and the only place I think it is needed is to ensure that a regular expression is a finite object. Maybe it should be left out and brought in only when needed.
5. I recommend introducing a namespace Automata above DA and NA, because the latter are very short names and we may want to re-use them in a different context.
6. Nitpick: You probably want to add explicit variable declarations of State, Symbol, etc, rather than leaving them implicit.

[Ching-Tsun Chou]

One more comment: I think I still prefer Alphabet over Symbol. I know an expression like x : Alphabet looks weird, but so do Finite Symbol, finite_symbol, and Language Symbol (see Language). Alphabet is the standard terminology. Let's use it.

[Fabrizio Montesi]

@Ching-Tsun Chou Thanks for the good comments.

1. Right.. Also, I've just added EpsilonNA, and it shows that problem, too (it extends NA, but its acceptance condition is different than NA, which is just gonna cause headaches!). I've moved things around.
2. I've moved this to DFA and NFA for now, too, for consistency. The problem is that the proof of correctness of that translation requires knowing the notion of acceptance. I would come back to this once we merge the first omega automata, so that we can look at what we can unify.
3. Done -- and every translation now has its own file. We can come back to this too.
4. I think it might be important once we get to regexps (like you say) and how to compute things with automata. So for now I'd keep it around (also because we need to keep them around in the translations between automata). We might wanna reconsider this and extend the hierarchy once we get further down the road of regexes, etc. But it's nontrivial to figure out the names, so for now I'm happy to postpone this problem. It might also very well be, like you say, that it might suffice to take these things as parameters where needed. I'd just like to see some code that uses these things before committing to a choice.
5. With the new structure where lots of things have been moved to DFA, NFA, etc., I hardly use DA or NA outside of structures that extend them, so I didn't perceive it as a big problem any longer. But I'm happy to reconsider this if some code starts getting too clunky; it's easy to change.
6. Lean seems to do the right and intuitive thing, but I agree it wouldn't hurt.. I'll keep that in mind for future edits of these files. (Or if anybody wants to make a PR for this, it'd be welcome.)

[Fabrizio Montesi]

Ching-Tsun Chou said:

One more comment: I think I still prefer Alphabet over Symbol. I know an expression like x : Alphabet looks weird, but so do Finite Symbol, finite_symbol, and Language Symbol (see Language). Alphabet is the standard terminology. Let's use it.

I'll mull over it. I see your point but for some reason my brain switches to set theory when I hear alphabet and I get some cognitive dissonance when then looking at the Lean code..

[Fabrizio Montesi]

I think we have a good design now, so I've made a PR that summarises everything so far: https://github.com/leanprover/cslib/pull/83

[Ching-Tsun Chou]

@Fabrizio Montesi Your automata PR looks good. I've added some comments.

[Fabrizio Montesi]

I can't seem to find them?

[Ching-Tsun Chou]

Hmm, I can see them: https://github.com/leanprover/cslib/pull/83. There are 4 comments.

[Fabrizio Montesi]

can you link to one of them? I see only @Chris Henson's comments for some reason.

[Fabrizio Montesi]

You might need to submit the review, if you've started a review.

[Fabrizio Montesi]

better :)

[Ching-Tsun Chou]

Can you see them now?

[Fabrizio Montesi]

yep!

[Ching-Tsun Chou]

Great!

[Fabrizio Montesi]

all done, modulo the last two comments (see my replies), which I agree with but since they're backwards compatible extensions I'd like to address them in a future PR.

[Fabrizio Montesi]

Thanks both, very good comments

[Ching-Tsun Chou]

I created a PR to show what the definitions of Büchi and Muller automata will look like:
https://github.com/leanprover/cslib/pull/85
Unfotunately, since it depends two other PRs, the PR shows too many changed files. The only really relevant files are:
Cslib/Computability/Automata/{DA,NA,BuchiNA,MullerDA}.lean

[Chris Henson]

As a reminder, you can link to PRs like this: cslib#85

[Fabrizio Montesi]

Just caught up with the discussion on OmegaList. There seem to be valid points on both sides.
Before I think more about this, could somebody explain why nobody has gone for the negative coinductive formulation (see, e.g., https://rocq-prover.org/doc/V8.14.1/refman/language/core/coinductive.html#caveat and https://proofassistants.stackexchange.com/questions/4142/what-is-a-positive-coinductive-type-and-why-are-they-so-bad)? That is something like:

structure ωList (α : Type _) where
  head : α
  tail : ωList α

One can then even define a view like this if we need it (this is just an example, we should use other functions in this, like skip I guess):

def ωList.toFunction (l : ωList α) (n : Nat) : α :=
  match n with
  | 0 => l.head
  | n + 1 => l.tail.toFunction n

Is this just unworkable when making interesting definitions, because of termination checking? I haven't tried it much, just wanted to hear opinions.

[Chris Henson]

My assumption was that the type of Stream' was selected because it was determined to be the easiest way to emulate coinductive definitions given such issues.

[Ching-Tsun Chou]

Attached below is a page from the following survey article:
automata on infinite words.pdf

Thomas, Wolfgang (1990). "Automata on infinite objects". In Van Leeuwen (ed.). Handbook of Theoretical Computer Science. Elsevier. pp. 133–164.

That's the sort of thing I want to formalize. Does anyone see co-induction there? (If you do, please specify where precisely you see it used.) Is a type that is basically ℕ → α but also supports the dot-notation not good enough? For example, the following notations:
image.png
are called s.extract m n and s.drop m, where s : ωList represents an infinite sequence. (Note that the naming convention agrees with that of List quite nice.) The following function:
image.png
is translated quite literally as:

def ωList.infOcc {X : Type*} (xs : ωList X) : Set X :=
  { x | ∃ᶠ k in atTop, xs k = x }

Yet someone was telling me that (1) I should be using Stream' and (2) with an expression like xs k, I have committed the sin of "defeq abuse".

[Chris Henson]

As I said in the review (cslib#80), my mention of potential defeq abuse is not my primary issue. My main concern is the tradeoffs of duplicating code from Steam' in CSLib. I think I have written down all my relevant thoughts on the review.

[Fabrizio Montesi]

I've been reading up some papers and the discussions on Zulip. Much of the discussion on Stream' stems from the fact that Stream''s goal is to be a data structure that cannot be written yet, so for now it's defined as a function hidden by a good API. We shouldn't confuse the two concepts.

I've drafted a new design in the branch omega-sequence to facilitate our discussion: https://github.com/leanprover/cslib/tree/omega-sequence

In particular, you'll find two files:

• Cslib.Foundations.Data.OmegaList, defining the data structure ωList. This is probably useless until we get good support for coinduction. It is what Stream' is intended to be, i.e., a data type to be used in programs. But although it cannot be inhabited, I could write some definitions about it, so we can at least keep track of some basic things and the fact that we want it to be translatable into an ωSequence.
• Cslib.Foundations.Data.OmegaSequence, defining ωSequence as a function ℕ → α. This is what @Ching-Tsun Chou is using. ωSequence embraces that it is supposed to be used as a function (whether it is defined as such doesn't matter too much).

Of course, since the implementations of ωSequence and Stream' are coincidentially the same for now, this will lead to some duplication of code. So I'd like that we port features from Stream' to ωSequence only when they're actually used.

@Ching-Tsun Chou, questions:

• Do you need to write s i or would you be equally happy with writing s[i]? We can easily define a GetElem instance that never requires a side-condition.
• Are you happy with replacing ωList with ωSequence in your code? (I've taken the liberty of putting your name on top of the ωSequence file for now, since it's basically your ωList.)

[Fabrizio Montesi]

I'm proposing this also because even in mathlib there are different uses, like here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Sequence.html#Polynomial.Sequence

[Ching-Tsun Chou]

I'm happy with the name ωSequence. Although it is longer than ωList, it is also a more accurate description of what the type actually is. But I do not like to write s[n]. Since we have made it clear that ωSequence α is but a (thin) abstraction of ℕ → α, we should take that POV seriously and be able to use the function application notation s i and not clutter the code with pointless [...]. (In contrast, there is a good reason for List and Array to use the [...] notation, because out-of-bound access is not well-defined. So several variations [...]'h, [...]?, and [...]! need to be differentiated and supported. This is obviously not an issue for ωSequence: s n is always well-defined for any s : ωSequence α and n : ℕ.)

I do have a concern about using the name ωList for the co-inductive version of infinite sequence. The concern is not about the name itself, but about the fact that we are probably going to use the existing List type for finite sequences/words. So the question may be raised about why we choose to use List to represent finite words/executions but use ωSequence instead of ωList to represent infinite words/sequences. The answer is of course that the theory of ω-automata (or temporal logic, for that matter) just doesn't use co-induction in its development, while the theory of automata on finite words will frequently take advantage of the inductive structure of List. But that's an answer that is probably too long to avoid all confusions. Perhaps a better name for the co-inductive view of infinite sequences could be ωStream? The current Stream (without the prime) type in mathlib is a type of both finite and infinite sequences, so the ω in ωStream would be quite appropriate. (Admittedly, one thing I learned from all these discussions is that there seems to be a lot of disagreements about what exactly a "stream" is in the literature.)

[Pieter Cuijpers]

Fabrizio Montesi said:

Tested a bit the first route and it looks pretty ok to me. :)

https://github.com/leanprover/cslib/blob/automata/Cslib/Computability/Dfa/Basic.lean

If we go down this route I could (should?) probably move the lts results to a dedicated Dfa/Lts.lean file.

Hopping on the CSLib train as well. (I missed the launch as I was teaching a lot lately...)

Question: I foresee that I can mobilize some students to work on process algebra, which relies on Lts as a semantics as well. Do we consider this "the same" as automata theory, or should Lts be placed more general than automata theory? (Same remark for Petri Nets)

My instinct would be to consider "syntactic" and "semantic" definitions as different things and let them live in different directories.

[Chris Henson]

I still strongly disagree with this direction, but I appreciate that we have thoroughly discussed it at least. Thank you for your patience.

Regarding the points above:

I think the naming of the "co-inductive" version is not so crucial since as Fabrizio points out we won't be able to do much with it. I personally would wait until it's inevitably defined upstream, but it probably won't matter much either way.

Ching-Tsun Chou said:

But I do not like to write s[n]. Since we have made it clear that ωSequence α is but a (thin) abstraction of ℕ → α, we should take that POV seriously and be able to use the function application notation s i and not clutter the code with pointless [...].

Please correct me if I am wrong, but my understanding is that a type being a "thin wrapper" is antithetical to the design philosophy of Mathlib, whose conventions we have decided to adhere to as much as possible. This would sidestep the API defined by for instance docs#Stream'.get, making it useless to have in the first place. If you could show me where in Mathlib Stream' is used like this, I would be more inclined to accept this usage. I agree that GetElem is awkward for the reasons you state, I only offered the idea as a compromise that gave you close to the notation you want.

[Pieter Cuijpers]

Ching-Tsun Chou said:

Sorry for the late reply.

Yes, I think compatibility with mathlib should take precedence. Whether the transition part of an automaton is called step or Tr or next is of no real mathematical consequence. Personally I do not want to spend my time fighting it.

As to whether the transition part of an automaton should have the type State → Symbol → Set State or State → Symbol → State → Prop, I think both options are valid and both have long traditions, though I think the former has a longer tradition. Attached below is Rabin and Scott's seminal 1959 paper in which the notion of a nondeterministic automaton first appeared:
Rabin and Scott - Finite_Automata_and_Their_Decision_Problems.pdf
Take a look at Definition 9 on page 120, which uses the first option. As far as I can tell, most of the subsequent textbooks on automata theory also continued that tradition.

All the above is just a long way for me to say that there is nothing wrong with both options to exist in mathlib and I think it is even valuable to have definitions and theorems for going back and forth between them.

A personal rant: If Lean didn't have "sets" in the first place, we wouldn't need to discuss this topic at all. I once raised the topic of why does Lean have "sets" at all and was promptly shot down:

#new members > How do I prove this about Nat.nth? @ 💬

Just a comment from my experience, I've found State -> Symbol -> State -> Prop to be more convienient while generating structured operational semantics. One can simply mimick SOS-rules using something like:

inductive MySOS State -> Symbol -> State -> Prop where | concatenate_rule (x a y) (y b z) (_ : c = a + b) : MySOS x c z

With the State -> Symbol -> Set State based approach, this is more of a hassle, I think.

[Ching-Tsun Chou]

@Pieter Cuijpers I think @Fabrizio Montesi has made LTS sufficiently flexible for the same LTS to support both styles now.

[Ching-Tsun Chou]

PR for the initial version of ωSequence: cslib#90

[Ching-Tsun Chou]

@Chris Henson Will something like the following make you feel better? Is it possible to define another coercion to get rid of the invocations of ωSequence.mk below?

structure ωSequence α where
  seq : ℕ → α

attribute [coe] ωSequence.seq

namespace ωSequence

instance coeFun : CoeFun (ωSequence α) (fun _ ↦ ℕ → α) := {coe := (fun s ↦ s.seq)}

/-- Head of an ω-sequence: `ωSequence.head s = ωSequence s 0`. -/
abbrev head (s : ωSequence α) : α := s 0

/-- Tail of an ω-sequence: `ωSequence.tail (h :: t) = t`. -/
def tail (s : ωSequence α) : ωSequence α := ωSequence.mk (fun i => s (i + 1))

/-- Drop first `n` elements of an ω-sequence. -/
def drop (n : ℕ) (s : ωSequence α) : ωSequence α := ωSequence.mk (fun i => s (i + n))

/-- `take n s` returns a list of the `n` first elements of ω-sequence `s` -/
def take : ℕ → ωSequence α → List α
  | 0, _ => []
  | n + 1, s => List.cons (head s) (take n (tail s))

/-- Get the list containing the elements of `xs` from position `m` to `n - 1`. -/
def extract (xs : ωSequence α) (m n : ℕ) : List α :=
  take (n - m) (xs.drop m)

[Chris Henson]

Originally (in cslib#80) you also ported an equivalent of Stream'.get, which is meant to be the API used instead of directly accessing with function application. In the new PR it seems you have removed get completely, and instead definitions like Any, All, etc. that were originally defined using get are now directly using application.

In the context of the original PR, I would maybe have suggested:

import Mathlib

structure ωSequence α where
  seq : ℕ → α

attribute [coe] ωSequence.seq

def ωSequence.get (s : ωSequence α) (n : ℕ) : α := s.seq n

instance coeFun : CoeFun (ωSequence α) (fun _ ↦ ℕ → α) := {coe := ωSequence.get}

with the point being that the one field structure prevents directly applying, then the coercion is defined in terms of the API. (And if you really need to convert to a function, the generated equational lemmas are still there)

Without defining things in terms of get as you have done in this latest PR, I don't see a reason for the misdirection. As you have said, it is a "thin abstraction" that does not follow the Mathlib pattern of defining and using API.

[Ching-Tsun Chou]

I think my latest design is in the same spirit as (though much simpler than) Equiv:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Defs.html#Equiv
where if you have f : α ≃ β and a : α, you can (and indeed are advised to) write f a, instead of f.toFun a. Note that ωSequence.get = fun s ↦ s.seq is a theorem.

I think a good name for ωSequence.mkis ωSequence.ofFn, just like List.ofFn and Array.ofFn. The following definitions are already more than what I needed in automata theory. I think I'll get rid of most of the other API functions. For example, if we take seriously the POV that ωSequence α is just an abstraction of ℕ → α which also supports the dot-notation, then we don't need All s because we can just write ∀ n, s n.

structure ωSequence α where
  seq : ℕ → α

attribute [coe] ωSequence.seq

namespace ωSequence

instance coeFun : CoeFun (ωSequence α) (fun _ ↦ ℕ → α) := {coe := (fun s ↦ s.seq)}

def ofFn (s : ℕ → α) := ωSequence.mk s

/-- Head of an ω-sequence: `ωSequence.head s = ωSequence s 0`. -/
abbrev head (s : ωSequence α) : α := s 0

/-- Tail of an ω-sequence: `ωSequence.tail (h :: t) = t`. -/
def tail (s : ωSequence α) : ωSequence α := ofFn (fun i => s (i + 1))

/-- Drop first `n` elements of an ω-sequence. -/
def drop (n : ℕ) (s : ωSequence α) : ωSequence α := ofFn (fun i => s (i + n))

/-- `take n s` returns a list of the `n` first elements of ω-sequence `s` -/
def take : ℕ → ωSequence α → List α
  | 0, _ => []
  | n + 1, s => List.cons (head s) (take n (tail s))

/-- Get the list containing the elements of `xs` from position `m` to `n - 1`. -/
def extract (xs : ωSequence α) (m n : ℕ) : List α :=
  take (n - m) (xs.drop m)

/-- Prepend an element to an ω-sequence. -/
def cons (a : α) (s : ωSequence α) : ωSequence α := ofFn (fun n ↦
  match n with
  | 0 => a
  | n + 1 => s n )

@[inherit_doc] scoped infixr:67 " :: " => cons

/-- Append an ω-sequence to a list. -/
def appendωSequence : List α → ωSequence α → ωSequence α
  | [], s => s
  | List.cons a l, s => a::appendωSequence l s

@[inherit_doc] infixl:65 " ++ω " => appendωSequence

[Chris Henson]

Maybe I was unclear. I don't really see the point of the structure or CoeFun at all if you're dropping the get API.

And if you did have a structure, I would not define .ofFun when it is the same as the default .mk constructor.

[Ching-Tsun Chou]

I see. Then I won't use structure, but I will get rid of some of the APIs.

[Fabrizio Montesi]

I'll try to reply to your points in a single go, @Chris Henson and @Ching-Tsun Chou, hopefully in a coherent way:

• We should of course try to make cslib work well with mathlib, not duplicate code, etc. But this situation seems a bit special to me. What Stream' is supposed to be can't be defined, and this led to understandable compromises. Unfortunately, misusing it is way too easy. For example, I'd accessed it as a function in all my development of divergence in LTS (see https://github.com/leanprover/cslib/blob/e9cfac98021aefab859d7310482266f72e772180/Cslib/Foundations/Semantics/LTS/Basic.lean#L585), because I wasn't aware that the future of Stream' is to be become an actual data structure. I tried to define it so that the underlying function definition becomes unaccessible, without success.
• It seems that the literature on omega automata works with infinite sequences, not streams. These are not the same. The former is usually formalised as a function, either with Nat (our case here) or Int (for sequences that can be infinite in two directions) as domain. It is a coincidence that Stream' can be misused as an infinite sequence now. I really dislike the code duplication, too. So if there are ideas to avoid it by means of typeclasses or other clever usages of Lean features, I'm all ears.
• In mathlib itself, I see at least an example of people using a sequence instead of Stream': https://github.com/leanprover-community/mathlib4/blob/3540854faab731972101b97b709a67bf0fe8636f/Mathlib/Algebra/Polynomial/Sequence.lean#L39-L44.
• My formulation of ωSequence is a def, not a structure, exactly because it embraces being a function (not a wrapper). I was asking about potential uses exactly to ensure that it's ok not defining any getter methods. It should be a function, also by contract (that's why I documented it as such).
• Stream'.Seq is not what we want, either.

We're the ones with the immediate need to use workable infinite sequences (not streams/colists) to define a sizable part of automata theory, which is core to CS. Hence my proposal to just introduce a new type (ωSequence) that is intended to be used exactly as we need and can be implemented with current Lean features.

[Chris Henson]

I understand your intent for ωSequence to "embrace being a function". I think that in Mathlib the response would be to question having a def designed for defeq abuse rather than using a function type directly and having dot notation from the Function namespace as Mario pointed out. Of course, we are free to make our own decision and be a bit less rigid about this (and Mathlib does sometimes too!).

My position remains that despite the undesirability of using Stream' because of its future as coinductive data that it is preferable to the ~1000 lines of code duplication being proposed. My reasoning is if we are able to express everything we want through the long-standing API of Stream', I think that the usual deprecation cycle of Mathlib will ensure that all existing code has a path to migration. I would rather follow this lifecycle than redefine things ourselves.

I will reiterate again that I am fine to defer to your decision, and am satisfied that you have considered all our arguments. I will be happy either way to move on to PRs for the much more interesting work @Ching-Tsun Chou has done!

[Fabrizio Montesi]

I tried what Mario suggested in that thread and I couldn't put the dot-notation stuff for Function under a specialised namespace. The only way it worked was to put it directly under Function, instead of, say ωSequence.Function or something like that (opening ωSequence then didn't give me access to the defs through dot-notation). So I'm at a bit of a loss regarding how to keep this thing not leak to dependencies, unless we adopt a definition like this.

[Fabrizio Montesi]

(I forgot to mention I tried this, thanks for bringing it up.)

[Fabrizio Montesi]

(deleted)

[Chris Henson]

I see what you mean, but I don't have a problem with adding to existing namespaces like that. We do so already in other places. It doesn't really solve code duplication though, it just means it gets duplicated in the Function namespace instead.

[Fabrizio Montesi]

Normally I don't have a problem either, I guess here I'm just a bit extra wary because the future of this is likely that we'll add so much stuff to Function that is really domain-specific.

[Fabrizio Montesi]

The code duplication I don't know how to avoid, unfortunately, as soon as one wants to use a function as interface for sequences.. :-\

[Mario Carneiro]

Fabrizio Montesi said:

I tried what Mario suggested in that thread and I couldn't put the dot-notation stuff for Function under a specialised namespace. The only way it worked was to put it directly under Function, instead of, say ωSequence.Function or something like that (opening ωSequence then didn't give me access to the defs through dot-notation). So I'm at a bit of a loss regarding how to keep this thing not leak to dependencies, unless we adopt a definition like this.

cc: @Kyle Miller

[Mario Carneiro]

for my part the backup plan if dot notation doesn't work is to just not use dot notation, put everything in a namespace and open it so the functions don't get too long to write. I don't think it should be a deal breaker, lots of functions are written without dot notation

[Fabrizio Montesi]

An alternative I've toyed around with in my head looks like this:

class ωSequence (α : Type _) where
  at : ℕ → α

def drop (n : ℕ) (s : ωSequence α) : ωSequence α := { at i := s.at (i + n) }

-- etc. etc.

-- Could also include:

instance : GetElem (ωSequence α) ℕ α (fun _ _ => True) where
  getElem s i := fun _ => s.at i

This would hide it's a function, and future coinductive data structures could just instantiate it. I'm just not sure if the level of indirection would really be worth it, and whether I'm abusing the class mechanism here.

[Fabrizio Montesi]

Mario Carneiro said:

for my part the backup plan if dot notation doesn't work is to just not use dot notation, put everything in a namespace and open it so the functions don't get too long to write. I don't think it should be a deal breaker, lots of functions are written without dot notation

I guess in this solution we could, optionally, still have ωSequence as an abbrev?

[Mario Carneiro]

you could call the at field get since that's what it is

[Fabrizio Montesi]

Yes ofc

[Fabrizio Montesi]

(That's actually what it was but somebody was confused that it doesn't require a side-condition. Anyway, doesn't matter.)

[Ching-Tsun Chou]

Chris Henson said:

My position remains that despite the undesirability of using Stream' because of its future as coinductive data that it is preferable to the ~1000 lines of code duplication being proposed.

In the 2nd commit of cslib#90 I have whittled down the API functions and associated theorems down to ~600 lines (including comments). Note that:

1. Even the remaining API functions are way more than what I actually used in the omega automata theory, where I needed only const,drop, take, extract, and appendωSequence. I kept some iterators as they seem to be potentially useful even with an ℕ → α view of infinite sequences.
2. The API function extract is NOT in Stream' and about 80 lines of theorems are about extract. So the actual LOC we are carrying over from Stream' is about 500.

[Ching-Tsun Chou]

I've made this point before and I'll make it again: if we want to support reasoning about infinite sequences (which are used not only in automata theory but also in temporal logic and related topics), we should be willing to pay the cost of maintaining a data type which is truly an abstraction of ℕ → αand not designed for some other purpose.

[Ching-Tsun Chou]

Fabrizio Montesi said:

An alternative I've toyed around with in my head looks like this:
[ ... ]

I think this approach is similar to the experiment I gave in an earlier message of this thread:
https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Automata/near/543862424
As you can see, I really don't want to have to use get or getElem, which always seems unnecessarily bureaucratic to me when I think of infinite sequences as objects of type ℕ → α in my mind. So I coerce it away. I think the main drawback of this approach is that you probably need an explicit constructor function to convert a function of type ℕ → α to an infinite sequence of type ωSequence α. This is also too bureaucratic in my view, but more tolerable than to have to use get or getElem all over the place.

[Ching-Tsun Chou]

Fabrizio Montesi said:

Mario Carneiro said:

for my part the backup plan if dot notation doesn't work is to just not use dot notation, put everything in a namespace and open it so the functions don't get too long to write. I don't think it should be a deal breaker, lots of functions are written without dot notation

I guess in this solution we could, optionally, still have ωSequence as an abbrev?

I was using ℕ → α to represent infinite sequences in my automata theory project before I got fed up. As you can see here:
https://github.com/ctchou/AutomataTheory/blob/2c3ba16124d8bef9d5df5e7ba151ef6290705d67/AutomataTheory/Sequences/Basic.lean
https://github.com/ctchou/AutomataTheory/blob/2c3ba16124d8bef9d5df5e7ba151ef6290705d67/AutomataTheory/Sequences/Basic.lean
it's not pretty. I introduce a bunch of notations to emulate the dot-notation. But they don't look good and don't let me use the same naming convention as in List. (Note that the naming convention is not just about the API functions themselves, but also about the theorems they are involved in.) Using abbrev is not going to work, because abbrev does not change the names and namespaces of the relevant theorems. So the thin veneer provided by abbrev disappears immediately once you want to prove anything.

[Fabrizio Montesi]

Mmmh, I see. What about this then? https://github.com/leanprover/cslib/blob/omega-sequence/Cslib/Foundations/Data/OmegaSequence.lean

I've coded things as:

structure ωSequence (α : Type _) where
  get : ℕ → α

instance : FunLike (ωSequence α) ℕ α where [...]

instance : Coe (ℕ → α) (ωSequence α) where [...]

This enables both accessing the sequence with function notation and to create one just by giving a function. For example, this works:

def drop (n : ℕ) (s : ωSequence α) : ωSequence α := fun i => s (i + n)

This codifies the contract that ωSequence should be definable as a function, and be accessible as a function, while hiding away how it is implemented. We get easy coercions from both stream' and omegalist, if we want them:

instance : Coe (ωList α) (ωSequence α) where
  coe as := as.get

instance : Coe (Stream' α) (ωSequence α) where
  coe as := as.get

[Fabrizio Montesi]

This looks like the right way we wanna access a sequence tbh. Could somebody tell me if there's an advantage to doing this over just defining ωSequence to be a function?

[Chris Henson]

The FunLike instance being defined as get means that you can write application freely that unfolds to the API, right? So it is technically abstracted from its implementation as a function without having to think about it. This is the proposal I've been most comfortable with so far.

[Fabrizio Montesi]

Yes, that's the idea. When you use function application, it unfolds to an invocation of .get. Unless you're proving theorems about ωSequence, you're never gonna use or see that get. If you do, however, it'll show, and then it's the same as defining it directly as a function.
We could make the field private or protected (I'm not 100% sure about what they do) to restrict knowledge of this implementation detail to the file on omega sequence.

[Snir Broshi]

You can also provide an instance of GetElem to get array-like syntax (lst[n]):

instance : GetElem (ωList α) ℕ α fun _ _ ↦ True where
  getElem lst n _ := lst n

[Fabrizio Montesi]

Hey that reminds me of something :-) #CSLib > Automata @ 💬

[Fabrizio Montesi]

Ah, but you're proposing it for omega list! Yes, definitely!

[Mario Carneiro]

FYI, your definition of ωList is an empty type

[Fabrizio Montesi]

We know, it's in the docstring. (But comment appreciated all the same.)

[Mario Carneiro]

the docstring does not say this

[Mario Carneiro]

This file is just a stub. It is currently not possible to construct and manipulate nicely an
`ωList`, due to the current lack of support for coinduction in Lean.

this is not saying that ωList is empty, it implies that better support will make it easier to write elements of the type but they provably don't exist

[Mario Carneiro]

structure ωList (α : Type _) where
  head : α
  tail : ωList α

theorem nolist : ωList α → False
  | { tail, .. } => nolist tail

[Mario Carneiro]

If you are trying to write coinductive streams then please use Stream'

[Fabrizio Montesi]

That's what I meant by 'it's not possible to construct'. I'll add a more explicit statement, thx.

[Mario Carneiro]

I was expecting the difference between ωList and ωSequence to be that one is infinite lists and the other is possibly infinite lists

[Fabrizio Montesi]

OmegaList is what I expect Stream' to become one day: the data structure. We have the file just to collect desiderata/thoughts.

[Fabrizio Montesi]

So nothing important right now.

[Fabrizio Montesi]

OmegaSequence is an infinite sequence in one direction, as the name (I hope) implies.

[Mario Carneiro]

If you want the data structure I would instead suggest

structure ωList (α : Type _) where
  β : Type
  start : β
  next : β → α × β

[Mario Carneiro]

note that this has universe issues

[Fabrizio Montesi]

I tried variations of this and always had some problems so far.

[Fabrizio Montesi]

Won't Stream' switch to be a data structure, when it becomes possible to have a nice one?

[Mario Carneiro]

indeed

[Fabrizio Montesi]

I'd rather not try to do the same job. OmegaList shouldn't be really used.

[Mario Carneiro]

which is why I don't understand why you are reinventing it

[Fabrizio Montesi]

It's in that branch to explore the interplay between the data structure (that we can't really write yet) and OmegaSequence (which we're gonna use).

[Mario Carneiro]

in that case you should relate OmegaSequence and Stream'

[Mario Carneiro]

because these types are actually isomorphic without cheats

[Fabrizio Montesi]

Of course. That I would gladly even see go in the main branch, it wouldn't be a design thought experiment like this one. (Assuming that it only uses the API of stream', which can be done.)

[Fabrizio Montesi]

To be clear, OmegaList is the thought experiment, not omega sequence.

[Ching-Tsun Chou]

Regarding the FunLike implementation that @Fabrizio Montesi posted above, the top commit of the following branch:
https://github.com/ctchou/cslib/tree/omega-sequence-funlike
shows what changes it incurs in OmegaSequence, using the whittled down API I posted yesterday. The main drawback of the FunLike implementation is that it breaks the naive inductive definition of iterate. I had to relegate the inductive definition to a helper function iterate' and fix the proof of map_iterate. But nearly everything else works. If you know a better way to define iterare, please let me know.

Is everyone happy with this implementation? If so, we should settle on it and start using it to define and prove other stuffs. There is much to be done.

[Chris Henson]

This seems fine to me.

[Ching-Tsun Chou]

Great! Then please review cslib#90. In particular, I would appreciate feedbacks on which theorems should be labeled with @[simp] and @[grind] and the theorems about extract, which are new (relative to Stream').

[Chris Henson]

Ching-Tsun Chou said:

Great! Then please review cslib#90. In particular, I would appreciate feedbacks on which theorems should be labeled with @[simp] and @[grind] and the theorems about extract, which are new (relative to Stream').

Review left, with a focus on these aspects.

[Ching-Tsun Chou]

@Chris Henson's comments have been incorporated.

[Fabrizio Montesi]

LGTM now

[Snir Broshi]

Fabrizio Montesi said:

François G. Dorais said:

No: (X Y Z : Type _) assigns different universes for each variable.

Good to know, thanks!

I found a clue you might be interested in: #6499

"This has nice performance benefits."

[Ching-Tsun Chou]

Exactly what is the difference between Type _ and Type*? Why do they have different performance characteristics?

[Chris Henson]

Type _ is core Lean, while Type* is syntax provided by Mathlib. My guess at the performance difference is that the former triggers universe unification (I believe that's the correct terminology) it is less performant the Mathlib syntax which explicitly calls docs#Lean.Meta.mkFreshLevelMVar. Once we have benchmarking set up, I would welcome a PR that follows suit with Mathlib and eliminates Type _.

[Ching-Tsun Chou]

Ignoring performance for the moment, are the following semantically equivalent?

variable (X Y Z : Type _)
variable (X Y Z : Type*)

[Ching-Tsun Chou]

The following suggests that they are not:
image.png

[Chris Henson]

In your image they just have different level names, but that is the same. The difference is that in the former they are being unified, while in the latter they were explicitly created.

[Chris Henson]

Much earlier in the thread I made the mistake of thinking that Type _ could accidentally force the same universe levels, which was subsequently corrected. They both assign fresh universes, but the way in which they do so has performance implications. (Anyone please correct me if that is wrong)

[Ching-Tsun Chou]

My impression is that ?u.20 is a meta-variable while u_1 is an object-level variable for type level. Is that correct?

[Chris Henson]

If you want to be precise, look at the definition of Type*. It creates a fresh level mvar and converts it into a paramater, while for Type _ it is unassigned and left to unification. I just meant "same" in that they are both fresh because I wasn't clear by what you meant by "semantically".

[Ching-Tsun Chou]

I'm not sure what I mean "semantically", either. As far as I can understand it, the formal semantics of Lean in Mario Carneiro's thesis doesn't seem to deal with meta-variables and unification.

[Damiano Testa]

The main difference is that with Type _, Lean can try to solve and unify level parameters, if it is necessary. With Type*, you are guaranteed new "independent" universe levels.

[Damiano Testa]

Here is a simple example:

import Mathlib

variable (X Y : Type _) in
example : X = Y := sorry

variable (X Y : Type*) in
example : X = Y := sorry -- Type mismatch

[Fabrizio Montesi]

Thanks for the discussion. This is starting to be convincing evidence for me that we should use Type* instead of Type _.

[Ching-Tsun Chou]

I'm puzzled by @Damiano Testa 's second example. Consider the following code:

variable (X Y : Type*)
def foo (x : X) := x
def bar (y : Y) := y
example : foo = bar := rfl

How come Lean doesn't complain about the last proof goal?

[Chris Henson]

Your foo and bar are universe polymorphic, so the printing is misleading. It's bringing in a single universe used with equality. I think it is clearer if you give it a name and print everything:

import Mathlib

variable (X Y : Type*)
def foo (x : X) := x
def bar (y : Y) := y
theorem foo_bar_eq : foo = bar := rfl

/-- info: foo_bar_eq.{u_3} : @Eq.{u_3 + 2} ((X : Type u_3) → (x : X) → X) foo.{u_3} bar.{u_3} -/
#guard_msgs in
set_option pp.all true in
#check foo_bar_eq

[Ching-Tsun Chou]

That's the thing I don't understand: the type-level variable given to X and Y can denote the same level, as exemplified in the theorem far_bar_eq. So why does Lean reject the expression X = Y?

[Chris Henson]

Let me try explaining another way. In your example, you have a variable X and Y and individually refer to these in your universe polymorphic definitions of foo and bar, so they can be unified. In Damiano's example variable (X Y : Type*) together parameterizes the signature, so they must be separate levels and are not free to unify.

Maybe more clear if you see the equivalent without using variable:

import Mathlib

-- fails, X and Y are explicitly assigned different levels
example (X Y : Type*) : X = Y := sorry

-- each of `foo` and `bar` use a single level param to create a universe polymorphic definition
def foo (X : Type*) (x : X) := x
def bar (Y : Type*) (y : Y) := y

-- so this is fine, because we're able to set a fixed level `u` and compare `foo.{u}` and `bar.{u}`
example : foo = bar := rfl

universe u v

-- also works
example : foo.{u} = bar := rfl
example : foo = bar.{u} := rfl

-- fails
example : foo.{u} = bar.{v} := rfl

[Ching-Tsun Chou]

I'm not sure I'm entirely convinced. Lean does accept the following example:

variable (X Y : Type*)
example : (X → Y) = (Y → X) := by sorry

So it seems that unification will happen except when X and Y are given (so to speak) "nakedly".

[Chris Henson]

This is not unification, this works because for types X : Type u and Y : Type v, X → Y and Y → X both are in Type (max u v). Your example here is still universe polymorphic over two levels.

[Damiano Testa]

Note also #general > Every Type is finite ;-): the example there has since been "fixed", but the issue was that α was implicitly introduced as α : Sort _ and this then unified the universe to make it α : Prop and therefore it was retrieving the Finite.of_subsingleton instance on α.

[Damiano Testa]

The code there no longer works (gladly!), but it has worked at some point! :slight_smile:

[Ching-Tsun Chou]

I think I can fully endorse the sentiment expressed by Kevin Buzzard in that thread. :sweat_smile:

[Damiano Testa]

I think that, with some exceptions, you should always use Type*. If some part of the code does not work and the issue is having used Type*, then try switching to Type _.

[Damiano Testa]

Note also that the autoImplicit feature introduces Sort _, and that may create some subtle universe dependencies, even when it does not look like this is the case.

[Fabrizio Montesi]

Ok, so roughly Type* means 'a type in its own fresh universe variable' and Type _ means 'a type in whatever suitable universe'?

[Fabrizio Montesi]

FYI, #mathlib4 > Move automata theory in mathlib to CSLib?