Are there non-constructive proofs of existence of "small" Turing machines / NFAs?

Question

After reading a related question, about non-constructive existence proofs of algorithms, I was wondering if there are methods of showing existence of "small" (say, state-wise) computation machines without actually building it.

Formally:

suppose we are given some language $L\subseteq \Sigma^*$ and fix some computation model (NFAs / turing machine/ etc.).

Are there any non-constructive existence results showing a $n$-state machine for $L$ exists, but without the ability of finding (in $poly(n,|\Sigma|)$ time) it?

For example, is there any regular language $L$ for which we can show $nsc(L)\leq n$ but we don't know how to build a $n$-state automaton for?

($nsc(L)$ is the non-deterministic state complexity of $L$, i.e. the number of states in the minimal NFA that accepts $L$).

---

EDIT: after some discussion with Marzio (thanks !) I think I can better formulate the question as follows:

Is there a language $L$ and a computation model for which the following holds:

1. We know how to build a machine that compute $L$ that has $m$ states.

2. We have a proof that $n$-states machine for $L$ exists (where $n << m$), but either we can't find it at all or it'd take exponential time to compute it.

Answer 1

Only an extended comment with a trivial example; you can pick the one-element language:

$$L_k = \{ M \mid \sigma(M) = \Sigma(k) \}$$

i.e. $L_k$ contains the first (in lexicographical order) busy beaver Turing machine of size $k$ (the Turing machine of size $k$ that attains the largest number of 1s on its tape after halting).

For every $k$ the language $L_k$ is regular ... but we have no idea on how to build the small DFA that recognizes it (though it has only $\leq 2*k(\log k+2)$ states) :-)

Answer 2

The language $ \mathtt{MOD_p} = \{a^{ip} \mid i \geq 0\} $ (for some prime number $p$) can be recognized by a $ O(\log p) $-state bounded-error quantum finite automata (QFAs) but the proof is non-constructive.

The best known constructively obtained number of states is $ O(\log^{2+o(1)}p) $ for bounded-error QFAs recognizing $ \mathtt{MOD_p} $.

REF: Section 4.2 of (Ambainis and Yakaryilmaz, 2015).

Answer 3

Another solution is to use Higman's lemma:

A language closed under subwords is regular.

With $u$ a subword of $v$ if we can obtain $u$ by removing some letter in $v$.

So take any language L, its subword closure is regular but is not at all constructible since L is arbitrary.