Jon Sterling on Nostr: It is kind of annoying in computer science courses when we talk about various ...
It is kind of annoying in computer science courses when we talk about various problems being (recursively) decidable. I am not complaining about constructive vs. classical approaches, because in such courses we are definitely classical and that is OK.
The thing I am complaining about is there is almost never any clarity as to whether when we say something like "acceptance in a DFA is decidable" whether we mean which of the following two distinct propositions:
1. The predicate that takes a DFA and a string and returns whether the former accepts the latter is decidable.
2. For a given DFA, the predicate that takes a string and returns whether the fixed DFA accepts the string is decidable.
In fact, (2) is obviously true and (1) is highly sensitive to what definitions we have given, and could be untrue in subtle ways. We do not even have the tools, at this level, to say what we mean by a "computable" function that takes an entire DFA as an argument—but I will just say that realisability is the simplest way to make sense of the question, and the following holds:
if every subset of a finite set is finite, then LEM holds.
Therefore, it follows that "well, check if the damn thing ends up in an accepting state" is not going to be a viable strategy for a *uniform* computational operation that checks DFAs against strings. This problem is avoided in case (2) above because we have a fixed DFA and we can easily "canonicalise" the (finite, by definition) set of states and (finite, by LEM) subset of accepting states before trying to compute anything.
The thing I am complaining about is there is almost never any clarity as to whether when we say something like "acceptance in a DFA is decidable" whether we mean which of the following two distinct propositions:
1. The predicate that takes a DFA and a string and returns whether the former accepts the latter is decidable.
2. For a given DFA, the predicate that takes a string and returns whether the fixed DFA accepts the string is decidable.
In fact, (2) is obviously true and (1) is highly sensitive to what definitions we have given, and could be untrue in subtle ways. We do not even have the tools, at this level, to say what we mean by a "computable" function that takes an entire DFA as an argument—but I will just say that realisability is the simplest way to make sense of the question, and the following holds:
if every subset of a finite set is finite, then LEM holds.
Therefore, it follows that "well, check if the damn thing ends up in an accepting state" is not going to be a viable strategy for a *uniform* computational operation that checks DFAs against strings. This problem is avoided in case (2) above because we have a fixed DFA and we can easily "canonicalise" the (finite, by definition) set of states and (finite, by LEM) subset of accepting states before trying to compute anything.