Rename DFA?

Stream: mathlib4

[Martin Dvořák]

I think that the name DFA is dangerous, as it stands for Deterministic Finite Automaton, while docs#DFA needn't be finite. I suggest StateMachine might be a better name. The downside is that we would have to rename NFA and εNFA as well. I think that NondetStateMachine and εNondetStateMachine might be acceptable names. Determinism is default (unless you use the initialism).

[Frédéric Dupuis]

Also, I think acronyms should be used sparingly in a project as big as mathlib.

[Shreyas Srinivas]

Martin Dvořák said:

I think that the name DFA is dangerous, as it stands for Deterministic Finite Automaton, while docs#DFA needn't be finite. I suggest StateMachine might be a better name. The downside is that we would have to rename NFA and εNFA as well. I think that NondetStateMachine and εNondetStateMachine might be acceptable names. Determinism is default (unless you use the initialism).

Good one. Just a small quibble. You want the names of the non-deterministic versions to have capitalised ds

[Martin Dvořák]

I find lowercase d slightly better.

[Eric Wieser]

I'd argue "DFA needn"t be finite" is not that different from "MonoidHom isn't actually between monoids", "Module doesn't actually imply a vector negation", and "RingEquiv isn't actually between rings"

[Eric Wieser]

We quite often name things based on the generality people are likely to look for rather than the actual generality we wrote them in

[Martin Dvořák]

/poll What do you prefer?
Keep DFA
Change it to StateMachine

[Shreyas Srinivas]

Eric Wieser said:

I'd argue "DFA needn"t be finite" is not that different from "MonoidHom isn't actually between monoids", "Module doesn't actually imply a vector negation", and "RingEquiv isn't actually between rings"

Except that would be misleading to an outsider peeking in. It would be reasonable for someone looking for DFAs to expect the finiteness assumption for the state set baked in somewhere. It would then be confusing to such a user as to why their textbook pumping lemma statement proof doesn't work (it uses pigeonhole principle).

[Eric Rodriguez]

but the solution is just to put Finite \sigma

[Martin Dvořák]

Eric Wieser said:

I'd argue "DFA needn"t be finite" is not that different from "MonoidHom isn't actually between monoids", "Module doesn't actually imply a vector negation", and "RingEquiv isn't actually between rings"

I don't think it is a fair comparison. Defining RingEquiv for (non-unital non-associative semi)rings is harmless — if you give me two rings and I give you a RingEquiv between them, it will indeed be a ring equivalence. In contrast, docs#DFA is a Trojan horse — if you give me a Language and I give you a DFA that accepts the language, it might mislead you into believing you have a regular language (if you don't read the full docs).

One possible improvement is to define Language.IsRegular in the style of Language.IsContextFree here
https://github.com/leanprover-community/mathlib4/blob/ffdb6fa3c42fc3f7bdaab2f3a071efcc34366b14/Mathlib/Computability/ContextFreeGrammar.lean#L195
where Language.IsRegular will restrict σ to be finite. Avoiding the use of the definition should raise a red flag "wait, why didn't the adversary prove regularity as the property defined on languages".

[Martin Dvořák]

Shreyas Srinivas said:

It would then be confusing to such a user as to why their textbook pumping lemma statement proof doesn't work (it uses pigeonhole principle).

You are definitely right, but please note that this isn't my main concern. I am not arguing on the basis "this definition is hard to work with because it is nonstandard". I am arguing on the basis "this definition is dangerous because it can facilitate academic misconduct"-

[Eric Wieser]

I think the resolution here is to document in the second line of the docstring that to actually enforce this is finite, you need Finite σ

[Martin Dvořák]

If it is written both in the module docstring (where it currently is) and in the structure docstring (where is currently isn't), it won't hurt, I guess.

[Shreyas Srinivas]

I don't see why names like SM and FSM cannot be used. These are common in the field. Then the acceptance conditions can be separated away and more types of automata can be included.

[Eric Wieser]

Because we would not have FSM at all, in the same way that we do not have GroupHom or MulOneHom at all

[Eric Wieser]

Martin Dvořák said:

If it is written both in the module docstring (where it currently is) and in the structure docstring (where is currently isn't), it won't hurt, I guess.

The duplication is unfortunate, but the structure docstring is the one that appears in vscode hovers

[Mario Carneiro]

and SM is even worse than DFA as far as acronym-naming is concerned

[Mario Carneiro]

Is this in a namespace?

[Eric Wieser]

docs#DFA: no, it is not

[Yury G. Kudryashov]

Why not use StateMachine?

[Yury G. Kudryashov]

Do we really try to save keystrokes over readability here?

[Mario Carneiro]

Personally I think StateMachine is a less good name than Deterministic(Finite)Automaton because the former is a blanket term used to refer to a variety of things that have state and the latter is a more specific implementation of the technique which has a common layout in the literature

[Mario Carneiro]

DFA is also much more commonly used as an acronym than FSM (I don't think I have ever seen SM used, nor DA)

[Yakov Pechersky]

Deterministic Pre-finite Automaton, the same way we have pre-connected and pre-prime.

[Martin Dvořák]

Predeterministic Finite Automaton

JOKE

[Bjørn Kjos-Hanssen]

To expand on Mario's comment, "finite-state machines can be subdivided into acceptors, classifiers, transducers and sequencers" (Wikipedia). Since we may also want to formalize transducers at some point, it seems bad to calls DFAs (which are acceptors) simply "state machines".

How about calling the deterministic potentially-infinite automaton "DeterministicAutomaton" with notation 𝓓𝓐 or 𝔻𝔸...