É decidível se o comprimento de saída de um transdutor é limitado pelo comprimento de entrada?

Os transdutores considerados aqui são aqueles que a Wikipedia chama de transdutores de estado finito . O comportamento de um transdutor , isto é, a relação que ele calcula, é escrito : uma palavra é uma saída para iff . $T$ $[T]$ $y$ $x$ $x[T]y$

Pergunta: O seguinte problema é decidível:

Dado: Um transdutor e uma linguagem regular Decida: Mantém que , uma palavra, implica que? $T$ $L$
$\forall x \in L$ $\forall y$ $x[T]y$ $|y| \leq |x|$

Estou à procura de análises não triviais / subcasas solucionáveis, redução de problemas conhecidos e / ou referências relacionadas. (agora nem tenho certeza se é decidível em geral ...?)

Motivação: esse problema foi inspirado pela análise / investigação do teorema automatizado de comprovação de problemas da teoria dos números em geral e por um estudo altamente estudado, a conjectura de Collatz , em particular.

ds.algorithms reference-request automata-theory regular-language dfa vzn
fonte

Os transdutores FSM ps (deveriam ter sido mencionados, há muito conhecido) são poderosos o suficiente para calcular iterações únicas das "descrições instantâneas" da TM . portanto, o problema parece possivelmente se relacionar com LBAs e CSLS .

vzn

por

você fala do número de saídas na entrada

, certo? Não é o tamanho das saídas; nesse caso, seria bastante direto.

| F (x) |

$|F(x)|$

x

$x$

Michaël Cadilhac

são palavras e

é o comprimento da palavra "saída". tenho algumas idéias, mas não vejo nada direto no momento, portanto, a pergunta. seu devido presumivelmente não trivial por exemplo, para

entradas / saídas em algumas transições etc

x, F (x)

$x, F(x)$

| F (x) |

$|F(x)|$

ϵ

$\epsilon$

vzn

Portanto, você assume implicitamente que seu transdutor é funcional - em termos de notação, não ficou claro para mim :-) Então, o que se segue: Seja

um transdutor (possivelmente não determinístico) e

seja uma linguagem comum. Modifique

em um transdutor

para verificar se sua entrada está em

e todos os seus estados são alcançáveis e co-alcançáveis. Então

para todos

se não houver um ciclo simples no transdutor

T

$T$

L

$L$

T

$T$

T^{'}

$T'$

L

$L$

| T (w) | \leq | w |

$|T(w)| \leq |w|$

w \in L

$w \in L$

T^{'}

$T'$ para as quais a entrada é menor que a saída e algumas propriedades fáceis adicionais nas transições que não aparecem em nenhum SCC.

Michaël Cadilhac

Está bem. para "a entrada é menor que a saída", você quer dizer ao longo do ciclo? acho que vale a pena escrever isso como resposta. havia outra maneira diferente de formular este / problema relacionado com critérios mais rígidos que provavelmente não é (como) fácil, talvez tente novamente ("parte 2 / sequência / acompanhamento") se sua resposta parecer correta. esse problema atual é provavelmente quase um caso especial do problema mais amplo.

vzn

Respostas:

O outro colaborador excluiu sua resposta, talvez para me permitir estender meu comentário acima, então aqui está.

Seja um transdutor possivelmente não determinístico e seja uma linguagem comum. Modifique em um transdutor que verifique se sua entrada está em (alterando, por exemplo, o estado definido no produto cartesiano dos conjuntos de estados e e modificando a função de transição para que a parte dos estados é atualizado corretamente, mantendo o comportamento de ) $T$ $L$ $T$ $T'$ $L$ $T$ $L$ $L$ $T$

Um ramo de é uma sequência $T'$ de tal modo que é um caminho aceitar simples em , e cada um é um componente fortemente conectado de cujos estados incluem o destino de (e a origem de $\rho_1 C_1\rho_2 C_2 \cdots \rho_n C_n \rho_{n+1}$ $\rho_1\rho_2 \cdots \rho_{n+1}$ $T'$ $C_i$ $T'$ $\rho_i$ ) A filial émansase: $\rho_{i+1}$

O comprimento de entrada do caminho é maior do que ou igual ao seu comprimento de saída; $\rho_1\rho_2\cdots\rho_{n+1}$
Para qualquer , qualquer ciclo simples em , o comprimento de entrada do ciclo é maior ou igual ao seu comprimento de saída. $i$ $C_i$

Fato: Para qualquer , implica em se todos os ramos são mansos. $\big[$ $x, y$ $x[T']y$ $|y| \leq |x|$ $\big]$

A prova é bastante imediata. Sendo a última propriedade decidível (como o número de ramificações é limitado e o número de ciclos simples também), isso mostra que o problema da questão é decidível.

Michaël Cadilhac
fonte

Parece, pela descrição, que é até decidível em NL (daí em P), assumindo que

é dado por uma FSA.

L

$L$

Emil Jerabek

Enviei um aviso (desculpe, não li atentamente seu comentário antes de postar), mas provavelmente você não o recebeu após a exclusão da resposta :-) ... mas agora - como reembolso do tempo - você deve mudar para (e resolva!), este é mais complicado: " Problema em aberto : existe

e uma codificação computável

n \geq 1

$n \geq 1$

S_{n}

$S_n$ tal que, para todos os

?" :-D :-D

k \geq 1

$k \geq 1$

L_{\leq n}^{S_{n}} = L_{\leq n + k}^{S_{n}}

$L^{S_n}_{\leq n} = L^{S_n}_{\leq n+k}$

Marzio De Biasi

@ EmilJeřábek De fato, é bem claro em co-NL (daí em NL).

Michaël Cadilhac

@MarzioDeBiasi Thanks! Na verdade, eu não vi o seu aviso ☺ vou trabalhar para reembolsar seu tempo quando tiver algum ☺ #

Michaël Cadilhac