Dominique Larchey-Wendling

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Keywords: 2012 ACM Subject Classification Theory of computation → Models of computation, Theory of computation → Linear logic, Theory of computation → Type theory Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq Digital Object Identifier 10.4230/LIPIcs.FSCD.2021.18

We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative subexponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.

Introduction

In the late 80s, Lincoln et al. [17] gave a first proof of the undecidability of propositional linear logic (LL) via a many-one reduction from "and-branching two-counter machines without zero-test, " a variant of Minsky machines extended with a fork instruction. The ability of LL to simulate the increment and decrement operations characteristic of Petri net operations was spotted very early and lead to paradigmatically characterise LL as a logic for counting resources. Critically, the exponential modality ! can be exploited to allow unbounded reuse of some specific resources like (Petri net) transitions or (Minsky machines) instructions.

To establish undecidability, one needed of course to go beyond Petri nets because those have a decidable reachability problem, a major result from the early 80s with a very involved proof still actively revisited nowadays [18,[START_REF] Leroux | Demystifying Reachability in Vector Addition Systems[END_REF][START_REF] Czerwiński | The reachability problem for Petri nets is not elementary[END_REF][START_REF] Leroux | The Reachability Problem for Petri Nets is Not Primitive Recursive[END_REF][START_REF] Czerwiński | Reachability in Vector Addition Systems is Ackermann-complete[END_REF]. As opposed to Minsky machines, Petri nets are not able to perform zero tests combined with a jump. Hence, the main idea of the reduction was to use forking to separate comparison with zero from jumping. In there, the additive conjunction of LL plays a central role:

Σ ⊢ α = 0 Σ ⊢ jump Σ ⊢ α = 0 & jump
Indeed this right introduction rule duplicates the context Σ in the left and right sub-proofs which allows to delegate checking for emptiness in the left branch, and jumping in the right branch, the requirement of the two premises ensuring the correctness of the combination. The same idea was then exploited to establish the undecidability of smaller fragments of LL [START_REF] Kanovich | Linear Logic as a Logic of Computations[END_REF][START_REF] Kanovich | The direct simulation of Minsky machines in linear logic[END_REF][START_REF] Larchey | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF]. In our own work [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF], we gave the first mechanisation of the undecidability of the elementary fragment of LL in Coq, and hence ILL, based on this forking idea as well.

The multiplicative and exponential fragment (MELL) of linear logic lacks additive connectives, and is thus unable to duplicate the context. Arguably, the question of its decidability is the most important open conjecture (see e.g. [START_REF] Lazić | Non-Elementary Complexities for Branching VASS, MELL, and Extensions[END_REF]) in the context of LL, even with some claimed proof of decidability [START_REF] Bimbó | The decidability of the intensional fragment of classical linear logic[END_REF], later refuted [20]. The recent encoding of two counters Minsky machines in a fragment of LL lacking additives opened a new logical perspective on the MELL question [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF]. Indeed, at the cost of a more complex modal structure, forking with & can be replaced with a constraint on modalities in the promotion rule. This extension of MELL is called multiplicative sub-exponential linear logic (MSELL).

In this paper, we mechanise this reduction from two counters Minsky machines to MSELL, following the encoding of [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF]. However, we proceed in the intuitionistic version of the logic (two sided sequents with exactly one conclusion formula) that we call IMSELL. That fragment only involves the linear implication ⊸ and the modalities ! m with m ∈ Λ = {a, b, ∞}, so it is short to describe. It is also convenient for comparing with our previous encoding in (elementary) intuitionistic LL [START_REF] Larchey | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF][START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. Schematically, we describe and mechanise the following many-one reduction chain, explained below:

FRACTRAN reg ⪯ MMA0 2 ⪯ MM nd ⪯ IMSELL Λ
Our work is based on and contributes to the Coq library of undecidability proofs; see [START_REF] Forster | A Coq Library of Undecidable Problems[END_REF] for a quick overview. As opposed to the legacy LL argument of forking, which can cope with Minsky machines using arbitrary many counters, the MSELL and IMSELL reductions rely on two counters machines in an essential way. Hence, we first had to implement the undecidability of the "halting on the zero state" problem for two counters Minsky machines, that we denote MMA0 2 ; see Section 3. To establish this, we could follow the legacy reduction from many counters to just two by Minsky [19], that uses a Gödel coding of lists of natural numbers as essential trick. Following [START_REF] Larchey | Hilbert's Tenth Problem in Coq[END_REF], we profit from the FRACTRAN language [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF] that adequately abstracts away the Gödel coding phase, hence we establish the undecidability of MMA0 2 by reducing from (regular) FRACTRAN halting instead, mainly by mechanising Euclidean division with two counters only.

In Section 4, we provide a sequent calculus style presentation of MMA0 2 , i.e. the instance (M, x, y) of MMA0 2 is viewed as a sequent Σ M // n x ⊕ y ⊢ 1, and the Minsky machine M starting at PC value 1 with register values (x, y) halts on the zero state if and only if the sequent Σ M // n x ⊕ y ⊢ 1 has a derivation. We call this system and the associated problem non-deterministic two counters Minsky machines, denoted MM nd . As MM nd is essentially a specialised proof theory for Minsky machines, reducing from it to logical entailment problems mainly consists in transformations of derivations. Hence Section 5, targeting IMSELL, can be understood from a proof theoretic perspective only. In there, we gives details of the reduction of two counters halting, explaining how the legacy fork trick for ILL is replaced by the modal constraints in the promotion rule of IMSELL, following [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF]. Additionally, our proof of correctness of the reduction differs significantly: the former proof relies on the completeness of focused proof-search; we instead generalise our semantic argument [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF], i.e. we prove and use the soundness of trivial phase semantics for IMSELL.

Our contributions in this work are the following. First, via a proof theoretic presentation of Minsky machines, a comparison of their encoding in ILL and in IMSELL, explaining precisely how and where forking is replaced with modalities. Then, a novel completeness proof of the IMSELL reduction based on the soundness of trivial phase semantics. On the implementation side, we provide the mechanized proof of the undecidability of two counters Minsky machines (with two different presentations), and of IMSELL. The Coq 8.13 code is available at https://github.com/uds-psl/coq-library-undecidability/tree/FSCD-2021 and (sub-)section titles generally provide hyperlinks to the relevant source code. Our code extends the existing library with about 1800 loc, 1200 of which concern the reductions from FRACTRAN to MM nd , and 600 more for the MM nd to IMSELL reduction.

The paper describes the major steps of the implementation, in the language of type theory, but should be readable with only basic knowledge of it. We denote P (resp. B and N) the type of propositions (resp. Booleans and natural numbers). We write L X for the type of lists over X, where [ ] represents the empty list, x :: l for the cons operation, l + + l ′ for the concatenation of two lists, and |l| : N for the length of l. We write X n for vectors ⃗ v over type X with length n : N, and F n for the finite type with exactly n elements. Notations for lists are overloaded for vectors. Moreover, for p : F n and x : X, we write ⃗ v p for the p-th component of ⃗ v : X n and ⃗ v {x/p} when ⃗ v is updated with x at component p. The (non-dependent) sum A + B represents a computable/Boolean choice between an inhabitant of A or an inhabitant of B. In the case where A and B are propositions (i.e. of type P), the sum A + B : Type is stronger than the disjunction A ∨ B : P, because one cannot computably determine which of A or B holds in the later case. We also use the type-theoretic dependent sum Σ x:A B(x), denoted {x : A | B x} in Coq, 1 inhabited by (Coq computable) values x : A paired with a proof of B x.

The framework of synthetic computability [START_REF] Forster | On synthetic undecidability in Coq, with an application to the Entscheidungsproblem[END_REF] is based on the notion of many-one reduction. If P : X → P is a predicate (on X) and Q : Y → P is a predicate, we say that P many-one reduces to Q and write P ⪯ Q if there is a Coq function f : X → Y s.t. ∀x : X, P x ↔ Q(f x), i.e. a many-one reduction from P to Q. Because we work in constructive (axiom-free) Coq, all definable functions are computable and thus the requirement of the computability of the reduction function f above can be discarded. If P ⪯ Q and P is undecidable then so is Q.

2

The FRACTRAN seed (files FRACTRAN.v and fractran_utils.v)

The FRACTRAN model of computation is very simple to describe. It was introduced by Conway [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF] but its main idea, the Gödel coding of a list [x 1 ; x 2 ; . . . ;

x n ] of natural numbers as the number

p x1 1 p x2 2 • • • p xn n ,
predates the introduction of FRACTRAN by several decades. In the FRACTRAN formalism, programs are lists of formal fractions, i.e. terms Q of type L (N × N). 2 The state of a program is modelled as a natural number x : N. A fraction p/q is executable at state x if x•p/q is a natural number (i.e. not a proper fraction) and in that case this is the new state. To allow FRACTRAN to discriminate, and b.t.w. turn it into a Turing complete model of computation, the first executable fraction in the list has to be picked up at each step of computation. The program Q stops when no fraction in the list is executable.

1 or simply {x | B x} when the type of x is guessable. 2 For the moment, we can ignore the case of degenerate fractions like p/0. F S C D 2 0 2 1 18:4

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Formally this prose translates in a straightforward inductive definition, not even involving the algebraic notion of fraction, and characterized by the two inductive rules below:

qy = px p/q :: Q // F x ≻ y q ∤ px Q // F x ≻ y p/q :: Q // F x ≻ y
where u ∤ v means u does not divide v, and Q // F x ≻ y reads as the FRACTRAN program Q transforms state x into state y in one step of computation. The computation is terminated at x, denoted Q // F x ⊁ ⋆, when there is no possibility to perform one step from x, and termination from x, denoted by Q // F x ↓, means there is exists a sequence of steps starting at state x at leading to the terminated state y. Formally, this gives us:

Q // F x ⊁ ⋆ := ∀y, ¬(Q // F x ≻ y) and Q // F x ↓ := ∃y, (Q // F x ≻ * y ∧ Q // F y ⊁ ⋆)
There are some obvious quick remarks to make here: the empty program Q = [ ] is terminated in any state; unless Q = [ ], the state 0 is not terminated. The step relation is strongly decidable in the sense that one can discriminate between non-terminated and terminated states, and in the former case, computationally find a next state, expressed below using (Coq) dependent types:

▶ Proposition 1. For any FRACTRAN program we have ∀x, {y | Q // F x ≻ y}+(Q // F x ⊁ ⋆).
Proof. By structural induction on the list Q combined with Euclidean division. ◀

The dependent sum {y | Q // F x ≻ y} represents a (computable) state y together with a proof that y is next after x. The proposition Q // F x ⊁ ⋆ is for a proof that x is a terminated state. Finally, the outer sum + represents a computable choice between the two alternatives.

Non-regular fractions like 0/0 can make the computation non-deterministic; and nonproper fractions like 1/1 or 6/2 are always executable, implying that programs including such fractions have no terminating state. Non-deterministic step relations involves at least two different notions of termination, weak termination as defined above, and strong termination, when no infinite sequence of steps from x can exist. For our use of FRACTRAN, it does not matter because we only consider regular FRACTRAN programs where formal fractions p/0 are disallowed. Regular FRACTRAN is a universal model of computation, up to a Gödel encoding of natural numbers [START_REF] Conway | FRACTRAN: A Simple Universal Programming Language for Arithmetic[END_REF]. 3▶ Definition 2. A FRACTRAN reg instance is a pair composed of a list of regular formal fractions and a natural number, i.e. of type (Q, x) : L (N × N) × N | ∀p, p/0 ̸ ∈ Q , and the question asked is whether Q // F x ↓ holds or not.

Notice the use of a dependent sum in the type of instances where the predicate ∀p, p/0 ̸ ∈ Q acts as a guard against non-regular instances.

▶ Theorem 3 (mechanized in [START_REF] Larchey | Hilbert's Tenth Problem in Coq[END_REF]). There is a many-one reduction from the Halting problem for single tape Turing machines to termination of regular FRACTRAN programs, i.e. Halt ⪯ FRACTRAN reg , and thus FRACTRAN reg is undecidable.

As a consequence, we can safely use FRACTRAN reg as our seed of undecidability for the chain of many-one reductions described in this paper.

3

From FRACTRAN to two registers alternate Minsky machines

Alternate Minsky machines (files MM.v and mma_defs.v)

We describe alternate n counters (or registers) Minsky machines, where states are described as (i, ⃗ v) : N × N n . The number i : N is the current program counter (PC) value and the vector ⃗ v : N n describes the n current values of the registers. When convenient, we also denote states as st , st 1 ... Instructions consist of either incrementing INC a x a register by one, or decrementing DEC a x j a register by one. Notice that when the register values 0, it is not possible to decrement it. So a conditional jump at j helps at discriminating between the zero and non-zero cases. Unless there is a conditional jump, the default behaviour after the register is updated is to jump to the next instruction at PC + 1. In contrast with [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF][START_REF] Larchey | Hilbert's Tenth Problem in Coq[END_REF] where the DEC x j instruction jumps at j when ⃗ v x is empty, here in DEC a x j, the jump occurs when decrementing is possible, and this is the reason we call these machines alternate and suffix instructions with an "a" just as a reminder for this alternate semantics. Hence a single (atomic) step of computation is described by the following relation

INC a x // a (i, ⃗ v) ≻ 1+i, ⃗ v{(1+u)/x} when ⃗ v x = u DEC a x j // a (i, ⃗ v) ≻ j, ⃗ v{u/x} when ⃗ v x = 1+u DEC a x j // a (i, ⃗ v) ≻ (1+i, ⃗ v) when ⃗ v x = 0
where σ // a (i 1 , ⃗ v 1 ) ≻ (i 2 , ⃗ v 2 ) reads as the MMA n instruction σ at PC value i 1 transforms the state (i 1 , ⃗ v 1 ) into the state (i 2 , ⃗ v 2 ). Notice that this alternate semantics allows to implement a universal jump without needing an empty register, which will be critical when we will need to limit the number of registers to n = 2. This means that starting from state (i 1 , ⃗ v 1 ), the instruction σ at PC value i 1 (provided there is one) changes the state in exactly one possible way, and the new state (i 2 , ⃗ v 2 ) is Coq-computable from the initial state (i 1 , ⃗ v 1 ). So the only way for such programs to terminate is to jump to a PC value which holds no instruction.

▶
A program is pair (i, P ) : N × L MMA n composed of the PC value of its first instruction and the sequence P of consecutive instructions of which is it composed. Informally, the program (i, [σ 0 ; . . . ; σ m-1 ]) would be read as e.g. i : σ 0 ; 1+i : σ 1 ; . . . ; m-1+i : σ m-1 using labelled instructions. We define the k-steps relation for a program (i, P ) inductively with

(i, P ) // a st ≻ 0 st i1 = |L| + i P = L + + σ :: R σ // a (i1, ⃗ v1) ≻ st2 (i, P ) // a st2 ≻ k st3 (i, P ) // a (i1, ⃗ v1) ≻ 1+k st3
where the constraints i 1 = |L| + i and P = L + + σ :: R impose that the instruction at PC value i 1 of (i, P ) is σ. From its structure as lists of instructions, there is at most one instruction at a given PC value and thus, the k-steps relation is also deterministic. However, it can be non-total if a jump outside of the interval [i, |P | -1 + i] occurs, the lack of an instruction blocking the computation. We write out j (i, P ) := j < i ∨ |P | + i ≤ j when there is no instruction at j in (i, P ), and because of Proposition 4 (totality), blocked states are exactly those outside of the code, i.e. out i 1 (i,

P ) ↔ ∀st 2 , ¬ (i, P ) // a (i 1 , ⃗ v 1 ) ≻ 1 st 2 .

F S C D 2 0 2 1 18:6 Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

We define the predicates of computation, of progress, of output and of termination as:

(i, P ) // a st 1 ≻ * st 2 := ∃k, (i, P ) // a st 1 ≻ k st 2 (computation) (i, P ) // a st 1 ≻ + st 2 := ∃k > 0, (i, P ) // a st 1 ≻ k st 2 (progress) (i, P ) // a st 1 ⇝ (i 2 , ⃗ v 2 ) := (i, P ) // a st 1 ≻ * (i 2 , ⃗ v 2 ) ∧ out i 2 (i, P ) (output) (i, P ) // a st 1 ↓ := ∃st 2 , (i, P ) // a st 1 ⇝ st 2 (termination)
output meaning that we have computed until we reach a state blocking the computation.

▶
) // a (1, ⃗ v) ⇝ (0, [0; 0]).
We mention that there is substantial machinery for (alternate) Minsky machines, and more generally PC based state machines, in the Coq library of undecidable problem initially described in [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. These tools enable modular reasoning in those models of computation.

A basic MMA n library up to Euclidean division (file mma_utils.v)

We specify, implement and verify a small library to compute some basic operations with MMA n . For this section, n : N is a fixed number of registers but all the below sub-programs involve at most two registers. In the coming statements, the vector ⃗ v : N n is implicitly universally quantified over. The names i, j, p, q : N range over PC values, k : N over natural number constants, and the names x, t, s, d : F n over registers indices.

Let us start with the easy simulations of an unconditional jump, the nullification of register x and the operation that adds k units to register x. ▶ Proposition 6. For i, j : N and x :

F n we have (i, JUMP a j x) // a (i, ⃗ v) ≻ + (j, ⃗ v) where JUMP a j x := [INC a x; DEC a x j]. ▶ Proposition 7. For x : F n and i : N, we have (i, NULL a x i) // a (i, ⃗ v) ≻ + (1 + i, ⃗ v{0/x}) where NULL a x i := [DEC a x i]. ▶ Proposition 8. For i, k : N, x : F n , we have (i, INCS a x k) // a (i, ⃗ v) ≻ * (k + i, ⃗ v{(k + ⃗ v x )/x}) where INCS a x k := [INC a x; . . . ; INC a x] is of length |INCS a x k| = k.
Then we simulate test for emptiness of register x, jumping to PC value p when x is empty, or else to the end of the sub-program otherwise. Registers are restored to their initial values when the sub-program is finished (assuming p points outside of its code).

▶ Proposition 9. For x : F n and p, i :

N we have (i, EMPTY a x p i) // a (i, ⃗ v) ≻ + (j, ⃗ v) where EMPTY a x p i := [DEC a x (3 + i); JUMP a p x; INC a x], and j := p in case ⃗ v x = 0, or else j := 4 + i in case ⃗ v x ̸ = 0.
Notice that this sub-program is of length |EMPTY a x p i| = 4 (despite looking 3), because we abuse the list notation [. . . ; . . . ; . . .] by allowing dots to be not only single instructions but also lists of instructions such as JUMP a p x. Hence, EMPTY a x p i is formally defined as DEC a x (3 + i) :: JUMP a p x + + INC a x :: [ ] but we choose the friendly display for readability.

We now simulate the transfer of the contents of register s (for source) to d (for destination).

▶ Proposition 10. For s ̸ = d : F n and i : N we have (i, TRANSFER a s d i) // a (i, ⃗ v) ≻ + (3 + i, ⃗ w) where TRANSFER a s d i := [INC a d; DEC a s i; DEC a d (3 + i)] and ⃗ w := ⃗ v{0/s}{(⃗ v s + ⃗ v d )/d}.
We simulate multiplication of a register by a constant. The idea is similar to transfer but instead of transferring one for one, when one unit is removed from s, k units are added to d.

▶ Proposition 11. For s ̸ = d : F n , k, i : N we have (i, MULT_CST a s d k i) // a (i, ⃗ v) ≻ + (j, ⃗ w) where MULT_CST a s d k i := [DEC a s (3 + i); JUMP a (5 + k + i) s; INCS a d k; JUMP a i s], j := 5 + k + i, ⃗ w := ⃗ v{0/s}{(k⃗ v s + ⃗ v d )/d}, and |MULT_CST a s d k i| = 5 + k.
We simulate the minus k operation (with overflow management), jumping to PC value p when k units can be removed from register x, or else to PC value q when register x contains less than k units (overflow).

▶ Proposition 12. For p, q, k, i : N and x : F n , we define

DECS a x p q k i := [DEC a x (3 + i); JUMP a q x; . . . ; DEC a x (3k + i); JUMP a q x; JUMP a p x]
where the pattern DEC a x (3u + i); JUMP a q x is repeated for u = 1, . . . , k.

Depending on the comparison between ⃗ v x and k, we have the following:

if ⃗ v x < k then (i, DECS a x p q k i) // a (i, ⃗ v) ≻ + (q, ⃗ v{0/x}); if ⃗ v x ≥ k then (i, DECS a x p q k i) // a (i, ⃗ v) ≻ + (p, ⃗ v{⃗ v x -k/x}).
Using an extra temporary register t, we implement a non-destructive minus k operation (with overflow management).

▶ Proposition 13. For x ̸ = t : F n and p, q, k, i : N, we define

DECS_COPY a x t p q k i :=    DECa x (4 -1 + i); JUMPa q x; INCa t; . . . DECa x (4k -1 + i); JUMPa q x; INCa t; JUMPa p x   
where the pattern DEC a x (4u -1 + i); JUMP a q x; INC a t is repeated for u = 1, . . . , k.

Depending on the comparison between ⃗ v x and k, we have the following:

if ⃗ v x < k then (i, DECS_COPY a x t p q k i) // a (i, ⃗ v) ≻ + (q, ⃗ v{0/x}{(⃗ v x + ⃗ v t )/t}); if ⃗ v x ≥ k then (i, DECS_COPY a x t p q k i) // a (i, ⃗ v) ≻ + (p, ⃗ v{(⃗ v x -k)/x}{(k + ⃗ v t )/t}). The length is |DECS_COPY a x t p q k i| = 2 + 4k.
Notice that the initial value of t has to be known if one wants to recover the initial value of x, e.g. if the initial value of t is 0 and x contains less than k units, then once the computation is finished, t contains a copy of the initial value of x.

We implement a non-destructive computation of a divisibility test of register x by a constant k > 0, using a spare register t to preserve the initial value of x. ▶ Proposition 14. For x, t : F n and p, q, k, i : N, we define

MOD_CST a x t p q k i := [EMPTY a x p i; DECS_COPY a x t i q k (4 + i)]
and we check the identity |MOD_CST a x t p q k i| = 6 + 4k. Assuming x ̸ = t and k > 0, we have (i, MOD_CST a x t p q k i) // a (i, ⃗ v) ≻ + (j, ⃗ v{0/s}{(⃗ v x + ⃗ v t )/t}) where j := p when k divides ⃗ v x , and j := q otherwise. We now implement division by a constant k > 0. It will only work when the contents of the input register s is a multiple of k and the quotient is then stored in d.

▶ Proposition 15. For s, d : F n and k, i : N, we define

DIV_CST a s d k i := [DECS a s (2 + 3k + i) (5 + 3k + i) k i; INC a d; JUMP a i s]
and we check the identity

|DIV_CST a s d k i| = 5 + 3k. Assuming s ̸ = d, k > 0 and ⃗ v s = ak, we have (i, DIV_CST a s d k i) // a (i, ⃗ v) ≻ + (5 + 3k + i, ⃗ v{0/s}{(a + ⃗ v d )/d}). F S C D 2 0 2 1

Compiling regular FRACTRAN programs (file fractran_mma.v)

We are now in position to compile regular FRACTRAN programs (with no p/0 fractions). We start with a sub-program for simulating the FRACTRAN step relation for one regular fraction p/q then we will chain those sub-programs.

We fix n := 2, and s := 0 : F 2 and d := 1 : F 2 are the two available registers for two counters alternate Minsky machines. Let use assume a regular fraction, i.e. p, q : N with q ̸ = 0, and i, j : N where i the starting PC value of the sub-program.

To help the readability of the following code, we decorate it with relevant labels (PC values), although those are not formally present in the mechanisation:

(i, FRAC_ONE a p q i j) :=            i0: MULT_CST a s d p i0; i1: MOD_CST a d s i2 i5 q i1; i2: DIV_CST a s d q i2; i3: TRANSFERa d s i3; i4: JUMPa j d; i5: DIV_CST a s d p i5; i6: TRANSFERa d s i6 i7:            where                      i0 := i, i1 := 5 + p + i0, i2 := 6 + 4q + i1, i3 := 5 + 3q + i2, i4 := 3 + i3, i5 := 2 + i4, i6 := 5 + 3p + i5, i7 := 3 + i6 ▶ Proposition 16. |FRAC_ONE a p q i j| = 29 + 4p + 7q and i 7 = |FRAC_ONE a p q i j| + i. ▶ Proposition 17. If qy = px then (i, FRAC_ONE a p q i j) // a (i, [x; 0]) ≻ + (j, [y; 0]). ▶ Proposition 18. If q ∤ px then (i, FRAC_ONE a p q i j) // a (i, [x; 0]) ≻ + (i 7 , [x; 0]).
Proof. The proof of Proposition 17 (resp. 18) is sketched in Appendix A (resp. B). ◀ Hence (i, FRAC_ONE a p q i j) performs the multiplication of x by p/q if the result is a natural number, transferring the control to PC value j, or else, would the result be a proper fraction, the registers are globally unmodified and the PC is transferred at i 7 , the end of this sub-program. Notice that the register d is assumed to be initially empty.

We now chain those sub-programs to simulate one step of a regular FRACTRAN program, encoding a list Q of fractions by structural recursion on Q:

FRAC_STEP a j [ ] i := [ ] FRAC_STEP a j (p/q :: Q) i := P + + FRAC_STEP a j Q (|P | + i)
where P := FRAC_ONE a p q i j ▶ Lemma 19. For any regular FRACTRAN program Q : L (N × N) and any i, j, x, y :

N, if Q // F x ≻ y then (i, FRAC_STEP a j Q i) // a (i, [x; 0]) ≻ + (j, [y; 0]).
Proof. By induction on the predicate Q // F x ≻ y using Propositions 17 and 18. ◀ ▶ Lemma 20. For any regular FRACTRAN program Q : L (N × N) and any i, j, x :

N, if Q // F x ⊁ ⋆ then (i, FRAC_STEP a j Q i) // a (i, [x; 0]) ≻ * (|FRAC_STEP a j Q i| + i, [x; 0]).
Proof. By induction on Q using Proposition 18. ◀

The instance FRAC_STEP a 1 Q 1 starts at i = 1 and loops on itself (j = 1) until no fraction can be executed. In addition, we finish by nullifying s and then jump to PC value 0:

FRAC_MMA a Q := FRAC_STEP a 1 Q 1 + + NULL a s |FRAC_STEP a 1 Q 1| + 1 + + JUMP a 0 s Σ // n 0 ⊕ 0 ⊢ p STOPn p ∈ Σ Σ // n 1+a ⊕ b ⊢ q Σ // n a ⊕ b ⊢ p INCn α p q ∈ Σ Σ // n a ⊕ b ⊢ q Σ // n 1+a ⊕ b ⊢ p DECn α p q ∈ Σ Σ // n 0 ⊕ b ⊢ q Σ // n 0 ⊕ b ⊢ p ZEROn α p q ∈ Σ Σ // n a ⊕ 1+b ⊢ q Σ // n a ⊕ b ⊢ p INCn β p q ∈ Σ Σ // n a ⊕ b ⊢ q Σ // n a ⊕ 1+b ⊢ p DECn β p q ∈ Σ Σ // n a ⊕ 0 ⊢ q Σ // n a ⊕ 0 ⊢ p ZEROn β p q ∈ Σ Figure 1
The S-MM nd sequent style calculus for non-deterministic two counters Minsky machines.

▶ Theorem 21. For any regular FRACTRAN program Q : L (N × N) and any x : N, the three following properties are equivalent:

1. Q // F x ↓; 2. (1, FRAC_MMA a Q) // a (1, [x; 0]) ⇝ (0, [0; 0]); 3. (1, FRAC_MMA a Q) // a (

Minsky machine termination as provability

While the (heavy) alternate Minsky machines framework was useful to simulate FRACTRAN programs with two counter machines, using it as a seed for other reductions is not recommended. First, explaining the semantics and termination predicates requires many definitions, not necessarily obvious at first. Also, manipulating them without the tools for modular reasoning is quite difficult.

Non-deterministic two counters Minsky machines (file ndMM2.v)

For our reductions to linear logic, we replace MMA 2 with an equivalent model, much easier to describe and work with, where computations are performed by proof-search and termination matches the provability/derivability predicate. Reductions to entailment in logical systems will thus mainly consist in encoding derivations from one system to another. We call this model non-deterministic two counters Minsky machines and denote MM nd . We comment this logical presentation, sequent style, of Minsky machines. MM nd instructions are of the form STOP n p | INC n x p q | DEC n x p q | ZERO n x p q where x ∈ {α, β} is a register index, either the first α or the second β, 4 and p, q : N are labels, here in type N, but the definitions in this section are completely parametric in the type of labels. A sequent of MM nd is of the form Σ // n a ⊕ b ⊢ p where Σ is a list of MM nd instructions viewed as a finite set, a and b of type N represent the values of the counters α and β respectively and p is the current label.

We define provability/derivability inductively by the rules the calculus S-MM nd in Fig. 1. Notice that since computation is simulated by proof-search, the initial state is the conclusion of a rule and it is transformed into the premise, when there is one. For example, the INC n _ p q rule contains both the initial label and the jump-to label, hence it can only execute at label p. However, nothing prevents the simultaneous occurrence of another instruction INC n _ p q ′ in Σ, and this could render proof-search non-deterministic, hence our choice of terminology. However, non-determinism is not relevant to the undecidability of the MM nd .

Notice that it is common practice to represent the sequent and the derivability predicate of the sequent by the same denotation Σ // n a ⊕ b ⊢ p which could lead to confusion. Usually, we qualify the notation with the "sequent" word to make it explicit. Unqualified or followed with "is derivable" means that the notation represents the S-MM nd derivability predicate.

▶ Definition 23. A MM nd problem instance is the data of a sequent Σ // n a ⊕ b ⊢ p, and the question is whether this sequent is derivable or not using the rules of S-MM nd (Fig. 1).

Notice that ZERO n x p q performs both a zero-test on x and if zero, a jump from p to q without changing registers. If we remove the ZERO n _ p q rules, we get Petri nets reachability, more specifically VASS with states, which have a decidable reachability problem with non-elementary complexity [START_REF] Czerwiński | The reachability problem for Petri nets is not elementary[END_REF], even non-primitive recursive according to [START_REF] Leroux | The Reachability Problem for Petri Nets is Not Primitive Recursive[END_REF][START_REF] Czerwiński | Reachability in Vector Addition Systems is Ackermann-complete[END_REF].

From MMA0 2 to MM nd (file MMA2_to_ndMM2_ACCEPT.v)

We give an alternate presentation of termination on zero for two registers Minsky machines, using the S-MM nd calculus of Section 4.1. Let us consider alternate Minsky machines MMA 2 with two counters, s := 0 : F 2 and d := 1 : F 2 . We denote by α, β : B the two registers of MM nd instructions. We define the following encodings of single instructions and programs:

(•) : F2 → B ⟨•, •⟩ : N → MMA2 → L MM nd ⟨⟨•, •⟩⟩ : N → L MMA2 → L MM nd 0 := α ⟨i, INCa x⟩ := [INCn x i (1+i)] ⟨⟨i, [ ]⟩⟩ := [ ] 1 := β ⟨i,
′ ]) and Σ // n a ′ ⊕ b ′ ⊢ j is derivable then so is Σ // n a ⊕ b ⊢ i; 2. assuming ⟨⟨1, P ⟩⟩ ⊆ Σ, if (1, P ) // a (i, [a; b]) ≻ 1 (j, [a ′ ; b ′ ]) and Σ // n a ′ ⊕ b ′ ⊢ j is derivable then so is Σ // n a ⊕ b ⊢ i.
Proof. Item 1 is by case analysis on σ and item 2 follows from item 1. ◀

Let us now define Σ P := STOP n 0 :: ⟨⟨1, P ⟩⟩ which constitutes the encoding of MMA 2 programs into MM nd sequents. We establish its soundness.

▶ Lemma 25. If (1, P ) // a (i, [a, b]) ≻ * (0, [0; 0]) then Σ P // n a ⊕ b ⊢ i is derivable.
Proof. We have ⟨⟨1, P ⟩⟩ ⊆ Σ P by definition of Σ P . Iterating Proposition 24 (item 2), we thus get Σ P // n 0 ⊕ 0 ⊢ 0 → Σ P // n a ⊕ b ⊢ i. The derivability of Σ P // n 0 ⊕ 0 ⊢ 0 follows from STOP n 0 ∈ Σ P and the STOP n 0 rule of S-MM nd . ◀ ▶ Lemma 26.

If Σ P // n a ⊕ b ⊢ i is derivable then (1, P ) // a (i, [a, b]) ≻ * (0, [0; 0]).

◀ Undecidability of Sub-Exponential Linear Logic

Having established the undecidability of MM nd via FRACTRAN reg and MMA0 2 , we can now switch to undecidability in some fragments of linear logic and give a comparison between two different reductions. We introduce the intuitionistic version of sub-exponential linear logic [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF] (IMSELL) and mechanise a many-one reduction from MM nd to entailment in IMSELL.

Even if the former reduction [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF] applies to classical sub-exponential linear logic with one sided sequents, our own reduction function is inspired from it. However, the completeness proof that we have mechanised largely differs since we avoid focused proofs (used to recover computations) and instead, adapt the trivial phase semantics argument [START_REF] Larchey | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF][START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. Additionally we precisely compare the reduction to ILL with the reduction to IMSELL by starting from the same MM nd seed, detailing what set of logical rules are used to simulate those machines.

The ILL and IMSELL fragments (files ILL.v and IMSELL.v)

We introduce two fragments/extensions of intuitionistic linear logic (ILL) that allow for a reduction from non-deterministic two counters Minsky machines.

The first fragment of the ILL logic we consider is composed of propositional formulae build from two binary connectives, the linear implication ⊸ and additive conjunction &, and one modality, exponentiation !. Logical variables come from (a copy of) the N type. Formally, the formulae of ILL are of the form A, B ::

= X | A ⊸ B | A & B | !A
where X : N. To simplify, we abusively call this fragment ILL. By cut-elimination, the reduction discussed below also works for larger fragments containing more connectives like ⊗, ⊕, etc.

The sequents of ILL are intuitionistic, i.e. a pair (Γ, A) written Γ ⊢ A where Γ is a multiset of formulae and A is a single formula. Multisets are just lists identified up-to permutations. If it is more convenient to work with lists, as we do in the Coq mechanization, then an explicit permutation rule is added to the sequent rules of the S-ILL calculus in Fig. 2.

The three leftmost rules are the identity (or axiom) rule stating that the sequent A ⊢ A has a trivial proof, and then the left-and right-introduction rules for the linear implication ⊸. The three rules middle-left are two left-and one right-introduction rules for the additive conjunction &. The two middle-right rules are modal rules, on top, the promotion rule, and at bottom, the dereliction rule. Finally, on the right-hand-side are the structural rules for the ! modality, i.e. weakening on top and contraction at the bottom. Notice that specifically, linear logic does not allow for general weakening or contraction rules.

On the other hand, IMSELL is a purely multiplicative fragment but with several modalities, among them exponentials. The logic is parameterized with a fixed type Λ of modalities and a fixed sub-type U : Λ → P of unbounded modalities, also called exponentials. We follow the set theoretic syntax and write u ∈ U (instead of U u) when u is unbounded. The formulae of IMSELL Λ are of the form A, B ::

= X | A ⊸ B | ! m A
where X : N and m : Λ. So compared to ILL, the additive & is missing whereas the modality ! becomes indexed as ! m with m spanning over Λ. IMSELL Λ sequents have the same structure Γ ⊢ A as those of ILL except that they are composed of IMSELL Λ formulae instead.

Before we describe the associated sequent calculus S-IMSELL Λ , we introduce supplementary structures on modalities: a pre-order ≼ : Λ → Λ → P, i.e. a reflexive and transitive binary relation, such that U is upward-closed for ≼, i.e. u ≼ m and u ∈ U entail m ∈ U for any m, u : Λ. In the sequel, we will somehow abuse the notation and denote Λ both for the base type and the modal structure (Λ, U, ≼) moreover assuming the pre-order and upward-closure properties.

F S C D 2 0 2 1 18:12 Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

A ⊢ A A, Γ ⊢ B Γ ⊢ A ⊸ B Γ ⊢ A B, ∆ ⊢ C A ⊸ B, Γ, ∆ ⊢ C Γ ⊢ A Γ ⊢ B Γ ⊢ A & B A, Γ ⊢ C A & B, Γ ⊢ C B, Γ ⊢ C A & B, Γ ⊢ C !Γ ⊢ B !Γ ⊢ !B A, Γ ⊢ B !A, Γ ⊢ B Γ ⊢ B !A, Γ ⊢ B !A, !A, Γ ⊢ B !A, Γ ⊢ B Figure 2
The S-ILL sequent calculus.

A ⊢ A A, Γ ⊢ B Γ ⊢ A ⊸ B Γ ⊢ A B, ∆ ⊢ C A ⊸ B, Γ, ∆ ⊢ C ! ⋆ Γ ⊢ B ! ⋆ Γ ⊢ ! m B m ≼ ⋆ A, Γ ⊢ B ! m A, Γ ⊢ B Γ ⊢ B ! u A, Γ ⊢ B u ∈ U ! u A, ! u A, Γ ⊢ B ! u A, Γ ⊢ B u ∈ U Figure 3
The S-IMSELL Λ sequent calculus with (Λ, U, ≼).

In the sequent rules of the S-IMSELL Λ calculus of Fig. 3, the three leftmost rules are common with S-ILL, there is no rule for the additive conjunction & since it does belong to the fragment, and the modal rules have changed a bit. We skip over the two middle rules for the moment and consider the rightmost structural rules of weakening and contraction which generalise the corresponding rules of S-ILL, except that their use is limited to unbounded modalities (u ∈ U). Back to the two middle rules, the bottom dereliction rule applies to every modality, so a direct generalisation of the corresponding rule of S-ILL. However, the promotion rule (reproduced below on the left)

! ⋆ Γ ⊢ B ! ⋆ Γ ⊢ ! m B m ≼ ⋆ ! k1 A 1 , . . . , ! kn A n ⊢ B ! k1 A 1 , . . . , ! kn A n ⊢ ! m B m ≼ k 1 , . . . , m ≼ k n ! m Γ ⊢ B ! m Γ ⊢ ! m B
is somehow more complicated and deserves further explanations. The ⋆ notation represents a multiset k 1 , . . . , k n of modalities and ! ⋆ Γ represents the multiset ! k1 A 1 , . . . , ! kn A n . The constraint m ≼ ⋆ imposes that m is lower than every modality in {k 1 , . . . , k n }. Using these more explicit notations, we reframe it as in the above displayed middle rule. Finally, the (uniform) instance where m = k 1 = • • • = k n (the rightmost above; the constraint m ≼ ⋆ holds by reflexivity), matches the promotion rule of S-ILL.

Considered independently, all modalities behave like ILL modalities, satisfying dereliction and promotion rules, while only unbounded modalities allow for contraction and weakening. However, depending on the relation ≼, the promotion rule allows for non-trivial interactions between modalities. Given an unbounded modality ∞ ∈ U and replacing ! with ! ∞ , one can trivially embed the multiplicative fragment of ILL and recover intuitionistic multiplicative and exponential linear logic (IMELL), of which the (un)decidability of entailment is a notoriously difficult open problem [START_REF] Lazić | Non-Elementary Complexities for Branching VASS, MELL, and Extensions[END_REF]20].

Embedding in S-ILL vs. S-IMSELL (file ndMM2_IMSELL.v)

For the reduction from MM nd to IMSELL Λ to work out properly, we need at least three modality {a, b, ∞} where ∞ is the only unbounded modality (∞ ∈ U and a, b ̸ ∈ U), a ≼ ∞, b ≼ ∞ and a and b are incomparable, i.e. a ̸ ≼ b and b ̸ ≼ a. As a consequence, ∞ is also strictly above a and b. From now on, we assume that Λ satisfies these requirements. The coming discussion can also be understood in the minimal case where Λ 3 = {a, b, ∞} and we denote IMSELL 3 for either of these logics.

D. Larchey-Wendling

18:13

In this section, we review the encoding of MM nd sequents into both ILL and IMSELL 3 , and explain how, while mostly similar, they noticeably differ on how they handle zero tests combined with jumps. Notice that the encoding targeting ILL can be adapted to n registers Minsky machines (as done in [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]), while in the case of IMSELL 3 , working with two counters only is critically important to the construction.

Identifying the exponential ! with the unbounded modality ! ∞ allows to discuss IMELL, ILL and IMSELL 3 in a common syntactic framework, avoiding cumbersome notations for trivial embeddings. We show the derivability of the two following rules: generalised weakening and customised absorption.

▶ Lemma 28. The two following rules are derivable in IMELL, and hence ILL and IMSELL 3 :

∆ ⊢ B ! ∞ Σ, ∆ ⊢ B A, ! ∞ Σ, ∆ ⊢ B ! ∞ Σ, ∆ ⊢ B A ∈ Σ
Proof. We obtain the left generalised weakening rule by repeating the weakening rule. For customised absorption, it is the combination of dereliction and contraction. ◀

These derived rules are essential tools for the reduction from MM nd . Let us review the other tools. Recall that a MM nd sequent is of the form Σ // n x ⊕ y ⊢ p. We encode this with an IMSELL 3 (or ILL) sequent of the form ! ∞ Σ, ∆ ⊢ p where ∆ := xα, yβ encodes the pair (x, y) : N × N, i.e. α (resp. β) is repeated x (resp. y) times. Hence increment and decrement operations on the values x/y naturally correspond to the multiset operations. We do not need to specify what formulae are α and β for the moment, but these will differ in the ILL case compared to the IMSELL 3 case. On the other hand, p or q will always be logical variables.

First, we show how to simulate the INC n α p q rule of S-MM nd :

Σ // n 1+x ⊕ y ⊢ q Σ // n x ⊕ y ⊢ p INCn α p q ∈ Σ ⇝ ! ∞ Σ, α, ∆ ⊢ q ! ∞ Σ, ∆ ⊢ α ⊸ q p ⊢ p (α ⊸ q) ⊸ p, ! ∞ Σ, ∆ ⊢ p (α ⊸ q) ⊸ p ∈ Σ ! ∞ Σ, ∆ ⊢ p
and the DEC n α p q rule of S-MM nd :

Σ // n x ⊕ y ⊢ q Σ // n 1+x ⊕ y ⊢ p DECn α p q ∈ Σ ⇝ α ⊢ α ! ∞ Σ, ∆ ⊢ q p ⊢ p q ⊸ p, ! ∞ Σ, ∆ ⊢ p α ⊸ (q ⊸ p), ! ∞ Σ, α, ∆ ⊢ p α ⊸ (q ⊸ p) ∈ Σ ! ∞ Σ, α, ∆ ⊢ p
Notice that we only use the customised absorption rule, the left-and right-introduction rules for ⊸ and the identity (axiom) rule hence simulating INC n α p q and DEC n α p q can be performed within the IMELL fragment.

The axiom rule STOP n p of S-MM nd (acceptance of (0, 0) at p) can also be simulated

Σ // n 0 ⊕ 0 ⊢ p STOPn p ∈ Σ ⇝ p ⊢ p ⊢ p ⊸ p p ⊢ p (p ⊸ p) ⊸ p ⊢ p (p ⊸ p) ⊸ p, ! ∞ Σ ⊢ p (p ⊸ p) ⊸ p ∈ Σ ! ∞ Σ, ∅ ⊢ p
using the customised absorption rule, then the generalised weakening rule, the left-and right-introduction rules for ⊸ and the identity rule. Hence an IMELL proof as well.

The remaining rules of MM nd , that of e.g. ZERO n α p q, a zero test combined with a jump instruction, are the problematic rules to encode in the IMELL fragment. This can however be done in ILL and in IMSELL 3 , but the techniques for the two fragments diverge precisely on these ZERO n α p q instructions. Let us first review5 the (idea behind the) legacy encoding of Minsky machines into linear logic [17], mechanized for ILL in [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. The idea is to fork the ZERO n α p q simulation into a proof-search branch where only a zero test on α is performed, and in the other branch, only a jump to q is performed:

Σ // n 0 ⊕ y ⊢ q Σ // n 0 ⊕ y ⊢ p ZEROn α p q ∈ Σ ⇝ . . . ! ∞ Σ, yβ ⊢ α ! ∞ Σ, yβ ⊢ q ! ∞ Σ, yβ ⊢ α & q p ⊢ p (α & q) ⊸ p, ! ∞ Σ, yβ ⊢ p (α & q) ⊸ p ∈ Σ ! ∞ Σ, yβ ⊢ p
Notice that α and β denote fresh logical variables. Critically for this encoding, the additive conjunction & is used to copy the context into the two premises, implementing a fork. The zero test on left sub-branch can however by performed in IMELL only:

β ⊢ β ! ∞ Σ, ∅ ⊢ α • • • ! ∞ Σ, yβ ⊢ α α ⊢ α α ⊸ α, ! ∞ Σ, yβ ⊢ α β ⊸ (α ⊸ α), ! ∞ Σ, β, yβ ⊢ α β ⊸ (α ⊸ α) ∈ Σ ! ∞ Σ, (1+y)β ⊢ α α ⊢ α ⊢ α ⊸ α α ⊢ α (α ⊸ α) ⊸ α, ∅ ⊢ α (α ⊸ α) ⊸ α, ! ∞ Σ, ∅ ⊢ α (α ⊸ α) ⊸ α ∈ Σ ! ∞ Σ, ∅ ⊢ α • • •
Notice that the dots above ! ∞ Σ, yβ ⊢ α mean repetition of the lower part of the proof until exhaustion of all the β from the context: this is implemented by an induction on y, and the base case where y = 0 corresponds to the upper part of the proof, starting at ! ∞ Σ, ∅ ⊢ α and completed on the right hand side, simulating of a would be STOP n α instruction (see above).

We see that α together with the formulae β ⊸ (α ⊸ α) and (α ⊸ α) ⊸ α in Σ allow α to perform the elimination of all the β from the context. However, α will not allow the removal of any α and hence, the zero test branch cannot be completed if ∆ contains an occurrence of α, i.e. when x ̸ = 0. This encoding of the zero test using α, while it can already be performed in IMELL, is pertinent only for ILL because it is in combination with the fork in (α & q) ⊸ p (see above) that it provides the ability to conditionally jump on zero.

Contrary to the ILL encoding, IMSELL 3 does not require (and cannot use) forking but instead uses sub-modalities to prevent jumping when the zero test fails. In that case, α and β are not atomic formulae anymore: they contain the bounded modalities ! a and ! b , and we define α := ! a α 0 and β := ! b β 0 where α 0 , β 0 are fresh variables. In the following encoding,

Σ // n 0 ⊕ y ⊢ q Σ // n 0 ⊕ y ⊢ p ZEROn α p q ∈ Σ ⇝ ! ∞ Σ, yβ ⊢ q ! ∞ Σ, yβ ⊢ ! b q p ⊢ p ! b q ⊸ p, ! ∞ Σ, yβ ⊢ p ! b q ⊸ p ∈ Σ ! ∞ Σ, yβ ⊢ p
notice that the upper rule is an instance of the promotion rule of S-IMSELL 3 . It is allowed because every formula on the left is prefixed either with the unbounded modality ! ∞ for those in ! ∞ Σ, or with the modality ! b for those in yβ = ! b β 0 , . . . , ! b β 0 , and we have both b ≼ ∞ and b ≼ b. On the other hand, an occurrence of α = ! a α 0 in the context, corresponding to a non-zero value of x, would prevent the application of the promotion rule (b ̸ ≼ a). This interaction of modalities in the promotion rule of IMSELL 3 is the key to simulate zero tests.

▶ Definition 29. Let us define α 0 := 0, β 0 := 1, p := 2 + p, α := ! a α 0 and β := ! b β 0 . We encode MM nd instructions as:

STOP n p := (p ⊸ p) ⊸ p
INC n α p q := (α ⊸ q) ⊸ p DEC n α p q := α ⊸ (q ⊸ p) ZERO n α p q := ! b q ⊸ p INC n β p q := (β ⊸ q) ⊸ p DEC n β p q := β ⊸ (q ⊸ p) ZERO n β p q := ! a q ⊸ p and then map (•) on the list Σ extensionally, i.e. [σ 1 ; . . . ; σ n ] := σ 1 , . . . , σ n .

▶ Lemma 30. If Σ // n x ⊕ y ⊢ p can be derived in S-MM nd then the sequent ! ∞ Σ, xα, yβ ⊢ p is provable in S-IMSELL 3 .
Proof. The argument proceeds by induction on the derivation of Σ // n x ⊕ y ⊢ p, combining the proof skeletons of the above discussion in a direct way. ◀

Trivial Phase semantics for IMSELL (file imsell.v)

We define trivial phase semantics for IMSELL Λ and show soundness w.r.t. the S-IMSELL Λ calculus. We start with a commutative monoid (M, •, ϵ). Typically, for the completeness of our reduction, we will only need to use the semantics for M = (N 2 , +, ⃗ 0), i.e. vectors of natural numbers of length 2, but the semantics works for any commutative monoid. For any X, Y ⊆ M , we define the point-wise extension by X • Y := {x • y | x ∈ X ∧ y ∈ Y } and its linear adjunct as X --• Y := {k ∈ M | {k} • X ⊆ Y } providing a residuated monoidal structure on the subset type M → P.

To interpret the modal structure (Λ, U, ≼), we further require for each modality m ∈ Λ, a subset K m ⊆ M i.e. a predicate K m : M → P. We assume that the map m → K m is monotonically decreasing w.r.t. ≼ (on the left below) and satisfies the three extra following rightmost axioms:

∀m k, m ≼ k → K k ⊆ K m ∀m, ϵ ∈ K m ∀m, K m •K m ⊆ K m ∀u ∈ U, K u ⊆ {ϵ}

Given any semantic interpretation [[•]

] ⊆ M of logical variables, we extend it inductively to IMSELL Λ sequents via trivial phase semantics: 6

[[A ⊸ B]] := [[A]] --• [[B]] [[! m A]] := [[A]] ∩ K m [[A 1 , . . . , A n ]] := [[A 1 ]] • • • • • [[A n ]]
:= [[A1]] • • • • • [[An]] instead of [[A1, . . . , An]] := cl([[A1]] • • • • • [[An]]
). Notice that trivial phase semantics is sound but not complete for IMELL, ILL and IMSELL Λ ; see [START_REF] Larchey | Nondeterministic Phase Semantics and the Undecidability of Boolean BI[END_REF] for details. Notice that because we work with commutative monoids, the above semantic interpretation of lists is invariant under permutations, hence is suitable for multisets. An

IMSELL Λ sequent Γ ⊢ A is valid in that interpretation if [[Γ]] ⊆ [[A]], or (equivalently) if ϵ ∈ [[Γ]] --• [[A]].
▶ Theorem 31. Trivial phase semantics is sound:

any sequent Γ ⊢ A provable in S-IMSELL Λ must satisfy ϵ ∈ [[Γ]] --• [[A]
] for any possible trivial phase semantics interpretation.

Proof. We proceed by structural induction on the S-IMSELL Λ derivation of Γ ⊢ A. In the code, the proof is limited to the case where M = (N n , +, ⃗ 0) for some n : N. Compared to the soundness of trivial phase semantics for S-ILL [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF], the only interesting new case is that of the promotion rule. In that case, we observe that m ≼ k 1 , . . . , k n implies Proof. We use a soundness argument for trivial phase semantics in place of reasoning by induction on focused derivation in MSELL as done in [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF]. We consider the monoid of vectors M = (N 2 , +, [0; 0]) of length 2 of natural numbers. We define the following interpretation for modalities,

K k1 •• • ••K kn ⊆ K m . ◀ 5
K m [x; y] := ≼ m → y = 0) ∧ (b ≼ m → x = 0) ∧ (m ∈ U → x = 0 ∧ y = 0),
and as a consequence, we can check that K m satisfies the required axioms as well as

K a = [x; 0] | x ∈ N , K b = [0; y] | y ∈ N ,
= ZERO n α p q. Then σ = ! b q ⊸ p is interpreted as ([[q]] ∩ K b ) --• [[p]]. Hence [0; 0] ∈ [[σ]] ↔ [[q]] ∩ K b ⊆ [[p]],
i.e. for any [x; y] : N 2 , if Σ // n x ⊕ y ⊢ q and x = 0 then Σ // n x ⊕ y ⊢ p which is precisely the instance of rule ZERO n α p q ∈ Σ of S-MM nd .

From the previous observation, we deduce [0

; 0] ∈ [[! ∞ Σ]]. Now let us consider a sequent ! ∞ Σ, xα, yβ ⊢ p which is provable in S-IMSELL 3 . By the soundness Theorem 31, we know that [0; 0] ∈ [[! ∞ Σ, xα, yβ]] --• [[p]]. Since [x; y] = [0; 0] + [x; y] ∈ [[! ∞ Σ]] • [[xα, yβ]] = [[! ∞ Σ,

Related works and Implementation remarks

While Theorem 33 gives us a mechanised synthetic proof of the undecidability of IMSELL 3 , neither its statement nor the arguments deployed directly provide hints towards a solution to the question of the decidability IMELL/MELL. As in the original pen and paper proof [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF], the two bounded modalities ! a and ! b , and their interaction with the unbounded modality ! ∞ in the promotion rule, play an essential role in the simulation of conditional jumps of two counters Minsky machines. While the zero test can be implemented in MELL only, the provided implementation consumes its context and thus cannot conditionally branch at the same time, hence the fork used in the case of ILL [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. However Theorem 33 does give indications that certain decidability arguments for MELL are bound to fail, e.g. those that would also apply to MSELL in general, or IMSELL 3 in particular. It is our understanding that the refutation [20] of the faulty proof attempt for the decidability of MELL [START_REF] Bimbó | The decidability of the intensional fragment of classical linear logic[END_REF] partly proceeds in showing how the claimed "proof" technique would easily generalise to MSELL. In the same vein, the lower bounds on the complexity of a would be decision procedure for MELL [START_REF] Lazić | Non-Elementary Complexities for Branching VASS, MELL, and Extensions[END_REF], and more recently the reachability problem for Petri nets themselves [START_REF] Czerwiński | The reachability problem for Petri nets is not elementary[END_REF], indicate that a decision procedure for MELL must be of non-elementary complexity. The most recent investigations [START_REF] Leroux | The Reachability Problem for Petri Nets is Not Primitive Recursive[END_REF][START_REF] Czerwiński | Reachability in Vector Addition Systems is Ackermann-complete[END_REF] might very well confirm that this problem is Ackermann complete and hence not primitive recursive.

Considering formalisation issues, the growing Coq library of undecidability proofs [START_REF] Forster | A Coq Library of Undecidable Problems[END_REF] was of course of great help to this work. Indeed, at the time we decided to try to implement the undecidability of MSELL, the framework for certified programming with Minsky machines was already part of the library [START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF]. Hence, to get two counters Minsky machines, i.e. the seed of undecidability of the pen and paper proof [START_REF] Chaudhuri | Expressing additives using multiplicatives and subexponentials[END_REF], only a modest step from many counters machines was necessary and this was even alleviated by the results on the FRACTRAN language [START_REF] Larchey | Hilbert's Tenth Problem in Coq[END_REF], factoring out the Gödel coding phase. In fact, we contributed the seed of two counters machines much ahead of the MSELL result, and in the meantime, this seed was used to establish to undecidability uniform boundedness for simple stack machines and then of the problem of semi-unification [START_REF] Dudenhefner | Undecidability of Semi-Unification on a Napkin[END_REF]. This illustrates a critical aspect of this undecidability framework: its extensive range of seed problems for plugging into it.

Indeed, there is an important issue to consider when proving undecidability by many-one reduction, by far the most used method in the field: even mechanised, your proof is only as strong as the implementation of your seed problem. Typical problems can exhibit subtleties that show up at the mechanisation level: for instance Turing machines are built on tapes, a potentially infinite structure of which it could be easy to corrupt the implementation. Choosing a seed already linked to the many-one equivalence class containing easy to describe problems such as e.g. the Post correspondence problem or FRACTRAN gives much more confidence that starting from an isolated seed, still to be mechanically checked undecidable.

Another aspect which is mostly overlooked in pen and paper proofs is the computability of the reduction function. The reason is that programming with low-level Turing complete models of computation is hard and painful, with encodings at every corner. To get a glimpse of the difficulty, think of a Turing machine working with logical formulas: because it only manipulates text written on tapes, it has to implement a syntax analyser, moreover proved correct. And only then can it start its real work. The general shortcut used in pen and paper proofs to avoid this kind of description is to speak about "algorithms" that manipulate high-level data-structures and rely on an informal and consensual understanding of what these are, hand-waving away the implementation issues completely.

In this regard, the synthetic computability framework allows, at the price of relying on the computability of Coq functions -e.g. by avoiding axioms, -to formally describe the reduction functions in a language strict enough to ensures their computability, but at the same time powerful enough to largely avoid complex encodings and hence get more natural correctness proofs following or inspired from pen and paper ones. Using a constructive framework like e.g. Coq or Agda is essential in that approach, because in classical frameworks, there is no direct way to automatically ensure the general computability of the defined (reduction) functions.

A Proof (sketch) of Proposition 17

Let us use the denotation s (resp. d) for the dynamic value of register s (resp. d). Hence, the contents of the registers is represented by the vector [s; d] of length 2 with initial value [x; 0]. Also, the initial value of the PC is i 0 = i. The sub-program MULT_CST a s d p i 0 multiplies s with p and adds the result to the contents of d while emptying s, so the PC moves to i 1 and s = 0 and d = px. Then MOD_CST a d s i 2 i 4 q i 1 tests the divisibility of d by q, which succeeds under the assumption qy = px. By Proposition 15, this transfers the control to i 2 and now d = 0 and s = px. Then DIV_CST a s d q i 2 divides s with q while swapping the registers hence now s = 0, d = y and the PC is at i 3 . Then TRANSFER a d s i 3 swaps s with d hence now s = y and d = 0 and PC is now i 4 . Finally, JUMP a j d transfers the control to j without altering the registers.

B Proof (sketch) of Proposition 18

As in the proof of Proposition 17, we reach the state where the PC is at i 1 and s = 0 and d = px. However now, MOD_CST a d s i 2 i 4 q i 1 gives a negative answer to the divisibility of d by s hence according to Proposition 14, the control is transferred to i 5 while s = px and d = 0. Then DIV_CST a s d p i 5 divides the contents of s by p, reverting it to its initial value but there is a swap: PC is at i 6 , s = 0 and d = x. Finally TRANSFER a d s i 6 swaps again and reverts the registers to their initial values s = x and d = 0 while the PC moves to the end of the sub-program at i 7 .

C Proof (sketch) of Theorem 21

The implication 2 =⇒ 3 is trivial. We

18:20 Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Let us now finish with 3 =⇒ 1 and assume (1, FRAC_MMA a Q) // a (1, [x; 0]) ↓. We show that Q // F x ↓. Because (1, FRAC_STEP a 1 Q 1) is a sub-program of (1, FRAC_MMA a Q), we also have (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ↓. Hence there is k, j : N and ⃗ v : N 2 such that (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ≻ k (j, ⃗ v) and out j (1, FRAC_STEP a 1 Q 1). We prove Q // F x ↓ by strong induction on k. By Proposition 1, one can decide between two possibilities: either Q // F x ⊁ ⋆ in which case Q // F x ↓ is obvious; or there is y such that Q // F x ≻ y. We deduce (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ≻ δ (1, [y; 0]) for some δ > 0 by Lemma 19. Since the step relation is deterministic for Minsky machines, we have (1, FRAC_STEP a 1 Q 1) // a (1, [y; 0]) ≻ k-δ (j, ⃗ v) hence we can apply the induction hypothesis (k -δ < k) and we get Q // F y ↓. Combining with Q // F x ≻ y, we conclude Q // F x ↓.

4

  hence formally a Boolean value of type B.F S C D 2 0 2 1 18:10 Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

  DECa x j⟩ := [DECn x i j; ZEROn x i (1+i)] ⟨⟨i, σ :: P ⟩⟩ := ⟨i, σ⟩ + + ⟨⟨1+i, P ⟩⟩ ▶ Proposition 24. The encodings ⟨•, •⟩ and ⟨⟨•, •⟩⟩ are sound: 1. assuming the inclusion ⟨i, σ⟩ ⊆ Σ, if σ // a (i, [a; b]) ≻ (j, [a ′ ; b

Proof.▶

  The argument proceeds by structural induction on the derivation of Σ P // n a ⊕ b ⊢ i, i.e. by analysing the structure of S-MM nd derivations. The following result is an essential ingredient in this case analysis: c ∈ ⟨⟨i, P ⟩⟩ → ∃L σ R, P = L + + σ :: R ∧ c ∈ ⟨|L| + i, σ⟩. It allows to recover the MMA 2 instructions from which MM nd instructions originate. ◀ Corollary 27. MMA0 2 ⪯ MM nd . Proof. The reduction maps an instance (P, [a; b]) of MMA0 2 to the sequent Σ P // n a ⊕ b ⊢ 1. Lemmas 25 and 26 provide the equivalence between (1, P ) // a (1, [a, b]) ⇝ (0, [0; 0]) and the derivability of Σ P // n a ⊕ b ⊢ 1, which ensures the correctness of the reduction.

6

  The trivial qualifier refers to the use of the identity closure cl(X) = X in the interpretation of modalities, i.e. [[! m A]] := [[A]] ∩ Km instead of the more general [[! m A]] := cl([[A]] ∩ Km) where cl(•) : (M → P) → (M → P) is a stable closure operator. This also applies to the (implicit) multiplicative conjunction where [[A1, . . . , An]]

F S C D 2 0 2 1 18: 16 Synthetic

 116 Undecidability of MSELL via FRACTRAN Mechanised in Coq

  and K ∞ = [0; 0] . We interpret logical variables as: [[α 0 ]] := [1; 0] and [[β 0 ]] := [0; 1] and [[p]] = [x; y] | Σ // n x ⊕ y ⊢ p and thus we have [[α]] = [[! a α 0 ]] = [[α 0 ]] ∩ K a = [1; 0] and [[β]] = [0; 1] . Consequently, we get [[xα, yβ]] = [x; y] . We verify that the interpretation of the IMSELL 3 encoding σ of MM nd instructions in Σ contains the zero vector, i.e. ∀σ, σ ∈ Σ → [0; 0] ∈ [[σ]]. For instance, let us consider the case σ

▶

  xα, yβ]], by the definition of --• we deduce [x; y] = [0; 0] + [x; y] ∈ [[p]], and hence we conclude that Σ // n x ⊕ y ⊢ p holds. ◀ Theorem 33. Let (Λ, U, ≼) contain three modalities a, b and ∞ such that ∞ ∈ U, a, b ̸ ∈ U, a, b ≼ ∞, a ̸ ≼ b and b ̸ ≼ a. Then we have a reduction MM nd ⪯ IMSELL Λ , hence derivability in the S-IMSELL Λ calculus is undecidable.

  show 1 =⇒ 2 and 3 =⇒ 1. Let us start with 1 =⇒ 2. As an instance of Lemma 19, if Q// F x ≻ y holds then we have (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ≻ + (1, [y; 0]). By transitivity, from Q // F x ≻ * y we can deduce (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ≻ * (1, [y; 0]). Now assuming Q // F x ↓, we get some y such that Q // F x ≻ * y and Q // F y ⊁ ⋆. Hence we have (1, FRAC_STEP a 1 Q 1) // a (1, [x; 0]) ≻ * (1, [y; 0]). By Lemma 20, as Q // F y ⊁ ⋆, we get (1, FRAC_STEP a 1 Q 1) // a (1, [y; 0]) ≻ * (|FRAC_STEP a 1 Q 1| + 1, [y; 0]). We deduce (1, FRAC_MMA a Q) // a (1, [x; 0]) ≻ * (|FRAC_STEP a 1 Q 1| + 1, [y; 0]) since (1, FRAC_STEP a 1 Q 1) is a sub-program of (1, FRAC_MMA a Q).The nullifying code and the jump finish the computation and we get our proof that (1, FRAC_MMA a Q) // a (1, [x; 0]) ⇝ (0, [0; 0]) holds. F S C D 2 0 2 1

Proposition 4. The

  step relation for alternate Minsky machines is deterministic and total: 1. for any states st , st 1 and st 2 , if σ // a st ≻ st 1 and σ // a st ≻ st 2 then st 1 = st 2 ; 2. for any state (i 1 , ⃗ v 1 ), one can compute a state (i 2 , ⃗ v 2 ) such that σ // a (i 1 , ⃗ v 1 ) ≻ (i 2 , ⃗ v 2 ).

.4 The completeness of the reduction (file ndMM2_IMSELL.v)

  If the sequent ! ∞ Σ, xα, yβ ⊢ p is provable in S-IMSELL 3 , then there is a derivation of Σ // n x ⊕ y ⊢ p in S-MM nd .

▶ Lemma 32.

17

  Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. In 31st Annual Symposium on Foundations of Computer Science, volume 2, pages 662-671. IEEE Computer Society, 1990. doi:10.1109/FSCS.1990.89588. 18 Ernst W. Mayr. An algorithm for the general Petri net reachability problem. In Proceedings of the Thirteenth Annual ACM Symposium on Theory of Computing, STOC '81, page 238-246, New York, NY, USA, 1981. Association for Computing Machinery. doi:10.1145/800076. 802477. 19 Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. 20 Lutz Straßburger. On the decision problem for MELL. Theoret. Comput. Sci., 768:91-98, 2019.

However, e.g. the function n → 0 cannot be directly represented by a FRACTRAN program where n would be the starting state leading, after finitely many steps of computation, to the 0 terminated state.

here we only discuss the ILL case, i.e. we do not replicate the former ILL mechanisation[START_REF] Forster | Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines[END_REF] in the code.

Funding Dominique Larchey-Wendling: partially supported by the TICAMORE project (ANR grant 16-CE91-0002).

: https://github.com/uds-psl/coq-library-undecidability/releases/tag/FSCD-2021 archived at swh:1:rev:4115398f10c42a41833036f8c4500f24233cc9a7


Yao-Qiang Li
email: yaoqiang.li@imj-prg.fr

HAUSDORFF DIMENSION OF FREQUENCY SETS OF UNIVOQUE SEQUENCES

Keywords: Mathematics Subject Classification. Primary 37B10; Secondary 11K55, 11A63, 28A80 univoque sequence, digit frequency, Hausdorff dimension, Bernoulli-type measure

We study the set Γ consisting of univoque sequences, the set Λ consisting of sequences in which the lengths of consecutive zeros and consecutive ones are bounded, and their frequency subsets Γ a , Γ a , Γ a and Λ a , Λ a , Λ a consisting of sequences respectively in Γ and Λ with frequency, lower frequency and upper frequency of zeros equal to some a ∈ [0, 1]. The Hausdorff dimension of all these sets are obtained by studying the dynamical system (Λ (m) , σ) where σ is the shift map and Λ (m) = w ∈ {0, 1} N : w does not contain 0 m or 1 m for integer m ≥ 3, studying the Bernoulli-type measures on Λ (m) and finding out the unique equivalent σ-invariant ergodic probability measure.

INTRODUCTION

Let N be the set of positive integers {1, 2, 3, • • • } and define Γ := w ∈ {0, 1} N : w < σ k w < w for all k ≥ 1 where σ is the shift map on {0, 1} N , 0 := 1, 1 := 0 and w :=

w 1 w 2 • • • for all w = w 1 w 2 • • • ∈ {0, 1} N .
The set Γ is strongly related to two well known research topics, iterations of unimodal functions and unique expansions of 1 (see [START_REF] Allouche | Non-integer bases, iteration of continuous real maps, and an arithmetic self-similar set[END_REF] for more details).

On the one hand, in 1985, Cosnard [START_REF] Cosnard | Étude de la classification topologique des fonctions unimodales[END_REF] proved that a sequence α = (α n ) n≥1 ∈ {0, 1} N is the kneading sequence of 1 for some unimodal function f if and only if τ (α) ∈ Γ , where τ : {0, 1} N → {0, 1} N is a bijection defined by τ (w) := ( n i=1 w i (mod 2)) n≥1 and Γ := w ∈ {0, 1} N : w ≤ σ k w ≤ w for all k ≥ 0 is similar to Γ in the sense that Γ \{periodic sequences} = Γ. The structure of Γ \{(10) ∞ } was studied in detail by Allouche [START_REF] Allouche | Théorie des nombres et automates[END_REF] (see also [START_REF] Allouche | Itérations de fonctions unimodales et suites engendrées par automates[END_REF]). The generalizations of Γ and Γ (to more than two digits) were studied in [START_REF] Allouche | Théorie des nombres et automates[END_REF][START_REF] Allouche | Univoque numbers and an avatar of Thue-Morse[END_REF].

On the other hand, expansions of real numbers in non-integer bases were introduced by Rényi [START_REF] Rényi | Representations for real numbers and their ergodic properties[END_REF] in 1957 and then widely studied until now (see for examples [START_REF] Allouche | Periodic unique beta-expansions: the Sharkovskiȋ ordering[END_REF][START_REF] Blanchard | β-expansions and symbolic dynamics[END_REF][START_REF] Wang | Distribution of full cylinders and the Diophantine properties of the orbits in β-expansions[END_REF][START_REF] Komornik | Unique developments in non-integer bases[END_REF][START_REF] Li | Beta-expansion and continued fraction expansion[END_REF][START_REF] Li | Distributions of full and non-full words in beta-expansions[END_REF][START_REF] Parry | On the β-expansions of real numbers[END_REF][START_REF] Schmeling | Symbolic dynamics for β-shifts and self-normal numbers[END_REF]). In 1990, Erdös, Joó and Komornik [START_REF] Erdös | Characterization of the unique expansions 1 = ∞ i=1 q -ni and related problems[END_REF] proved that a sequence α = (α n ) n≥1 ∈ {0, 1} N is the unique expansion of 1 in some base q ∈ (1, 2) if and only if α ∈ Γ. Thus we call Γ the set of univoque sequences in this paper. Note that the term "univoque sequence" is different in some other papers [START_REF] Daróczy | Univoque sequences[END_REF][START_REF] Vries | On the number of unique expansions in non-integer bases[END_REF][START_REF] Vries | Unique expansions of real numbers[END_REF].

For any a ∈ [0, 1], the frequency subsets of Γ are defined by

Γ a := w ∈ Γ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , Γ a := w ∈ Γ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , Γ a := w ∈ Γ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a ,
and the frequency subsets of Λ := w ∈ {0, 1} N : the lengths of consecutive 0's and consecutive 1's in w are bounded are defined by

Λ a := w ∈ Λ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , Λ a := w ∈ Λ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , Λ a := w ∈ Λ : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a ,
where # denotes the cardinality. It is straightforward to check Γ ⊂ Λ. Let U := q ∈ (1, 2) : 1 has a unique q-expansion be the set of univoque bases. It is proved in [START_REF] Daróczy | On the structure of univoque numbers[END_REF][START_REF] Komornik | Hausdorff dimension of univoque sets and Devil's staircase[END_REF] that U is of full Hausdorff dimension. That is, dim H U = 1. For more research on U, we refer the reader to [START_REF] Vries | Topology of the set of univoque bases[END_REF][START_REF] Komornik | On the topological structure of univoque sets[END_REF][START_REF] Kong | Univoque bases and Hausdorff dimension[END_REF].

On frequency sets, there is a well known result given by Eggleston [START_REF] Eggleston | The fractional dimension of a set defined by decimal properties[END_REF] saying that for any a ∈ [0, 1], the classical Eggleston-Besicovitch set has Hausdorff dimension dim H

x ∈ [0, 1) :

lim n→∞ #{k : 1 ≤ k ≤ n, ε k (x) = 0} n = a = -a log a -(1 -a) log(1 -a) log 2 , (1.1) where ε 1 (x)ε 2 (x) • • • ε n (x) • • •
is the greedy binary expansion of x, and 0 log 0 := 0.

Motivated by the above mentioned results, correspondingly, we study the set of univoque sequences Γ and the larger set Λ, study their frequency subsets Γ a , Γ a , Γ a , Λ a , Λ a , Λ a and give the following theorem as the main result in this paper. Let dim H (•, d 2 ) denote the Hausdorff dimension in {0, 1} N equipped with the usual metric d 2 .

Theorem 1.1. (1) We have dim H (Γ, d 2 ) = dim H (Λ, d 2 ) = 1. (2) For all a ∈ [0, 1] we have dim H (Γ a , d 2 ) = dim H (Γ a , d 2 ) = dim H (Γ a , d 2 ) = dim H (Λ a , d 2 ) = dim H (Λ a , d 2 ) = dim H (Λ a , d 2 ) = -a log a -(1 -a) log(1 -a) log 2 ,
where 0 log 0 := 0.

It is known that by defining Bernoulli measures, and then calculating the lower local dimension of the measures and using Billingsley Lemma [18, Proposition 2.3], the Hausdorff dimension of classical Eggleston-Besicovitch sets mentioned above can be obtained. But this is based on the fact that only expansions in integer bases are considered in classical Eggleston-Besicovitch sets, there are no forbidden words in the symbolic space and the Bernoulli measures are invariant and ergodic with respect to the shift map. Ergodicity garuantees that classical Eggleston-Besicovitch sets have positive Bernoulli measures, which is a condition needed for applying Billingsley Lemma to get the lower bound of the Hausdorff dimension. If there are forbidden words, such as expansions in non-integer bases [START_REF] Li | Random walks associated to beta-shifts[END_REF], the corresponding Bernoulli-type measures are not ergodic (actually not invariant). This makes some difficulties to be overcome. In [START_REF] Li | Random walks associated to beta-shifts[END_REF], after defining Bernoullitype measures, the authors found out the equivalent invariant ergodic measures, studied the relation between the equivalent measures and the original measures and obtained the Hausdorff dimension of Eggleston-Besicovitch (frequency) sets for a class of non-integer bases (see [START_REF] Li | Random walks associated to beta-shifts[END_REF]Theorem 1.2]) by applying an avatar of the Billingsley Lemma. This paper follows a similar framework and construction, but most of the details we need to confirm are different.

For any a ∈ [0, 1] we define the global frequency sets in {0, 1} N by

G a := w ∈ {0, 1} N : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , G a := w ∈ {0, 1} N : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a , G a := w ∈ {0, 1} N : lim n→∞ #{k : 1 ≤ k ≤ n, w k = 0} n = a ,
for any integer m ≥ 3 we define

Λ (m) := w ∈ {0, 1} N : w does not contain 0 m or 1 m ,
and we let

Λ (m) a := Λ (m) ∩ G a .
Here we give an outline for the proof of Theorem 1.1 (2) to explain how the concepts in this paper interact. Following the simple argument at the beginning of the Proof of Theorem 1.1 in Section 5, we know that it suffices to consider the lower bound of dim H (Γ a , d 2 ). Since (5.2) says that dim H (Γ a , d 2 ) ≥ dim H (Λ (m) a , d 2 ) for any integer m ≥ 3, we only need to find a good lower bound for dim H (Λ (m) a , d 2 ). Hence the main we need to prove is Lemma 5.3. By the Billingsley Lemma in metric space (Proposition 2.6), this can be done by constructing a suitable measure on (Λ (m) , d 2 ) such that Λ (m) a has positive measure. Thus we define the Bernoulli-type measure µ p in Section 4. To guarantee that Λ (m) a has positive measure, we want ergodicity (see (2) 2 in the Proof of Lemma 5.3). Hence we find out the unique σ-invariant ergodic measure λ p equivalent to µ p in Section 4, and calculate its value on the cylinder [0] in Lemma 5.2, which is in fact a relation between µ p and λ p . Finally we apply Billingsley Lemma to obtain Lemma 5.3.

This paper is organized as follows. In Section 2, we give some basic notation and preliminaries on dynamical systems and measure theory. In Section 3, we study related digit occurrence parameters and their properties which will be used later. In Section 4 we study Bernoulli-type measures, and finally we prove our main result in Section 5.

NOTATION AND PRELIMINARIES

Let {0, 1} * := ∞ n=1 {0, 1} n and {0, 1} N be the sets of finite words and infinite sequences respectively on two digits {0, 1}. For any integer m ≥ 3, recall where n ∈ N. For a finite word w ∈ {0, 1} * , we use |w|, |w| 0 and |w| 1 to denote its length, the number of 0's in w and the number of 1's in w respectively. Besides,

Λ (m) = w ∈ {0,
w| k := w 1 w 2 • • • w k denotes the prefix of w with length k for w ∈ {0, 1} N or w ∈ {0, 1} n where n ≥ k. Let σ : {0, 1} N → {0, 1} N be the shift map defined by σ(w 1 w 2 • • • ) = w 2 w 3 • • • for w ∈ {0, 1} N
and d 2 be the usual metric on {0, 1} N defined by

d 2 (w, v) := 2 -inf{k≥0:w k+1 =v k+1 } for w, v ∈ {0, 1} N ,
where

2 -∞ = 0. Then σ is continuous on ({0, 1} N , d 2 ). By σ(Λ (m) ) = Λ (m) , we know that (Λ (m) , σ) is a dynamical system. It is straightforward to check that the natural projection map π 2 : {0, 1} N → [0, 1], defined by π 2 (w) := ∞ n=1 w n 2 n for w ∈ {0, 1} N ,
is surjective and continuous. Besides, we need the following concepts and notation.

Definition 2.1 (Cylinder). Let m ≥ 3 be an integer and w ∈ Λ (m), * . We call

[w] := v ∈ Λ (m) : v begins with w
the cylinder in Λ (m) generated by w.

Definition 2.2 (Absolute continuity and equivalence). Let µ and ν be measures on a measurable space (X, F). We say that µ is absolutely continuous with respect to ν and denote it by µ ν if, for any A ∈ F, ν(A) = 0 implies µ(A) = 0. Moreover, if µ ν and ν µ we say that µ and ν are equivalent and denote this property by µ ∼ ν. Definition 2.3. Let C be a family of certain subsets of a set X.

(

) C is called a monotone class on X if 1 {A n } n≥1 ⊂ C and A 1 ⊂ A 2 ⊂ • • • ⇒ ∞ n=1 A n ∈ C; 2 {A n } n≥1 ⊂ C and A 1 ⊃ A 2 ⊃ • • • ⇒ ∞ n=1 A n ∈ C. (2) C is called a semi-algebra on X if 1 ∅ ∈ C; 2 A, B ∈ C ⇒ A ∩ B ∈ C; 3 A ∈ C ⇒ A c ∈ C Σf where A c := X \ A and C Σf := n i=1 C i : C 1 , • • • , C n ∈ C are disjoint, n ∈ N . (The subscript Σf means finite disjoint union.) (3) C is called an algebra on X if 1 ∅, X ∈ C; 2 A ∈ C ⇒ A c ∈ C; 3 A, B ∈ C ⇒ A ∩ B ∈ C. (4) C is called a sigma-algebra on X if 1 ∅, X ∈ C; 2 A ∈ C ⇒ A c ∈ C; 3 A 1 , A 2 , A 3 • • • ∈ C ⇒ ∞ n=1 A n ∈ C. 1
The following useful approximation lemma follows from [31, Theorem 0.1 and 0.7].

Lemma 2.4. Let (X, B, µ) be a probability space, C be a semi-algebra which generates the sigmaalgebra B and A be the algebra generated by C. Then

(1) A = C Σf := n i=1 C i : C 1 , • • • , C n ∈ C are disjoint, n ∈ N ;
(2) for each B ∈ B and each ε > 0, there is some A ∈ A with µ(A B) < ε.

In order to extend some properties from a small family to a larger one in some proofs in Section 4, we recall the following well known Monotone Class Theorem (see for example [20, Page 66]).

Theorem 2.5 (Monotone Class Theorem).

Let A be an algebra. Then the smallest monotone class containing A is precisely the smallest sigma-algebra containing A.

Let B(x, r) denote the closed ball centered on x with radius r. The following version of the Billingsley Lemma in metric space follows in the same way as the classical one in Euclidean space. Proposition 2.6 ([17, 18]). Let (X, d) be a metric space, E ⊂ X be a Borel set, µ be a finite Borel measure on X and s ≥ 0. If

µ(E) > 0 and lim r→0 log µ(B(x, r)) log r ≥ s for all x ∈ E,
then the Hausdorff dimension of E in (X, d) is no less than s.

DIGIT OCCURRENCE PARAMETERS

The digit occurrence parameters and their properties studied in this section will be used in Sections 4 and 5. (w) where #N denotes the cardinality of the set N . Proposition 3.2. Let m ≥ 3 be an integer and w, v ∈ Λ (m), * such that wv ∈ Λ (m), * . Then (wv). By v k = 0, we only need to prove

(1) N (m) 0 (w) + N (m) 0 (v) -1 ≤ N (m) 0 (wv) ≤ N (m) 0 (w) + N (m) 0 (v); (2) N (m) 1 (w) + N (m) 1 (v) -1 ≤ N (m) 1 (wv) ≤ N (m) 1 (w) + N (m) 1 (v). Proof. Let a = |w| and b = |v|. (1) 1 Prove N (m) 0 (wv) ≤ N (m) 0 (w) + N (m) 0 (v). It suffices to prove N (m) 0 (wv) ⊂ N (m) 0 (w) ∪ (N (m) 0 (v) + a), where N (m) 0 (v) + a := {j + a : j ∈ N (m) 0 (v)}. Let k ∈ N (m) 0 (wv). i) If 1 ≤ k ≤ a, then w k = 0, w 1 • • • w k-1 1 ∈ Λ (m), * and we get k ∈ N (m) 0 (w). ii) If a + 1 ≤ k ≤ a + b, then v k-a = 0 and w 1 • • • w a v 1 • • • v k-a-1 1 ∈ Λ (m), * . It follows from v 1 • • • v k-a-1 1 ∈ Λ (m), * that k -a ∈ N (m) 0 (v) and k ∈ N (m) 0 (v) + a. 2 Prove N (m) 0 (w) + N (m) 0 (v) ≤ N (m) 0 (wv) + 1. When v = 1 b , we get N (m) 0 (v) =
w 1 • • • w a v 1 • • • v k-1 1 ∈ Λ (m), * . (By contradiction) Assume w 1 • • • w a v 1 • • • v k-1 1 / ∈ Λ (m), * . Then w 1 • • • w a v 1 • • • v k-1 1 contains 0 m or 1 m . i) If w 1 • • • w a v 1 • • • v k-1 1 contains 0 m , then w 1 • • • w a v 1 • • • v k-1 contains 0 m . This con- tradicts wv ∈ Λ (m), * . ii) If w 1 • • • w a v 1 • • • v k-1 1 contains 1 m , by k ≥ s + 1, we know that w 1 • • • w a v 1 • • • v s-1 0v s+1 • • • v k-1 1 contains 1 m . Thus w 1 • • • w a v 1 • • • v s-1 contains 1 m or v s+1 • • • v k-1 1 contains 1 m . But w 1 • • • w a v 1 • • • v s-1 contains 1 m will contradict wv ∈ Λ (m), * , and v s+1 • • • v k-1 1 con- tains 1 m will imply v 1 • • • v k-1 1 contains 1 m which contradicts k ∈ N (m) 0 (v).
(2) follows in the same way as (1).

(w) = k : 1 ≤ k ≤ n, w k = 0, w 1 • • • w k-1 1 ∈ Λ (m), *
and

N (m) 0 (w) = #N (m) 0 (w).
We define (2) follows in the same way as (1).

N (m) 1 m-1 0 (w) := k : m ≤ k ≤ n, w k-m+1 • • • w k-1 w k = 1 m-1 0 and N (m) 1 m-1 0 := #N (m) 1 m-1 0 (w). 1 Prove {k : 1 ≤ k ≤ n, w k = 0} = N (m) 0 (w) ∪ N (m) 1 m-1 0 (w). ⊃ Obvious. ⊂ Let k ∈ {1, • • • , n} such that w k = 0. If k / ∈ N (m) 0 (w), then k ≥ m and w 1 • • • w k-1 1 / ∈ Λ (m), * . By w 1 • • • w k-1 ∈ Λ (m), * , we get w k-m+1 • • • w k-1 = 1 m-1 . This implies k ∈ N (m) 1 m-1 0 (w). 2 Prove N (m) 0 (w) ∩ N (m) 1 m-1 0 (w) = ∅. (By contradiction) Assume that there exists k ∈ N (m) 0 (w) ∩ N (m) 1 m-1 0 (w). Then k ≥ m, w k-m+1 • • • w k-1 = 1 m-1 and w 1 • • • w k-1 1 ∈ Λ (m), * . These imply w 1 • • • w k-m 1 m ∈ Λ (m), * ,

BERNOULLI-TYPE MEASURES ON Λ (m)

Let m ≥ 3 be an integer, B(Λ (m) ) be the Borel sigma-algebra on Λ (m) (equipped with the usual metric d 2 ) and p ∈ (0, 1). We define the (p, 1 -p) Bernoulli-type measure µ p on (Λ (m) , B(Λ (m) )) as follows:

I. Let µ p (∅) = 0, µ p (Λ (m) ) = 1, µ p [0] = p, and µ p [1] = 1 -p.
II. Suppose µ p has been defined for all cylinders of order n ∈ N. For any w ∈ Λ (m),n , if w0, w1 ∈ Λ (m),n+1 , we define III. By Carathéodory's measure extension theorem, we uniquely extend µ p from its definition on the family of cylinders to become a measure on B(Λ (m) ).

Remark 4.1. By the definition of µ p , we have

µ p [w] = p N (m) 0 (w) (1 -p) N (m) 1 (w)
for all w ∈ Λ (m), * .

Note that µ p is not σ-invariant. In fact,

µ p [0 m-2 1] = p m-2 (1 -p) but µ p (σ -1 [0 m-2 1]) = µ p [0 m-1 1]+µ p [10 m-2 1] = p m-1 +p m-2 (1-p) 2 = p m-2
(1-p) for all p ∈ (0, 1).

The main result in this section is the following.

Theorem 4.2. Let m ≥ 3 be an integer and p ∈ (0, 1). Then there exists a unique σ-invariant ergodic probability measure λ p on (Λ (m) , B(Λ (m) )) equivalent to µ p , where λ p is defined by

λ p (B) := lim n→∞ 1 n n-1 k=0 σ k µ p (B) for B ∈ B(Λ (m) ).
The proof is based on the following lemmas.

Lemma 4.3. Let m ≥ 3 be an integer, p ∈ (0, 1) and w, v ∈ Λ (m), * such that wv ∈ Λ (m), * . Then

µ p [w]µ p [v] ≤ µ p [wv] ≤ p -1 (1 -p) -1 µ p [w]µ p [v].
Proof. It follows from Remark 4.1 and Proposition 3.2.

Lemma 4.4. Let m ≥ 3 be an integer and p ∈ (0, 1). Then there exists a constant c >

1 such that c -1 µ p (B) ≤ σ k µ p (B) ≤ cµ p (B)
for all k ∈ N and B ∈ B(Λ (m) ).

ii) Prove

µ p σ -k [w] ≥ c -1 µ p [w].
In fact, when w 1 = 0, we have

µ p σ -k [w] = u 1 •••u k w∈Λ (m), * µ p [u 1 • • • u k w] ≥ u 1 •••u k-1 1w∈Λ (m), * µ p [u 1 • • • u k-1 1w] ( ) = u 1 •••u k-1 1∈Λ (m), * µ p [u 1 • • • u k-1 1w] ( ) ≥ u 1 •••u k-1 1∈Λ (m), * µ p [u 1 • • • u k-1 1]µ p [w] = µ p σ -(k-1) [1]µ p [w] ( ) ≥ p(1 -p) 2 µ p [w].
where ( ) follows from w 1 = 0 and w ∈ Λ (m), * , ( ) follows from Lemma 4.3 and ( ) follows from i). When w 1 = 1, in the same way, we can get

µ p σ -k [w] ≥ p 2 (1 -p)µ p [w]. (2) Prove c -1 µ p (B) ≤ σ k µ p (B) ≤ cµ p (B) for all k ∈ N and B ∈ B(Λ (m) ). Let C := [w] : w ∈ Λ (m), * ∪ ∅ , C Σf := n i=1 C i : C 1 , • • • , C n ∈ C are disjoint, n ∈ N and G := B ∈ B(Λ (m) ) : c -1 µ p (B) ≤ σ k µ p (B) ≤ cµ p (B) for all k ∈ N .
Then C is a semi-algebra on Λ (m) , C Σf is the algebra generated by C (by Lemma 2.4 (1)) and G is a monotone class. Since in [START_REF] Allouche | Théorie des nombres et automates[END_REF] we have already proved C ⊂ G, it follows that

C Σf ⊂ G ⊂ B(Λ (m) ). Noting that B(Λ (m)
) is the smallest sigma-algebra containing C Σf , it follows from the Monotone Class Theorem (Theorem 2.5) that G = B(Λ (m) ).

Lemma 4.5 ([14]). Let (X, B, µ) be a probability space and T be a measurable transformation on X satisfying µ(T -1 B) = 0 whenever B ∈ B with µ(B) = 0. If there exists a constant M > 0 such that for any B ∈ B and any n ∈ N,

1 n n-1 k=0 µ(T -k B) ≤ M µ(B),
then for any real integrable function f on X, the limit

lim n→∞ 1 n n-1 k=0 f (T k x)
exists for µ-almost every x ∈ X.

Lemma 4.6. Let m ≥ 3 be an integer and p ∈ (0, 1). For any B ∈ B(Λ (m) ) satisfying σ -1 B = B, we have µ p (B) = 0 or 1.

Proof. Let α = p 2 (1 -p) 2 > 0.
(1) Let w ∈ Λ (m), * and n = |w|. For any A ∈ B(Λ (m) ), we prove

αµ p [w]µ p (A) ≤ µ p ([w] ∩ σ -(n+2) A). 1 For any v ∈ Λ (m), * , prove αµ p [w]µ p [v] ≤ µ p ([w] ∩ σ -(n+2) [v]).
In fact, it follows from

ww n v 1 v ∈ Λ (m), * and [w] ∩ σ -(n+2) [v] ⊃ [ww n v 1 v] that µ p ([w] ∩ σ -(n+2) [v]) ≥ µ p [ww n v 1 v] ( ) ≥ µ p [w]µ p [w n ]µ p [v 1 ]µ p [v] ≥ (p(1 -p)) 2 µ p [w]µ p [v]
where ( ) follows from Lemma 4.3.

2 Let C := [v] : v ∈ Λ (m), * ∪ ∅ and G w := A ∈ B(Λ (m) ) : αµ p [w]µ p (A) ≤ µ p ([w] ∩ σ -(n+2) A) .
Then G w is a monotone class. Since in 1 we have already proved C ⊂ G w , in the same way as the end of the proof of Lemma 4.4, we get G w = B(Λ (m) ).

(2) We use B c to denote the complement of B in Λ (m) . For any ε > 0, by Lemma 2.4, there exist finitely many disjoint cylinders [w (i) ] ⊂ C such that µ p (B c ∆E ε ) < ε where

E ε = i [w (i) ]. (3) Let B ∈ B(Λ (m) ) with σ -1 B = B. For any w ∈ Λ (m), * , by B = σ -(|w|+2) B and (1) we get αµ p (B)µ p [w] ≤ µ(σ -(|w|+2) B ∩ [w]) = µ p (B ∩ [w]).
Thus

αµ p (B)µ p (E ε ) = i αµ p (B)µ p [w (i) ] ≤ i µ p (B ∩ [w (i) ]) = µ p (B ∩ i [w (i) ]) = µ p (B ∩ E ε ). Let a = µ p ((B ∪ E ε ) c ), b = µ p (B ∩ E ε ), c = µ p (B \ E ε ) and d = µ p (E ε \ B).
Then we already have

α(b + c)(b + d) ≤ b, a + b < ε (by µ p (B c ∆E ε ) < ε) and a + b + c + d = 1. It follows from α(b + c)(a + d -ε) ≤ α(b + c)(b + d) ≤ b < ε that (b + c)(a + d) < ( 1 α + b + c)ε ≤ ( 1 α + 1)ε. This implies µ p (B)µ p (B c ) ≤ ( 1 α + 1)ε for any ε > 0. Therefore µ p (B)(1 -µ p (B)) = 0 and then µ p (B) = 0 or 1.
Proof of Theorem 4.2. (1) For any n ∈ N and B ∈ B(Λ (m) ), define

λ n p (B) := 1 n n-1 k=0 µ p (σ -k B).
Then λ n p is a probability measure on (Λ (m) , B(Λ (m) )). By Lemma 4.4, there exists c > 0 such that

c -1 µ p (B) ≤ λ n p (B) ≤ cµ p (B) for any B ∈ B(Λ (m) ) and n ∈ N. (4.1)
(2) For any B ∈ B(Λ (m) ), prove that lim n→∞ λ n p (B) exists.

Let 1 B : Λ (m) → {0, 1} be defined by

1 B (w) := 1 if w ∈ B 0 if w / ∈ B
for any w ∈ Λ (m) . Then

lim n→∞ λ n p (B) = lim n→∞ 1 n n-1 k=0 ˆ1σ -k B dµ p = lim n→∞ ˆ1 n n-1 k=0 1 B (σ k w) dµ p (w) = ˆlim n→∞ 1 n n-1 k=0 1 B (σ k w) dµ p (w)
where the last equality is an application of the dominated convergence theorem, in which the µ p -a.e. (almost every) existence of lim n→∞ By the well known Vitali-Hahn-Saks Theorem, λ p is a probability measure on (Λ (m) , B(Λ (m) )).

1 n n-1 k=0 1 B (σ k w)
(4) The fact λ p ∼ µ p on B(Λ (m) ) follows from (4.1) and the definition of λ p .

(5) Prove that λ p is σ-invariant.

In fact, for any B ∈ B(Λ (m) ) and n ∈ N, we have

λ n p (σ -1 B) = 1 n n k=1 µ p (σ -k B) = 1 n n k=0 µ p (σ -k B) - µ p (B) n = n + 1 n λ n+1 p (B) - µ p (B) n .
Let n → ∞, we get λ p (σ Since λ p ∼ µ p ∼ λ p , there exists w ∈ Λ (m) such that λ p (B) = lim n→∞

-1 B) = λ p (B). (6)
1 n n-1 k=0 1 B (σ k w) = λ p (B)
. It means that λ p and λ p are the same on B(Λ (m) ).

PROOF OF THE MAIN RESULT

For any a ∈ [0, 1], recall the definition of the global frequency sets G a , G a and G a from the introduction. The following lemma follows immediately from (1.1), [START_REF] Li | Random walks associated to beta-shifts[END_REF]Theorem 6.1] and the invariance of Hausdorff dimension under the projection π 2 . (See also [START_REF] Fan | A multifractal mass transference principle for Gibbs measures with applications to dynamical Diophantine approximation[END_REF]Theorem 3.3].) Lemma 5.1. For any a ∈ [0, 1], we have

dim H (G a , d 2 ) = dim H (G a , d 2 ) = dim H (G a , d 2 ) = -a log a -(1 -a) log(1 -a) log 2 .
To prove Theorem 1.1, we also need the next two lemmas, which will be proved later.

Lemma 5.2. Let m ≥ 3 be an integer, p ∈ (0, 1) and λ p be the measure on (Λ (m) , B(Λ (m) )) defined in Theorem 4.2. Then

λ p [0] = p -p m 1 -p m -(1 -p) m .
For any integer m ≥ 3, we recall

Λ (m) = w ∈ {0, 1} N : w does not contain 0 m or 1 m and Λ (m) a = Λ (m) ∩ G a for a ∈ [0, 1].
Lemma 5.3. Let a ∈ (0, 1) and integer m ≥ 3 be large enough such that 1 m < a < 1 -1 m . Define f m : (0, 1) → R by f m (x) :=

x -x m 1 -x m -(1 -x) m for x ∈ (0, 1). Then there exists q m ∈ (0, 1) such that f m (q m ) = a and dim H (Λ (m) a , d 2 ) ≥ -(ma -1) log q m -(m -ma -1) log(1 -q m ) (m -1) log 2 .

Moreover, q m → a as m → ∞.

Proof of Theorem 1.1. First we prove [START_REF] Allouche | Periodic unique beta-expansions: the Sharkovskiȋ ordering[END_REF]. Let a ∈ [0, 1]. Since it is straightforward to check Γ ⊂ Λ, we have

Γ a ⊂ Λ a ⊂ G a , Γ a ⊂ Γ a ⊂ Λ a ⊂ G a and Γ a ⊂ Γ a ⊂ Λ a ⊂ G a .
By Lemma 5.1, we only need to prove

dim H (Γ a , d 2 ) ≥ -a log a -(1 -a) log(1 -a) log 2 . ( 5.1)
If a = 0 or 1, this follows immediately from 0 log 0 := 0 and 1 log 1 = 0. So we only need to consider 0 < a < 1 in the following. For any integer m ≥ 3, we define

Θ (m) a := w ∈ G a : w 1 • • • w 2m = 1 2m , w km+1 • • • w km+m / ∈ {0 m , 1 m } for all k ≥ 2 and Ξ (m) a := w ∈ G a : w km+1 • • • w km+m / ∈ {0 m , 1 m } for all k ≥ 0 . Then dim H (Γ a , d 2 ) ( ) ≥ dim H (Θ (m) a , d 2 ) ( ) ≥ dim H (Ξ (m) a , d 2 ) ( ) ≥ dim H (Λ (m) a , d 2 ) (5.2)
where ( ) follows from Γ a ⊃ Θ and the fact that σ 2m is Lipschitz continuous (since d 2 (σ 2m (w), σ 2m (v)) ≤ 2 2m d 2 (w, v) for all w, v ∈ {0, 1} N ). By (5.2) and Lemma 5.3, for m large enough, there exists q m ∈ (0, 1) such that q m → a (as m → ∞) and

dim H (Γ a , d 2 ) ≥ -(ma -1) log q m -(m -ma -1) log(1 -q m ) (m -1) log 2 .
Let m → ∞, we get (5.1). Finally we deduce (1) from (2). In fact, since (2) implies dim H (Γ1

2 , d 2 ) = 1, it follows from Γ1 2 ⊂ Γ ⊂ Λ ⊂ {0, 1} N that dim H (Γ, d 2 ) = dim H (Λ, d 2 ) = 1.
Finally we prove Lemmas 5.2 and 5.3 to end this paper.

Proof of Lemma 5.3. Since f m is continuous on (0, 1), lim x→0 + f m (x) = 1 m , lim x→1 -f m (x) = 1 -1 m and 1 m < a < 1 -1 m , there exists q m ∈ (0, 1) such that f m (q m ) = a. (1) Prove q m → a as m → ∞. Notice that |q m -a| = |q m -f m (q m )| = q m m (1 -q m ) -q m (1 -q m ) m 1 -q m m -(1 -q m ) m . Let g m (x) := x m (1 -x) -x(1 -x) m 1 -x m -(1 -x) m for x ∈ (0, 1). Then |q m -a| = |g m (q m )| ≤ sup x∈(0,1) |g m (x)|.
In order to prove q m → a, it suffices to check |g m (x)| ≤ 1 m for all x ∈ (0, 1). That is, m

• |x m (1 -x) -x(1 -x) m | ≤ 1 -x m -(1 -x) m for all x ∈ (0, 1). 1 When x ∈ (0, 1 2 ], we get x m (1 -x) -x(1 -x) m ≤ 0. It suffices to prove (m -mx - 1)x m + 1 -(mx + 1)(1 -x) m ≥ 0. Since m -mx -1 > 0, we only need to prove h m (x) := (mx + 1)(1 -x) m ≤ 1 for all x ∈ [0, 1 2 ]. This follows from h m (0) = 1 and h m (x) = -m(m + 1)x(1 -x) m-1 ≤ 0 for all x ∈ [0, 1 2 ]. 2 When x ∈ ( 1 2 , 1), we get x m (1 -x) -x(1 -x) m ≥ 0. It suffices to prove (mx - 1)(1 -x) m + 1 -(1 + m -mx)x m ≥ 0. Since mx -1 > 0, we only need to prove h m (x) := (1 + m -mx)x m ≤ 1 for all x ∈ [ 1 2 , 1]. This follows from h m (1) = 1 and h m (x) = m(m + 1)(1 -x)x m-1 ≥ 0 for all x ∈ [ 1 2 , 1]. (2
) We apply Proposition 2.6 to get the lower bound of dim H (Λ (m) a , d 2 ). Let µ qm be the (q m , 1 -q m ) Bernoulli-type measure on (Λ (m) , B(Λ (m) )) defined in Section 4. 1 The fact that Λ For any integer k ≥ 0, let

(m) a = Λ (m) ∩ G a is a Borel set in (Λ (m) , d 2 ) follows from the fact that G a is a Borel set in ({0, 1} N , d 2 ).
a k := µ p σ -k [0] = u 1 •••u k 0∈Λ (m), * µ p [u 1 • • • u k 0], b k := µ p σ -k [1] = u 1 •••u k 1∈Λ (m), * µ p [u 1 • • • u k 1], c k := µ p σ -k [01] = u 1 •••u k 01∈Λ (m), * µ p [u 1 • • • u k 01], d k := µ p σ -k [10] = u 1 •••u k 10∈Λ (m), * µ p [u 1 • • • u k 10].
By Theorem 4.2, the following limits exist: a := lim

  1} N : w does not contain 0 m or 1 m , and define Λ (m), * := w ∈ {0, 1} * : w does not contain 0 m or 1 m and Λ (m),n := w ∈ {0, 1} n : w does not contain 0 m or 1 m

Definition 3 . 1 (

 31 Digit occurrence parameters). Let m ≥ 3 be an integer. For any w ∈ Λ (m), * , defineN (m) 0 (w) := k : 1 ≤ k ≤ |w|, w k = 0 and w 1 . . . w k-1 1 ∈ Λ (m), * , N(m) 1 (w):= k : 1 ≤ k ≤ |w|, w k = 1 and w 1 . . . w k-1 0 ∈ Λ (m), * ,

  0 and then the conclusion follows immediately from N (m) 0 (w) ≤ N (m) 0 (wv). Thus it suffices to consider v = 1 b in the following. Let s ∈ {1, • • • , b} be the smallest such that v 1 = • • • = v s-1 = 1 and v s = 0. In order to get the conclusion, it suffices to show N , we only need to prove (a + N ∪ {a + s}. Let k ∈ N (m) 0 (v) \ {s}. It suffices to check a + k ∈ N (m) 0

Proposition 3 . 3 .

 33 Let m ≥ 3 be an integer and w ∈ Λ (m), * . Then(1) m • |w| 0 ≤ (m -1)N (m) 0 (w) + |w|; (2) m • |w| 1 ≤ (m -1)N (m) 1 (w) + |w|.Proof. (1) Let n = |w|. If n ≤ m -1, the conclusion follows immediately from N (m) 0 (w) = |w| 0 . In the following, we assume n ≥ m. Recall N (m) 0

  which contradicts the definition of Λ (m), * . Combining 1 and 2 , we get |w| 0 = N (m) 0 (w)+N (m) 1 m-1 0 (w). It follows from (m-1)N (m) 1 m-1 0 (w) ≤ |w| 1 = |w|-|w| 0 that (m-1)(|w| 0 -N (m) 0 (w)) ≤ |w|-|w| 0 , i.e., m•|w| 0 ≤ (m-1)N (m) 0 (w)+|w|.

µ

  p [w0] := pµ p [w] and µ p [w1] := (1 -p)µ p [w]; if w0 ∈ Λ (m),n+1 but w1 / ∈ Λ (m),n+1 , then [w1] = ∅, [w0] = [w] and naturally we have µ p [w0] = µ p [w]; if w1 ∈ Λ (m),n+1 but w0 / ∈ Λ (m),n+1 , then [w0] = ∅, [w1] = [w] and naturally we have µ p [w1] = µ p [w].

  follows from Lemma 4.5, Lemma 4.4 and (4.1). (3) For any B ∈ B(Λ (m) ), define λ p (B) := lim n→∞ λ n p (B).

1 n n- 1 k=0 1 Bn n- 1 k=0 1 B

 11111 Prove that (Λ(m) , B(Λ (m) ), λ p , σ) is ergodic. In fact, for any B ∈ B(Λ (m) ) satisfying σ -1 B = B, by Lemma 4.6 we get µ p (B) = 0 or 1, which implies λ p (B) = 0 or 1 since λ p ∼ µ p .[START_REF] Wang | Distribution of full cylinders and the Diophantine properties of the orbits in β-expansions[END_REF] Prove that such λ p is unique on B(Λ (m) ). Let λ p be a σ-invariant ergodic probability measure on (Λ (m) , B(Λ (m) )) equivalent to µ p . Then for any B ∈ B(Λ (m) ), by the Birkhoff Ergodic Theorem, we get λ p (B) = ˆ1B dλ p = lim n→∞ (σ k w) for λ p -a.e. w ∈ Λ (m) and λ p (B) = ˆ1B dλ p = lim n→∞ 1 (σ k w) for λ p -a.e. w ∈ Λ (m) .

2 1 n n- 1 k=0 1 (w 1

 21111 Prove µ qm (Λ (m) a ) = 1.Let λ qm be the measure defined in Theorem 4.2 such that (Λ(m) , B(Λ (m) ), λ qm , σ) is ergodic. It follows from the Birkhoff Ergodic Theorem thatlim n→∞ 1 n n-1 k=0 1 [0] (σ k w) = ˆ1[0] dλ qm = λ qm [0] by ======= Lemma 5.2 q m -q m m 1 -q m m -(1 -q m ) m = f m (q m ) = a for λ qm -almost every w ∈ Λ (m) . By |w 1 •••wn| 0 n = [0] (σ k w), we get lim n→∞ |w 1 • • • w n | 0 n = a for λ qm -almost every w ∈ Λ (m) , which implies λ qm (Λ (m) a ) = 1. It follows from λ qm ∼ µ qm that µ qm (Λ •••wn) n (-log q m ) + lim n→∞ N (m) 1 (w 1 •••wn) n (-log(1 -q m )) log 2 ( ) ≥ lim n→∞ m•|w 1 •••wn| 0 (m-1)n -1 m-1 (-log q m ) + lim n→∞ m•|w 1 •••wn| 1 (m-1)n -1 m-1 (-log(1 -q m )) log 2 ( ) = -(ma -1) log q m -(m -ma -1) log(1 -q m ) (m -1) log 2where ( )follows from w ∈ Λ (m)a , ( ) follows from Proposition 3.3 and ( ) can be proved as follows. For any r ∈ (0, 1), there exists n = n(r) ∈ N such that 1 2 n ≤ r < 1 2 n-1 . Then by B(w, r) = [w 1 • • • w n ] and log µ qm [w 1 • • • w n ] < 0, we get log µq m (B(w,r)) log r ≥ log µq m [w 1 •••wn] log 2 -n . (In fact, ( ) can take "=".) Thus the lower bound of dim H (Λ (m) a , d 2 ) follows from 1 , 2 , 3 and Proposition 2.6. Proof of Lemma 5.2. By the definition of λ p , we know λ p [0] = lim n→∞ 1 n n-1 k=0 µ p σ -k [0].

c

  k = λ p [01], d := lim n→∞ 1 n n-1 k=0 d k = λ p [10].

( 1 )

 1 We have a + b = 1 since λ p [0] + λ p [1] = λ p (Λ (m) ). (2) We have c = d since λ p [00] + λ p [01] = λ p [0] = λ p σ -1 [0] = λ p [00] + λ p[START_REF] Daróczy | On the structure of univoque numbers[END_REF].

Acknowledgement. The author is grateful to Professor Jean-Paul Allouche for his advices on a former version of this paper, and also grateful to the Oversea Study Program of Guangzhou Elite Project (GEP) for financial support (JY201815).

Proof. Let c = p -2 (1 -p) -2 > 1.

(1) Prove c -1 µ p [w] ≤ σ k µ p [w] ≤ cµ p [w] for any k ∈ N and w ∈ Λ (m), * . Fix w ∈ Λ (m), * and k ∈ N. Note that

is a disjoint union. 1 Estimate the upper bound of σ k µ p [w]:

where ( ) follows from Lemma 4.3.

2 Estimate the lower bound of σ k µ p [w]: 2 . In fact, when k = 1, the conclusion is obvious. When k ≥ 2, we have

where ( ) follows from

and ( ) follows from Lemma 4.3. In the same way, we can get

where ( ), ( ) and ( ) follow from

and

respectively, recalling the definition of µ p . 2 For k ≥ m, we have

where ( ), ( ) and ( ) follow from

, * respectively, recalling the definition of µ p .

Combining