{"id":935,"date":"2016-01-11T13:22:49","date_gmt":"2016-01-11T12:22:49","guid":{"rendered":"http:\/\/www.mimuw.edu.pl\/~bojan\/?page_id=935"},"modified":"2016-02-19T14:08:16","modified_gmt":"2016-02-19T13:08:16","slug":"8-automata-with-infinite-alphabets","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20152016-2\/jezyki-automaty-i-obliczenia-2\/8-automata-with-infinite-alphabets","title":{"rendered":"8. Automata with infinite alphabets"},"content":{"rendered":"

Define a data word to be a word over an alphabet of the form \"\Sigma \times \atoms\", where \"\Sigma\" is a finite set, and \"\atoms\" is an infinite set. The first coordinate is called the label\u00a0<\/em>and the second coordinate is called the\u00a0data value.\u00a0<\/em>The idea is we will be able to test\u00a0labels explicitly by asking questions like “does the second\u00a0letter have \"a \in \Sigma\" as its label?” but we will only be allowed to test the data value for equality e.g. ask “do the third and fifth letters have the same data value?”<\/p>\n

By abuse of notation, we assume that a word over the alphabet \"\Atoms\" is also a data word, here there are no labels. Here are some examples of languages of data words, in all of these examples we \u00a0use no labels:<\/p>\n

    \n
  1. the first data value is the same as the last data value<\/li>\n
  2. some data value appears twice<\/li>\n
  3. no data value appears twice<\/li>\n
  4. the first data value appears again<\/li>\n
  5. consecutive data values are different<\/li>\n<\/ol>\n

    In this lecture, we introduce automata models for data words that capture the properties above. We begin with a\u00a0nondeterministic register automaton.\u00a0<\/em><\/p>\n

    Definition.\u00a0<\/strong>A\u00a0nondeterministic register automaton\u00a0<\/em>consists of:
    \n\u2022 a finite alphabet \"\Sigma\" for the labels;
    \n\u2022 a finite set \"Q\" control states;
    \n\u2022 a finite\u00a0set \"R\" of register names;
    \n\u2022 an initial state \"q_0 \in Q\" and a set of accepting \u00a0states \"F \subseteq Q\";
    \n\u2022 a transition relation<\/p>\n

      <\/span>   <\/span>\"\[\delta \subseteq \underbrace{Q \times (\atoms \cup \set \bot)^R}_{\text{configurations}} \times \underbrace{\Sigma \times \atoms}_{\text{input}} \times \underbrace{Q \times (\atoms \cup \set \bot)^R}_{\text{configurations}}\]\"<\/p>\n

    subject to the\u00a0equivariance\u00a0<\/em>condition described below.<\/p>\n

    The automaton is used to accept or reject data words where the alphabet is \"\Sigma \times \atoms\". After processing part of the input, the automaton keeps track of a configuration, <\/em>which consists of a control state and a register valuation (i.e. a partial function from register names to atoms).\u00a0Initially, the configuration consists of the initial state and a completely undefined register valuation. The configuration is then updated according to the transition relation \"\delta\", and the automaton accepts if at the end of the word the control state belongs to the accepting set.<\/p>\n

    The only issue is how to describe the transition relation. Since the space of configurations is infinite, the transition relation cannot be any relation. We choose the following restriction, called equivariance<\/em>: the transition relation can only compare data values with respect to equality. Equivariance\u00a0can be formalized\u00a0in two different ways below:<\/p>\n

      \n
    1. Semantic equivariance.\u00a0<\/b>Suppose that \"\pi\" is a bijection on the data values \"\atoms\". We can apply \"\pi\" to configurations in the natural way, and therefore also to triples in the transition relation \"\delta\". We say that \"\delta\" is semantically equivariant<\/em> if \u00a0\"\delta = \pi(\delta)\" holds for every bijection \"\pi\" of the atoms.<\/li>\n
    2. Syntactic equivariance.\u00a0<\/strong>We say that \"\delta\" is\u00a0syntactically\u00a0<\/em>equivariant\u00a0<\/em>if it can be defined by a finite Boolean combination of statements of the following types:
      \n\u2022 the control state in the source (respectively, target) configuration is \"q \in Q\";
      \n\u2022 the label in the input letter is \"a \in \Sigma\";
      \n\u2022 the data value is undefined in register \"r\" of the source configuration (respectively, target configuration);
      \n\u2022 the data value in the input letter equals the contents of register \"r\" in the source configuration (respectively, target configuration);
      \n\u2022 the data value in register \"r\" of the source configuration (respectively, target configuration) equals\u00a0the data value in register \"s\" of the source configuration (respectively, target configuration).<\/li>\n<\/ol>\n

      The advantage of semantic equivariance is that the definition is short. The advantage of syntactic equivariance is that it shows how the transition relation can be represented. The following straightforward lemma is given without proof.<\/p>\n

      Lemma.\u00a0<\/strong>Semantics and syntactic equivariance are the same.<\/p>\n

      This completes the definition of nondeterministic register automata: the transition relation is required to be equivariant in either of the two equivalent senses defined above. The transition relation is called deterministic\u00a0<\/i>if the source configuration and the input letter determine uniquely the target configuration.<\/p>\n

      Recall the five example languages. Deterministic register automata can 1,4,5. Nondeterministic\u00a0register\u00a0automata can do 1,2,4,5. In particular, deterministic register automata are strictly weaker than nondeterministic ones, and nondeterministic ones are not closed under complement.<\/p>\n

      Theorem.\u00a0<\/strong>Emptiness is decidable for nondeterministic register automata, but universality is not.<\/p>\n

      Proof.\u00a0<\/strong>When talking about decidability, we assume that the transition function is represented according to the syntactic equivariance condition.<\/p>\n

      Let us begin with the decidability argument. Define the\u00a0equality type\u00a0<\/em>of a configuration to be the following information: the control state, which registers are defined, and which registers store the same data value. It is not difficult to see that if a configuration of some equality type is reachable in the automaton, then all configurations of this equality type are also reachable. The algorithm for nonemptiness computes the equality types of reachable configurations. Intitially, we have the equality type of the unique initial configuration, which can be easily computed. If we have the equality type of some configuration, we can easily compute the equality types of all configurations reachable from it in one step; thus finishing the description of the algorithm.<\/p>\n

      Let us do the undecidability. We reduce from the halting problem. Suppose that we have a Turing machine which is an instance of the halting problem. We encode a run of a Turing machine as a data word according to the following following picture:<\/p>\n

      \"undecidability\"<\/a><\/p>\n

      Each letter encodes a single cell in a single configuration. The word represents a sequence of configurations, padded with blanks so that they all have the same length, and separated by a letter #. The labels are used to store the contents of the cell (light blue), plus the control state (dark blue) of the head if the head happens to be over that cell. Finally, each cell gets a unique identifier, a data value (red). We claim that there is a nondeterministic register automaton which accepts a data word if and only if it is\u00a0not an\u00a0<\/em>encoding of an accepting run of the Turing machine, and therefore solving universality for this automaton also solves\u00a0the halting problem. To prove the claim, we list the mistakes that can happen in a word that does not encode an accepting run of a Turing machine:<\/p>\n

      1. The data values identifying\u00a0the\u00a0cells are chosen wrong. This means that either:
      \n\u2022 the separator # is used with\u00a0more than one\u00a0data value; or
      \n\u2022 some data value \"d\" appears in two different places, with successor positions having data values \"e \neq e'\".
      \nThe first condition can be tested using one register, the second condition using two registers.<\/p>\n

      2. There is a mistake between two consecutive configurations. Assuming the identifiers are chosen correctly, this can be tested using only one register, to tell which cells correspond to which ones in the following configuration.<\/p>\n

      3. The first configuration is not initial, or the last configuration is not accepting. For this, no registers are needed.<\/p>\n

      \"\Box\"<\/p>\n

       <\/p>\n

       <\/p>\n

       <\/p>\n","protected":false},"excerpt":{"rendered":"

      Define a data word to be a word over an alphabet of the form , where is a finite set, and is an infinite set. The first coordinate is called the label\u00a0and the second coordinate is called the\u00a0data value.\u00a0The idea is we will be able to test\u00a0labels explicitly by asking questions like “does the second\u00a0letter […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":535,"menu_order":8,"comment_status":"open","ping_status":"open","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-935","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/935"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=935"}],"version-history":[{"count":20,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/935\/revisions"}],"predecessor-version":[{"id":1038,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/935\/revisions\/1038"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/535"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=935"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}