A Máquina-X (XM) é um modelo de computação teórico introduzido por Samuel Eilenberg em 1974.<ref name="Eil74">S. Eilenberg (1974) Automata, Languages and Machines, Vol. A. Academic Press, London.</ref> O X em Máquina-X representa o tipo de dados fundamental sobre o qual a máquina opera; por exemplo, a máquina que opera em databases (objetos do tipo database) seria chamada de database-machine. O modelo da Máquina-X é estruturalmente idêntico à máquina de estados finitos, exceto que os símbolos usados para marcar as transições da máquina denotam uma relação do tipo X->X. Realizar uma transição é equivalente a aplicar a relação que a rotulaa (computar um conjunto de mudanças ao tipo de dados X), e percorrer um caminho na máquina corresponde a aplicar todas as relações associadas, uma após a outra.
Teoria Original
A teoria original da Máquina-X proposta por Eilenberg era um modelo geral de computação completamente teórico (subsumindo a Máquina de Turing, por exemplo), o qual admitia computações determinísticas, não-determinísticas e não-terminantes. Sua obra seminal inclui muitas variantes do modelo básico da Máquina-X, cada um dos quais generalizava uma máquina de estados finitos de uma maneira ligeiramente diferente.
No modelo mais geral, uma Máquina-X é essencialmente uma "máquina para manipular objetos do tipo X". Suponha que X é algum tipo de dados, chamado tipo de dado fundamental, e que Φ é um conjunto de relações parciais φ: X → X. Uma Máquina-X é uma máquina de estados finitos com suas transições marcadas pelas relações em Φ. Em qualquer dado estado, uma ou mais transições podem ser liberadas se algum domínio da relação associada φi aceita (um sobconjunto dos) os valores atuais de X. Em cada ciclo, todas as transições ativadas são assumidas como utilizadas. Cada caminho reconhecido pela máquina gera uma lista φ1 ... φn de relações. Chamamos a composição φ1 o ... o φn dessas relações de caminho de relações correspondente ao caminho. O comportamento da Máquina-X é definido como a união de todos os comportamentos computados por seus caminhos de relações. De modo geral, isso é não-deterministico, uma vez que aplicar qualquer relação computa um conjunto de saídas em X. No modelo formal, todas as saídas possíveis são consideradas juntas, em paralelo.
Para fins práticos, uma Máquina-X deve descrever alguma computação finita. Uma função de codificação α: Y → X converte de alguma entrada do tipo Y para o estado inicial do tipo X, e uma função de decodificação β: X → Z converte de volta do estado final X para algum tipo de saída Z. Uma vez que o estado inicial de X é populado, a Máquina-X é executada até parar, e as saídas podem então ser observadas. De modo geral, a máquina pode entrar em deadlock (travar), livelock (nunca parar), ou executar uma ou mais computações completas. Por este motivo, pesquisas mais recentes focam em Máquinas-X determinísticas, as quais possuem um comportamento que pode ser controlado e observado mais precisamente.
Exemplo
Um compilador com um "olho-mágico" otimizador pode ser considerado como uma máquina para otimizar a estrutura de programas. Nesse Otimizador, a função de codificação α toma o código-fonte da entrada do tipo Y (a fonte do programa) e a carrega na memória de tipo X (árvore de análise sintática). Suponha que a máquina tenha diversos estados, chamados FindIncrements, FindSubExprs e Completed. A máquina começa no estado inicial FindIncrements, o qual é conectado aos outros estados pelas transições:
FindIncrements →DoIncrement FindIncrements FindIncrements →SkipIncrement FindSubExprs FindSubExprs →DoSubExpr FindSubExprs FindSubExprs →SkipSubExpr Completed
A relação DoIncrement mapeia a subárvore sintática correspondendo a "x := x + 1" na subárvore otimizada "++x". A relação DoSubExpr mapeia a árvore sintática contendo múltiplas ocorrencias da mesma expressão "x + y ... x + y" em uma versão otimizada com uma variável local para armazenar as repetidas computações "z := x + y; ... z ... z". Estas relações são ativadas somente se X contiver os valores de domínio (subárvores) nas quais elas operam. As relações remanescentes SkipIncrement e SkipSubExpr são nullops (relações identidade) ativadas em casos complementares.
Assim, a máquina Otimizadora vai rodar até completar, primeiro convertendo adições triviais em incrementos (durante o estado FindIncrements), a máquina vai então mover para o estado FindSubExpres e realizar uma séria de remoções de sub-expressões comuns, seguindo depois para o estado final Completed. A função de decodificação β vai então mapear do tipo de memória X (a árvore sintática otimizada) para o tipo de saída Z (código de máquina otimizado).
Convenção
Referindo-se ao modelo original de Eilenberg, "Máquina-X" é tipicamente escrita com um "m" minúsculo, pelo sentido de "qualquer máquina para processar X". Quando referindo-se a modelos específicos mais recentes, a convenção é de se usar o "M" maiúsculo como parte do nome próprio da variante.
Década de 1980 O interesse nas Máquinas-X foi revivido no fim dos anos 1980 por Mike Holcombe, <ref name="Hol88a">M. Holcombe (1988) 'X-machines as a basis for dynamic system specification', Software Engineering Journal 3(2), pp. 69-76.</ref> quando este percebeu que o modelo era ideal para especificação formal de software, pois ele claramente separa fluxo de controle de processamento. Em um nível de abstração suficientemente alto, o fluxo de controle de uma computação pode ser representado como uma máquina de estados finita, então, para completar a especificação da máquina-X, basta especificar o processamento associado com cada uma das transições da máquina. A simplicidade estrutural do modelo o faz extremamente flexível; outras ilustrações iniciais da ideia incluiam as especificações de interfaces homem-computador de Holcombe,<ref name="Hol88b">M. Holcombe (1988) 'Formal methods in the specification of the human-machine interface', International J. Command and Control, Communications and Info. Systems. 2, pp. 24-34.</ref> seu modelamento de processos em bioquímica celular, <ref name="Hol86">M. Holcombe (1986) 'Mathematical models of cell biochemistry'. Technical Report CS-86-4, Dept of Computer Science, Sheffield University.</ref> e o modelamento para tomadas de decisão em sistemas de comando militar de Stannett.<ref name="Sta87">M. Stannett (1987) 'An organisational approach to decision-making in command systems.' International J. Command and Control, Communications and Info. Systems. 1, pp. 23-34.</ref>
Década de 1990 Máquinas-X passaram a receber atenção renovada desde meados da década de 1990, quando a "Stream X-Machine" determinística de Gilbert LaycockGilbert Laycock (1993) The Theory and Practice of Specification Based Software Testing. PhD Thesis, University of Sheffield. Abstract serviu como base para especificação de grandes sistemas de software que são completamente testáveis.<ref name="HI98">M. Holcombe and F. Ipate (1998) Correct Systems - Building a Business Process Solution. Springer, Applied Computing Series.</ref> Outra variante, a "Communicating Stream X-Machine" oferece um modelo útil para testes de processos biológicosA. Bell and M. Holcombe (1996) 'Computational models of cellular processing', in Computation in Cellular and Molecular Biological Systems, eds. M. Holcombe, R. Paton and R. Cuthbertson, Singapore, World Scientific Press. e futuros sistemas de satélites swarm. <ref name="HRRT05"> M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005) 'Requirements of an Integrated Formal Method for Intelligent Swarms', in Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal. Association for Computing Machinery, pp. 125-133.</ref>
Década de 2000 Máquinas-X foram aplicadas a analisadores semânticos por Andras Kornai, que modelam o significado de palavras por máquinas "apontadoras", que possuem um membro do conjunto base X distinto.A. Kornai (2009) The Algebra of Lexical Semantics. Paper presented at the 2009 Meeting of the Assiciation for Mathematics of Language. In In C. Ebert, G. Jäger, J. Michaelis (eds) Proc. 11th Mathematics of Language workshop (MOL11) Springer LNCS 6149 174-199 Aplicações para outros ramos da linguística, em particular a reformulação contemporânea de Panini foram liderados por Gerar Huet e seus colegas de trabalho.G. Huet and B. Razet (2008) "Computing with Relational Machines" Tutorial presented at ICON, Dec 2008, Poona P. Goyal, G. Huet, A. Kulkarni, P. Scharf, R. Bunker (2012) "A Distributed Platform for Sanskrit Processing" In Proc. COLING 2012, pp 1011–1028
Principais variantes A Máquina-X raramente é encontrada em sua forma original, mas sustenta vários modelos subsequentes de computação. O mais influente modelo em teste de software foi a "Stream X-Machine". A NASA discutiu recentemente o uso de uma combinação de "Communicating Stream X-Machines" e o processo de cálculo WSCSS no design e teste de sistemas de de satélite swarm.
Analog X Machine (AXM) A mais antiga variante, a máquina de tempo contínuo Analog X-Machine (AXM) foi introduzida por Mike Stannet em 1990 como um potencial modelo de computação "super-Turing"; <ref name="Sta90">M. Stannett (1990) 'X-machines and the Halting Problem: Building a super-Turing machine'. Formal Aspects of Computing 2, pp. 331-41.</ref> ela é consequentemente relacionada a teoria da hipercomputação.<ref name="Cop02">B. J. Copeland (2002) 'Hypercomputation'. Minds and Machines 12', pp. 461-502.</ref>
Stream X-Machine (SXM) O modelo mais comumente encontrado de variante da Máquina-X é a "Stream X-Machine" feita por Gilbert Laycock em 1993, que forma a base da teoria do teste completo de software de Mike Holcombe e Florentin Ipate, que garante propriedades de correção conhecidas, uma vez que os testes tenham acabado.F. Ipate and M. Holcombe (1998) 'A method for refining and testing generalised machine specifications'. Int. J. Comp. Math. 68, pp. 197-219. A "Stream X-Machine" difere do modelo original de Eilenberg no que o tipo de dado fundamental X é da forma Out* x Mem x In*, onde In* é uma sequencia de entrada, Out* é uma sequência de saída, e Mem é a memória.
A vantagem deste modelo é que ele permite que o sistema seja dirigido, um passo por vez, através de seus estados e transições, enquanto observam-se as saídas de cada passo. Estes valores são testemunhas, que garantem que funções em particular tenham sido executadas em cada passo. Como resuldado, sistemas de software complexos podem ser decompostos em uma hierarquia de Stream-X Machines, projetadas de maneira "top-down" e testadas de maneira "bottom-up". Essa abordagem de dividir-e-conquistar para projetar e testar é apoiada pela prova da integração correta de Florentin Ipate,F. Ipate and M. Holcombe (1997) 'An integration testing method that is proved to find all faults', International Journal of Computer Mathematics 63, pp. 159-178. que prova que testar as máquinas em camada independentemente é equivalente a testar o sistema composto.
Communicating X-Machine (CXM)
A mais antiga proposta para conectar diversas Máquinas-X em paralelo é o modelo da "Communicating X-Machine" de Judith Barnard, 1995.<ref name="BTWM95">J. Barnard, C. Theaker, J. Whitworth and M. Woodward (1995) 'Real-time communicating X-machines for the formal design of real-time systems', in Proceedings of DARTS '95, Universite Libre, Brussels, Belgium, 9–11 November 2005</ref><ref name="Bar96">J. Barnard (1996) COMX: A methodology for the formal design of computer systems using Communicating X-machines. PhD Thesis, Staffordshire University.</ref> no qual máquinas são conectadas por canais de comunicação nomeados (conhecidos como portas); este modelo existe em ambas as variantes de tempo real e discretas.<ref name="AldBarn97">A. Alderson and J. Barnard (1997) 'On Making a Crossing Safe', Technical Report SOCTR/97/01, School of Computing, Staffordshire University. (Citeseer)