text: 22 K. ASADA, N. KOBAYASHI, R. SIN’YA, AND T. TSUKADA Hence we have (cid:48) (cid:48) (cid:48)(cid:48) Φ (U[E](cid:74)P (cid:75)) = Φ (U [E ](cid:74)P (cid:75)) m m 0 j (cid:48) (cid:48) (cid:48) (cid:48) (cid:48) (cid:48) (cid:48)(cid:48) = Φ (a (T , . . . , T (cid:48)− , U (cid:48), T (cid:48) , . . . , T (cid:48) )[E ](cid:74)P (cid:75)) m 1 j 1 j j +1 Σ(a ) j (cid:48) (cid:48) (cid:48) (cid:48) (cid:48)(cid:48) (cid:48) (cid:48) = Φ (a (T , . . . , T (cid:48)− , U (cid:48)[E ](cid:74)P (cid:75), T (cid:48) , . . . , T (cid:48) )) m 1 j 1 j j j +1 Σ(a ) (cid:48) (cid:48)(cid:48) = ([ ], (cid:74) (cid:75)n[E ], U · P ) 1 j 0 (cid:48) = (U, E, P ) • The third case of Equation (3.2): We have |T | = |U [E ]| ≥ m for a unique j ∈ j j j {1, . . . , Σ(a)} (and thus |T | < m for every i (cid:54)= j) and: i U = a(T , . . . , T − , U , T , . . . , T ) |U| < m E = E P = P . 1 j 1 j j+1 Σ(a) j j By the induction hypothesis, (cid:48) (cid:48) Φ (U [E ](cid:74)P (cid:75)) = (U , E , P ). m j j j j Since |T | < m for every i (cid:54)= j and |a(T , . . . , T − , U , T , . . . , T )| < m, we have i 1 j 1 j j+1 Σ(a) (cid:48) (cid:48) Φ (U[E](cid:74)P (cid:75)) = Φ (a(T , . . . , T − , U [E ](cid:74)P (cid:75), T , . . . , T )) m m 1 j 1 j j j+1 Σ(a) (cid:48) = (a(T , . . . , T − , U , T , . . . , T ), E , P ) 1 j 1 j j+1 Σ(a) j (cid:48) = (U, E, P ) • The fourth case of Equation (3.2): Let n be |T |; we have n ≥ m and: U = [ ] E = (cid:74) (cid:75)n P = T. 0 (cid:48) (cid:48) (cid:48) (cid:48) (cid:48) (cid:48) Since P : E, P must be a singleton sequence consisting of a tree, say T = a (T , . . . , T (cid:48) ). (cid:48) (cid:48) (cid:48) 1 Σ(a ) By the assumption, T is good for m. Hence |T | ≥ m and |T | < m for every i = (cid:48) i 1, . . . , Σ(a ). So (cid:48) (cid:48) (cid:48) (cid:48) Φ (U[E](cid:74)P (cid:75)) = Φ (T ) = ([ ], (cid:74) (cid:75)n, T ) = (U, E, P ). m m 0 (cid:81) • • (cid:48) (cid:48) (cid:48) Corollary 3.13. If (E, P ) = Φ (T ), then Φ (E(cid:74)P (cid:75)) = (E, P ) for any P ∈ shn(E) Um(cid:5) . m m i=1 E i (cid:81) (cid:81) • (cid:48) (cid:48) (cid:48) Proof. If (E, P ) = Φ (T ), then (U, E , P ) = Φ (T ) and U[E ] = E for some U, E . m (cid:48) m (cid:48) (cid:48) (cid:48) Since shn(E) Um(cid:5) = shn(E ) Um(cid:48)(cid:5) , Lemma 3.12 implies Φ (E(cid:74)P (cid:75)) = Φ (U[E ](cid:74)P (cid:75)) = (cid:48) i(cid:48)=1 E i i=1 • E i (cid:48) (cid:48) (cid:48) m(cid:48) m (U, E , P ). Thus, we have Φ (E(cid:74)P (cid:75)) = (U[E ], P ) = (E, P ) as required. m ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine##

text: K.

text: ASADA,

text: N.

text: KOBAYASHI,

text: R.

text: SIN’YA,

text: AND

text: T.

text: TSUKADA

text: Hence

text: we

text: have

text: Φ

text: Φ

text: (U

text: [E

text: m

text: m

text: j

text: Φ

text: (a

text: (T

text: T

text: U

text: T

text: T

text: )[E

text: m

text: j

text: j

text: j

text: Σ(a

text: j

text: Φ

text: (a

text: (T

text: T

text: U

text: T

text: T

text: m

text: j

text: j

text: j

text: j

text: Σ(a

text: U

text: P

text: j

text: (U,

text: E,

text: P

text: The

text: third

text: case

text: of

text: Equation

text: We

text: have

text: |T

text: |U

text: [E

text: m

text: for

text: a

text: unique

text: j

text: j

text: j

text: j

text: Σ(a)}

text: (and

text: thus

text: |T

text: m

text: for

text: every

text: i

text: j)

text: and:

text: i

text: U

text: a(T

text: T

text: U

text: T

text: T

text: |U|

text: m

text: E

text: E

text: P

text: P

text: j

text: j

text: Σ(a)

text: j

text: j

text: By

text: the

text: induction

text: hypothesis,

text: Φ

text: (U

text: [E

text: (U

text: E

text: P

text: m

text: j

text: j

text: j

text: j

text: Since

text: |T

text: m

text: for

text: every

text: i

text: j

text: and

text: |a(T

text: T

text: U

text: T

text: T

text: m,

text: we

text: have

text: i

text: j

text: j

text: Σ(a)

text: Φ

text: Φ

text: (a(T

text: T

text: U

text: [E

text: T

text: T

text: m

text: m

text: j

text: j

text: j

text: Σ(a)

text: (a(T

text: T

text: U

text: T

text: T

text: E

text: P

text: j

text: j

text: Σ(a)

text: j

text: (U,

text: E,

text: P

text: The

text: fourth

text: case

text: of

text: Equation

text: Let

text: n

text: be

text: |T

text: we

text: have

text: n

text: m

text: and:

text: U

text: E

text: P

text: T.

text: Since

text: P

text: E,

text: P

text: must

text: be

text: a

text: singleton

text: sequence

text: consisting

text: of

text: a

text: tree,

text: say

text: T

text: a

text: (T

text: T

text: Σ(a

text: By

text: the

text: assumption,

text: T

text: is

text: good

text: for

text: m.

text: Hence

text: |T

text: m

text: and

text: |T

text: m

text: for

text: every

text: i

text: i

text: Σ(a

text: So

text: Φ

text: Φ

text: (T

text: T

text: (U,

text: E,

text: P

text: m

text: m

text: Corollary

text: If

text: (E,

text: P

text: Φ

text: (T

text: then

text: Φ

text: (E,

text: P

text: for

text: any

text: P

text: shn(E)

text: m

text: m

text: E

text: i

text: Proof.

text: If

text: (E,

text: P

text: Φ

text: (T

text: then

text: (U,

text: E

text: P

text: Φ

text: (T

text: and

text: U[E

text: E

text: for

text: some

text: U,

text: E

text: m

text: m

text: Since

text: shn(E)

text: shn(E

text: Lemma

text: implies

text: Φ

text: Φ

text: (U[E

text: E

text: i

text: E

text: i

text: m

text: (U,

text: E

text: P

text: Thus,

text: we

text: have

text: Φ

text: (U[E

text: P

text: (E,

text: P

text: as

text: required.

text: m

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##


text: ALMOST EVERY SIMPLY TYPED λ-TERM HAS A LONG β-REDUCTION SEQUENCE 35 (cid:48) (2) The converse of (1) holds for suﬃciently large n: for any N, N ∈ N inf and n ≥ n , if (cid:48) 0 n ≡ d (cid:48) mod c then L (G, N⇒N ) (cid:54)= ∅. N,N n (3) d = 0 for every N ∈ N inf. N,N (cid:48) (cid:48)(cid:48) (4) d (cid:48) + d (cid:48) (cid:48)(cid:48) ≡ d (cid:48)(cid:48) mod c for every N, N , N ∈ N inf. N,N N ,N N,N (cid:48) Proof. Let c be the basic period of G. We ﬁrst deﬁne d (cid:48) for each N, N ∈ N inf. Since (cid:48) N,N (cid:48) L(G, N⇒N ) is inﬁnite (Lemma 3.34(1)), there exists U (cid:48) ∈ L(G, N⇒N ). Let d (cid:48) be N,N N,N the unique natural number 0 ≤ d (cid:48) < c such that |U (cid:48)| ≡ d (cid:48) mod c. This deﬁnition N,N N,N N,N of d (cid:48) does not depend on the choice of U (cid:48), by Lemma 3.34(5). N,N (cid:48) N,N (cid:48) W(cid:48) e deﬁne n0. For every N, N ∈(cid:0)N inf, sinc(cid:1)e c is a period o(cid:0)f L(G, N⇒(cid:1)N ), there exists N,N n such that: 0 N,N(cid:48) N (cid:48) (cid:48) ∀n ≥ n . ∀k ∈ . L G, N⇒N (cid:54)= ∅ ⇔ L G, N⇒N (cid:54)= ∅. 0 n n+ck (cid:44) (cid:48) (cid:48) Let n max{nN,N | N, N ∈ N inf}. 0 0 Then: • (1) follows from Lemma 3.34(5). (cid:48) • (2) follows from the deﬁnition of n , inﬁnity of L(G, N⇒N ) (Lemma 3.34(1)), and 0 (cid:48) Lemma 3.34(5) (given n ≥ n , pick U ∈ L(G, N⇒N ) such that |U| ≥ n; then |U| = n+ck 0 for some k ≥ 0). • (3) follows from Lemma 3.34(3). (cid:48)(cid:48) • (4) follows from U (cid:48) (cid:48)(cid:48)[U (cid:48)] ∈ L(G, N⇒N ) and Lemma 3.34(5). N ,N N,N Now we are ready to prove key lemmas. First, for every S ∈ Sinf(G), we can transform a given context into U (cid:23) S without changing its type and size, provided that the size of the given context (= |U|) is suﬃciently large (Lemma 3.36). Furthermore we can assume that the transformation preserves the property “good for m” (Lemma 3.37). Lemma 3.36. Let G = (Σ, N , R) be a regular tree grammar in canonical form. Assume that G is unambiguous and essentially strongly-connected and #(L(G)) = ∞. Then there N exists a constant n ∈ that satisﬁes the following condition: For every 0 • S ∈ Sinf(G), • n ≥ n + |S|, and 0 (cid:48) (cid:48) (cid:48) • κ = (⇒N ) or (N⇒N ) where N, N ∈ N inf, if L (G, κ) (cid:54)= ∅, then there exists U ∈ L (G, κ) with S (cid:22) U. n n Proof. First, let us choose the following constants: N (cid:48) (cid:48) • m ∈ such that, for every N, N ∈ N inf, there exists S (cid:48) ∈ L(G, N⇒N ) with 0 N,N |S (cid:48)| ≤ m . The existence of m is a consequence of essential strong-connectivity and N,N 0 0 of ﬁniteness of N . (cid:83) • m which is the constant n of Lemma 3.35. 1 0 N • m ∈ such that, for every N ∈ N \N inf and every T ∈ L(G, N), we have |T | < m . The 2 2 existence of m follows from the fact that ∈N\N L(G, N) is a ﬁnite set. 2 N inf ##LTLine## ##LTLine## ##LTLine## ##LTLine##

text: ALMOST

label: paragraph

text: EVERY

text: SIMPLY

text: TYPED

text: λ-TERM

text: HAS

text: A

text: LONG

text: β-REDUCTION

text: SEQUENCE

label: list

text: The

text: converse

text: of

text: holds

text: for

text: suﬃciently

text: large

text: n:

text: for

text: any

text: N,

text: N

text: N

text: inf

text: and

text: n

text: n

text: if

text: n

text: d

text: mod

text: c

text: then

text: L

text: (G,

text: N⇒N

text: N,N

text: n

text: d

text: for

text: every

text: N

text: N

text: inf.

text: N,N

text: d

text: d

text: d

text: mod

text: c

text: for

text: every

text: N,

text: N

text: N

text: N

text: inf.

text: N,N

text: N

text: ,N

text: N,N

text: Proof.

text: Let

text: c

text: be

text: the

text: basic

text: period

text: of

text: G.

text: We

text: ﬁrst

text: deﬁne

text: d

text: for

text: each

text: N,

text: N

text: N

text: inf.

text: Since

text: N,N

text: L(G,

text: N⇒N

text: is

text: inﬁnite

text: (Lemma

text: there

text: exists

text: U

text: L(G,

text: N⇒N

text: Let

text: d

text: be

text: N,N

text: N,N

text: the

text: unique

text: natural

text: number

text: d

text: c

text: such

text: that

text: |U

text: d

text: mod

text: c.

text: This

text: deﬁnition

text: N,N

text: N,N

text: N,N

text: of

text: d

text: does

text: not

text: depend

text: on

text: the

text: choice

text: of

text: U

text: by

text: Lemma

text: N,N

text: N,N

text: e

text: deﬁne

text: For

text: every

text: N,

text: N

text: inf,

text: c

text: is

text: a

text: period

text: L(G,

text: there

text: exists

text: N,N

text: n

text: such

text: that:

text: N

text: ∀n

text: n

text: ∀k

text: L

text: G,

text: N⇒N

text: L

text: G,

text: N⇒N

text: n

text: n+ck

text: Let

text: n

text: max{nN,N

text: N,

text: N

text: N

text: inf}.

text: Then:

text: follows

text: from

text: Lemma

text: follows

text: from

text: the

text: deﬁnition

text: of

text: n

text: inﬁnity

text: of

text: L(G,

text: N⇒N

text: (Lemma

text: and

text: Lemma

text: (given

text: n

text: n

text: pick

text: U

text: L(G,

text: N⇒N

text: such

text: that

text: |U|

text: n;

text: then

text: |U|

text: n+ck

text: for

text: some

text: k

text: follows

text: from

text: Lemma

text: follows

text: from

text: U

text: L(G,

text: N⇒N

text: and

text: Lemma

text: N

text: ,N

text: N,N

text: Now

text: we

text: are

text: ready

text: to

text: prove

text: key

text: lemmas.

text: First,

text: for

text: every

text: S

text: Sinf(G),

text: we

text: can

text: transform

text: a

text: given

text: context

text: into

text: U

text: S

text: without

text: changing

text: its

text: type

text: and

text: size,

text: provided

text: that

text: the

text: size

text: of

text: the

text: given

text: context

text: |U|)

text: is

text: suﬃciently

text: large

text: (Lemma

text: Furthermore

text: we

text: can

text: assume

text: that

text: the

text: transformation

text: preserves

text: the

text: property

text: “good

text: for

text: m”

text: (Lemma

text: Lemma

text: Let

text: G

text: (Σ,

text: N

text: R)

text: be

text: a

text: regular

text: tree

text: grammar

text: in

text: canonical

text: form.

text: Assume

text: that

text: G

text: is

text: unambiguous

text: and

text: essentially

text: strongly-connected

text: and

text: #(L(G))

text: Then

text: there

text: N

text: exists

text: a

text: constant

text: n

text: that

text: satisﬁes

text: the

text: following

text: condition:

text: For

text: every

text: S

text: Sinf(G),

text: n

text: n

text: |S|,

text: and

text: κ

text: (⇒N

text: or

text: (N⇒N

text: where

text: N,

text: N

text: N

text: inf,

text: if

text: L

text: (G,

text: κ)

text: then

text: there

text: exists

text: U

text: L

text: (G,

text: κ)

text: with

text: S

text: U.

text: n

text: n

text: Proof.

text: First,

text: let

text: us

text: choose

text: the

text: following

text: constants:

text: N

text: m

text: such

text: that,

text: for

text: every

text: N,

text: N

text: N

text: inf,

text: there

text: exists

text: S

text: L(G,

text: N⇒N

text: with

text: N,N

text: |S

text: m

text: The

text: existence

text: of

text: m

text: is

text: a

text: consequence

text: of

text: essential

text: strong-connectivity

text: and

text: N,N

text: of

text: ﬁniteness

text: of

text: N

text: m

text: which

text: is

text: the

text: constant

text: n

text: of

text: Lemma

text: N

text: m

text: such

text: that,

text: for

text: every

text: N

text: N

text: \N

text: inf

text: and

text: every

text: T

text: L(G,

text: N),

text: we

text: have

text: |T

text: m

text: The

text: existence

text: of

text: m

text: follows

text: from

text: the

text: fact

text: that

text: ∈N\N

text: L(G,

text: N)

text: is

text: a

text: ﬁnite

text: set.

text: N

text: inf

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##


text: ALMOST EVERY SIMPLY TYPED λ-TERM HAS A LONG β-REDUCTION SEQUENCE 5 where n ≥ 0. For a (cid:104)Γ; τ(cid:105)-term t, we deﬁne the order and internal arity of Γ (cid:96) t : τ written ord(Γ (cid:96) t : τ) and iar(Γ (cid:96) t : τ) by: (cid:44) (cid:48) (cid:48) (cid:48) (cid:48) ord(Γ (cid:96) t : τ) max{ord(τ ) | (Γ (cid:96) t : τ ) occurs in ∆} (cid:44) (cid:48) (cid:48) (cid:48) (cid:48) iar(Γ (cid:96) t : τ) max{iar(τ ) | (Γ (cid:96) t : τ ) occurs in ∆} where ∆ is the (unique) derivation tree for Γ (cid:96) t : τ. Note that the notions of size, order, internal arity, and β(t) (the maximum length of β-reduction sequences of t, as deﬁned in Section ) are well-deﬁned with respect to α-equivalence. (cid:44) − − Example 2.2. Recall the term 2 λfτ(j 1).λxτ(j 2).f(f x) (with τ(j) being the order-j j − − type deﬁned by: τ(0) = o and τ(j) = τ(j 1) → τ(j 1)) in Section . For t = 23 22 (λxo.x) y, we have ord(y:o (cid:96) t : o) = iar(y:o (cid:96) t : o) = 3. Note that the derivation for y:o (cid:96) t : o contains the type judgment ∅ (cid:96) 23 : τ(3), where τ(3) = ((o → o) → (o → o)) → (o → o) → o → o, and ord(τ(3)) = iar(τ(3)) = 3. We now deﬁne the set Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) of (α-equivalence classes of) (cid:104)Γ; τ(cid:105)-terms of size n n, whose order, internal arity, and the number of variables are bounded above by δ, ι and ξ respectively. Deﬁnition 2.3 (terms with bounds on types and variables). Let δ, ι, ξ ≥ 0 and n ≥ 1 be (cid:0) (cid:1) integers. We denote by Types(δ, ι) the set of types {τ | ord(τ) ≤ δ, iar(τ) ≤ ι}. For each Γ and τ, Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) and Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) are deﬁned by: n (cid:44) (cid:48) Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) {[t]α | Γ (cid:96) t : τ, ord(Γ (cid:96) t : τ) ≤ δ, iar(Γ (cid:96) t : τ) ≤ ι, (cid:48)m∈in# V(t ) ≤ ξ} t [t]α (cid:44) Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) {(cid:93)[t] ∈ Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) | |t| = n}. n α We also deﬁne: (cid:44) (cid:44) Λα(δ, ι, ξ) Λα((cid:104)∅; τ(cid:105), δ, ι, ξ) Λα(δ, ι, ξ) {[t] ∈ Λα(δ, ι, ξ) | |t| = n}. n α ∈ τ Types(δ,ι) Note that in the deﬁnition of Λα((cid:104)Γ; τ(cid:105), δ, ι, ξ) above, we count the minimum number of used variables up to α-equivalence. Therefore, [λxo.λyo.λzo.x]α belongs to Λα((cid:104)∅; o → o → o → o(cid:105), 1, 3, 1), because λxo.λyo.λzo.x ∼α λxo.λ∗.λ∗.x and #(V(λxo.λ∗.λ∗.x)) = 1. We are now ready to state our main result, which is proved in Section . (cid:0) (cid:1) Theorem 2.4. For δ, ι, ξ ≥ 2 and k = min{δ, ι}, there exists a real number p > 0 such that # {[t] ∈ Λα(δ, ι, ξ) | β(t) ≥ exp − (np)} α n k 1 l→im∞ = 1. n #(Λα(δ, ι, ξ)) n The theorem above says that if the order, internal arity, and the number of used variables are bounded independently of term size, most of the simply-typed λ-terms of size n have a very long β-reduction sequence, which is as long as (k − 1)-fold exponential in n. ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine##

text: ALMOST

text: EVERY

text: SIMPLY

text: TYPED

text: λ-TERM

text: HAS

text: A

text: LONG

text: β-REDUCTION

text: SEQUENCE

text: where

text: n

text: For

text: a

text: t,

text: we

text: deﬁne

text: the

text: order

text: and

text: internal

text: arity

text: of

text: Γ

text: t

text: τ

text: written

text: ord(Γ

text: t

text: τ)

text: and

text: iar(Γ

text: t

text: τ)

text: by:

text: ord(Γ

text: t

text: τ)

text: max{ord(τ

text: (Γ

text: t

text: τ

text: occurs

text: in

text: iar(Γ

text: t

text: τ)

text: max{iar(τ

text: (Γ

text: t

text: τ

text: occurs

text: in

text: where

text: is

text: the

text: (unique)

text: derivation

text: tree

text: for

text: Γ

text: t

text: τ.

text: Note

text: that

text: the

text: notions

text: of

text: size,

text: order,

text: internal

text: arity,

text: and

text: β(t)

text: (the

text: maximum

text: length

text: of

text: β-reduction

text: sequences

text: of

text: t,

text: as

text: deﬁned

text: in

text: Section

text: are

text: well-deﬁned

text: with

text: respect

text: to

text: α-equivalence.

text: Example

text: Recall

text: the

text: term

text: λfτ(j

text: x)

text: (with

text: τ(j)

text: being

text: the

text: order-j

text: j

text: type

text: deﬁned

text: by:

text: o

text: and

text: τ(j)

text: τ(j

text: τ(j

text: in

text: Section

text: For

text: t

text: (λxo.x)

text: y,

text: we

text: have

text: ord(y:o

text: t

text: o)

text: iar(y:o

text: t

text: o)

text: Note

text: that

text: the

text: derivation

text: for

text: y:o

text: t

text: o

text: contains

text: the

text: type

text: judgment

text: where

text: ((o

text: o)

text: (o

text: o))

text: (o

text: o)

text: o

text: o,

text: and

text: We

text: now

text: deﬁne

text: the

text: set

text: δ,

text: ι,

text: ξ)

text: of

text: (α-equivalence

text: classes

text: of)

text: of

text: size

text: n

text: n,

text: whose

text: order,

text: internal

text: arity,

text: and

text: the

text: number

text: of

text: variables

text: are

text: bounded

text: above

text: by

text: δ,

text: ι

text: and

text: ξ

text: respectively.

text: Deﬁnition

text: (terms

text: with

text: bounds

text: on

text: types

text: and

text: variables).

text: Let

text: δ,

text: ι,

text: ξ

text: and

text: n

text: be

text: integers.

text: We

text: denote

text: by

text: Types(δ,

text: ι)

text: the

text: set

text: of

text: types

text: {τ

text: ord(τ)

text: δ,

text: iar(τ)

text: ι}.

text: For

text: each

text: Γ

text: and

text: τ,

text: δ,

text: ι,

text: ξ)

text: and

text: δ,

text: ι,

text: ξ)

text: are

text: deﬁned

text: by:

text: n

text: δ,

text: ι,

text: ξ)

text: {[t]α

text: Γ

text: t

text: τ,

text: ord(Γ

text: t

text: τ)

text: δ,

text: iar(Γ

text: t

text: τ)

text: ι,

text: V(t

text: ξ}

text: t

text: [t]α

text: δ,

text: ι,

text: ξ)

text: δ,

text: ι,

text: ξ)

text: |t|

text: n}.

text: n

text: α

text: We

text: also

text: deﬁne:

text: Λα(δ,

text: ι,

text: ξ)

text: δ,

text: ι,

text: ξ)

text: Λα(δ,

text: ι,

text: ξ)

text: {[t]

text: Λα(δ,

text: ι,

text: ξ)

text: |t|

text: n}.

text: n

text: α

text: τ

text: Types(δ,ι)

text: Note

text: that

text: in

text: the

text: deﬁnition

text: of

text: δ,

text: ι,

text: ξ)

text: above,

text: we

text: count

text: the

text: minimum

text: number

text: of

text: used

text: variables

text: up

text: to

text: α-equivalence.

text: Therefore,

text: [λxo.λyo.λzo.x]α

text: belongs

text: to

text: o

text: o

text: o

text: because

text: λxo.λyo.λzo.x

text: ∼α

text: λxo.λ∗.λ∗.x

text: and

text: #(V(λxo.λ∗.λ∗.x))

text: We

text: are

text: now

text: ready

text: to

text: state

text: our

text: main

text: result,

text: which

text: is

text: proved

text: in

text: Section

text: Theorem

text: For

text: δ,

text: ι,

text: ξ

text: and

text: k

text: min{δ,

text: ι},

text: there

text: exists

text: a

text: real

text: number

text: p

text: such

text: that

text: {[t]

text: Λα(δ,

text: ι,

text: ξ)

text: β(t)

text: exp

text: (np)}

text: α

text: n

text: k

text: l→im∞

text: n

text: #(Λα(δ,

text: ι,

text: ξ))

text: n

text: The

text: theorem

text: above

text: says

text: that

text: if

text: the

text: order,

text: internal

text: arity,

text: and

text: the

text: number

text: of

text: used

text: variables

text: are

text: bounded

text: independently

text: of

text: term

text: size,

text: most

text: of

text: the

text: simply-typed

text: λ-terms

text: of

text: size

text: n

text: have

text: a

text: very

text: long

text: β-reduction

text: sequence,

text: which

text: is

text: as

text: long

text: as

text: (k

text: exponential

text: in

text: n.

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##


text: 50 K. ASADA, N. KOBAYASHI, R. SIN’YA, AND T. TSUKADA 5. Related Work As mentioned in Section , there are several pieces of work on probabilistic properties of untyped λ-terms [2, 3, 4]. David et al. [2] have shown that almost all untyped λ-terms are strongly normalizing, whereas the result is opposite for terms expressed in SK combinators. Their former result implies that untyped λ-terms do not satisfy the inﬁnite monkey theorem, i.e., for any term t, the probability that a randomly chosen term of size n contains t as a subterm tends to zero. Bendkowski et al. [4] proved that almost all terms in de Brujin representation are not strongly normalizing, by regarding the size of an index i is i + 1, instead of the constant 1. The discrepancies among those results suggest that this kind of probabilistic property is quite fragile and depends on the deﬁnition of the syntax and the size of terms. Thus, the setting of our paper, especially the assumption on the boundedness of internal arities and the number of variables is a matter of debate, and it would be interesting to study how the result changes for diﬀerent assumptions. We are not aware of similar studies on typed λ-terms. In fact, in their paper about combinatorial aspects of λ-terms, Grygiel and Lescanne [3] pointed out that the combinatorial study of typed λ-terms is diﬃcult, due to the lack of (simple) recursive deﬁnition of typed terms. In the present paper, we have avoided the diﬃculty by making the assumption on the boundedness of internal arities and the number of variables (which is, as mentioned above, subject to a debate though). In a larger context, our work may be viewed as an instance of the studies of average-case complexity [23, Chapter 10], which discusses “typical-case feasibility”. We are not aware of much work on the average-case complexity of problems with hyper-exponential complexity. 6. Conclusion We have shown that almost every simply-typed λ-term of order k has a β-reduction sequence as long as (k − 1)-fold exponential in the term size, under a certain assumption. To our knowledge, this is the ﬁrst result of this kind for typed λ-terms. We obtained the result through the parameterized inﬁnite monkey theorem for regular tree grammars, which we may be of independent interest. A lot of questions are left for future work, such as (i) whether our assumption (on the boundedness of arities and the number of variables) is reasonable, and how the result changes for diﬀerent assumptions, (ii) whether our result is optimal (e.g., whether almost every term has a k-fold exponentially long reduction sequence), and (iii) whether similar results hold for Terui’s decision problems [15] and/or the higher-order model checking problem [7]. We would like to thank anonymous referees of FoSSaCS 2017 for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706. References [1] Beckmann, A.: Exact bounds for lengths of reductions in typed lambda-calculus. Journal of Symbolic Logic 66(3) (2001) 1277–1285

text: K.

text: ASADA,

text: N.

text: KOBAYASHI,

text: R.

text: SIN’YA,

text: AND

text: T.

text: TSUKADA

label: section

text: Related

text: Work

text: As

text: mentioned

text: in

text: Section

text: there

text: are

text: several

text: pieces

text: of

text: work

text: on

text: probabilistic

text: properties

text: of

text: untyped

text: λ-terms

text: David

text: et

text: al.

text: have

text: shown

text: that

text: almost

text: all

text: untyped

text: λ-terms

text: are

text: strongly

text: normalizing,

text: whereas

text: the

text: result

text: is

text: opposite

text: for

text: terms

text: expressed

text: in

text: SK

text: combinators.

text: Their

text: former

text: result

text: implies

text: that

text: untyped

text: λ-terms

text: do

text: not

text: satisfy

text: the

text: inﬁnite

text: monkey

text: theorem,

text: i.e.,

text: for

text: any

text: term

text: t,

text: the

text: probability

text: that

text: a

text: randomly

text: chosen

text: term

text: of

text: size

text: n

text: contains

text: t

text: as

text: a

text: subterm

text: tends

text: to

text: zero.

text: Bendkowski

text: et

text: al.

text: proved

text: that

text: almost

text: all

text: terms

text: in

text: de

text: Brujin

text: representation

text: are

text: not

text: strongly

text: normalizing,

text: by

text: regarding

text: the

text: size

text: of

text: an

text: index

text: i

text: is

text: i

text: instead

text: of

text: the

text: constant

text: The

text: discrepancies

text: among

text: those

text: results

text: suggest

text: that

text: this

text: kind

text: of

text: probabilistic

text: property

text: is

text: quite

text: fragile

text: and

text: depends

text: on

text: the

text: deﬁnition

text: of

text: the

text: syntax

text: and

text: the

text: size

text: of

text: terms.

text: Thus,

text: the

text: setting

text: of

text: our

text: paper,

text: especially

text: the

text: assumption

text: on

text: the

text: boundedness

text: of

text: internal

text: arities

text: and

text: the

text: number

text: of

text: variables

text: is

text: a

text: matter

text: of

text: debate,

text: and

text: it

text: would

text: be

text: interesting

text: to

text: study

text: how

text: the

text: result

text: changes

text: for

text: diﬀerent

text: assumptions.

text: We

text: are

text: not

text: aware

text: of

text: similar

text: studies

text: on

text: typed

text: λ-terms.

text: In

text: fact,

text: in

text: their

text: paper

text: about

text: combinatorial

text: aspects

text: of

text: λ-terms,

text: Grygiel

text: and

text: Lescanne

text: pointed

text: out

text: that

text: the

text: combinatorial

text: study

text: of

text: typed

text: λ-terms

text: is

text: diﬃcult,

text: due

text: to

text: the

text: lack

text: of

text: (simple)

text: recursive

text: deﬁnition

text: of

text: typed

text: terms.

text: In

text: the

text: present

text: paper,

text: we

text: have

text: avoided

text: the

text: diﬃculty

text: by

text: making

text: the

text: assumption

text: on

text: the

text: boundedness

text: of

text: internal

text: arities

text: and

text: the

text: number

text: of

text: variables

text: (which

text: is,

text: as

text: mentioned

text: above,

text: subject

text: to

text: a

text: debate

text: though).

text: In

text: a

text: larger

text: context,

text: our

text: work

text: may

text: be

text: viewed

text: as

text: an

text: instance

text: of

text: the

text: studies

text: of

text: average-case

text: complexity

text: Chapter

text: which

text: discusses

text: “typical-case

text: feasibility”.

text: We

text: are

text: not

text: aware

text: of

text: much

text: work

text: on

text: the

text: average-case

text: complexity

text: of

text: problems

text: with

text: hyper-exponential

text: complexity.

text: Conclusion

text: We

text: have

text: shown

text: that

text: almost

text: every

text: simply-typed

text: λ-term

text: of

text: order

text: k

text: has

text: a

text: β-reduction

text: sequence

text: as

text: long

text: as

text: (k

text: exponential

text: in

text: the

text: term

text: size,

text: under

text: a

text: certain

text: assumption.

text: To

text: our

text: knowledge,

text: this

text: is

text: the

text: ﬁrst

text: result

text: of

text: this

text: kind

text: for

text: typed

text: λ-terms.

text: We

text: obtained

text: the

text: result

text: through

text: the

text: parameterized

text: inﬁnite

text: monkey

text: theorem

text: for

text: regular

text: tree

text: grammars,

text: which

text: we

text: may

text: be

text: of

text: independent

text: interest.

text: A

text: lot

text: of

text: questions

text: are

text: left

text: for

text: future

text: work,

text: such

text: as

text: (i)

text: whether

text: our

text: assumption

text: (on

text: the

text: boundedness

text: of

text: arities

text: and

text: the

text: number

text: of

text: variables)

text: is

text: reasonable,

text: and

text: how

text: the

text: result

text: changes

text: for

text: diﬀerent

text: assumptions,

text: (ii)

text: whether

text: our

text: result

text: is

text: optimal

text: (e.g.,

text: whether

text: almost

text: every

text: term

text: has

text: a

text: k-fold

text: exponentially

text: long

text: reduction

text: sequence),

text: and

text: (iii)

text: whether

text: similar

text: results

text: hold

text: for

text: Terui’s

text: decision

text: problems

text: and/or

text: the

text: higher-order

text: model

text: checking

text: problem

text: We

text: would

text: like

text: to

text: thank

text: anonymous

text: referees

text: of

text: FoSSaCS

text: for

text: useful

text: comments.

text: This

text: work

text: was

text: supported

text: by

text: JSPS

text: KAKENHI

text: Grant

text: Number

text: References

text: Beckmann,

text: A.:

text: Exact

text: bounds

text: for

text: lengths

text: of

text: reductions

text: in

text: typed

text: lambda-calculus.

text: Journal

text: of

text: Symbolic

text: Logic


text: (cid:6) (cid:7) (cid:6) (cid:7) × by: (i) breaking the binary vector of length T into parts, (ii) where B¯ , of dimension b T , has as rows all non-zero ptoroevaicdhingpaarltl, paonsdsi(biilie)ncoonm-zbeirnoinbgintahreysvoelcuttoiorsnsthtaot creocrorenssptrouncdt vecStiomrsilaorflydi,imtheenmsiaotnrix(cid:104)TBk k.,Toifhedriemfkoernesiwone bhka×(cid:105)veTb,iis=co2n(cid:100)sTktr(cid:101)u−cte1d. the original vector. However, the two schemes differ in the as follows following: 1) Scheme-1 splits the vector into larger but fewer paadrdtistitvhealny Swchhielme eS-c2h, eamnde-22) Sacghgeremgea-t1esagthgeremgamteusltthipeliscoalutitvieolnys. Bk = 0bk×(k−1)(cid:100)Tk (cid:101) B¯ k , While it is indeed true that providing all possible vectors for × the parts in Scheme-1 would lead to larger partial solutions where B¯ k, of dimension bk Trem, has as rows all non-−zero than those in Scheme-2, aggregating those solutions additively vectors of dimension Trem. Therefore we have bk = 2Trem 1. eventually leads to a smaller number of vectors than in In other words, the matrix Ak is constructed as a block- Scheme-2. Figure 1 shows a comparison between the improved di∈agonal matrix, with the diagonal elements being B¯ i for all scheme proposed in III.1 and its counterpart in [1] for full- i [k]. (cid:88)Therefore equatio(cid:16)n (2) hold(cid:17)s by computing space covering. The remainder of this section proves Theorem III.1 by k − (cid:100) (cid:101) − − ≤ (cid:100) (cid:101) showing how the scheme works (i.e. how A is constructed). Tk = bi = (k 1) 2 Tk 1 +(cid:6)2Tr(cid:7)em 1 k2 Tk , k i=1 Example: We ﬁrst show how the scheme is constructed via a ≤ sremcaolnlsetrxuacmt palve,ecwtohre(cid:6)vre∈(cid:7)T(cid:6)F=8,(cid:7)8weantdreakt =it a3s.kT=he3iddeiasjoisintthpaat,rttso; wWhhiacthrfeomllaoiwnss bisytnootsihnogwthtahtatTraenmy(cid:6) v(cid:7)ecTktor. v ∈ FT2 can be the ﬁrst 2 are of length T2 = 3 and the remaining part is of reconstructed by adding at mos·t· ·k vectors of Ak. T∈o sh−ow this, length T − (k − 1) T =k 2. We then construct A as k = 3 we can express it as v = [v1 vk] where vi, i [k 1] are disjoint sections, whekre each section allowsus to rkeconstruct parts of the vector v each of length Tk , while vk is the last one part of the vector. Speciﬁcally, we construct A as part of v of length Trem(cid:88). Then we(cid:88)can write k   B¯ 0 × 0 × k 1 7 3 7 2 (cid:104) v = v¯ = v¯ , (cid:105) Ak = 07×3 B¯ 2 07×2 , i ∈K i 0 × 0 × B¯ (cid:104) i=1 (cid:105)i (v) 3 3 3 3 3 ∈   where v¯ = 0 − (cid:100) (cid:101) v 0 − − (cid:100) (cid:101) 0 for i where − i (i 1) Tk i (k 1Ki) Tk⊆ Trem     [k 1], v¯ = 0 − (cid:100) (cid:101) v and (v) [k] is the set   k (k 1) T k 0 0 1   of indices for which vi isk no∈t aKll-zero. Then, according to the 0 1 0 construction of A , for all i (v), the corresponding vector   0 1 k B¯ 1 = B¯ 2 = 0 1... 1 , B¯ 3 = 11 01 . vbyi iast omnoesotfkthveecrtoowrss oinf BAik,.and therefore we can construct (cid:4)v 1 1 1 IV. PARTIAL-SPACE COVERING Here we study some speciﬁc instances of the problem, Then any vector v can be reconstructed by picking at most which we will later use in our algorithms. We ﬁrst represent k vectors out of Ak, one from each section. For example, let the problem through a bipartite graph as follows. We assume v = [0 1 0 0 1 1 1 0]. Then this vector can be recons(cid:6)tru(cid:7)cted by that the rank of the matrix G is T. Then, there exists a adding vectors number 2, 10 and 16 from Ak. set of T linearly independent vectors in G; without loss of Proof of Theorem III.1: Let Trem = T − (k − 1) T . Then generality, denote them as g1 to UgT∪.VWEe can th|eUn| represent we can write k t|Vhe| probl−em as a bipartit∈e gUraph ( , ) with = ∈T and   = n T, where u represents vector g for i [T],   ∈ V i ∈ − i B1 vi represents vector gi+T for i [n T], and an edge B2 exists from node ui to node vj if gi is one of the component Ak = ... , vectors of gj+T . Figure 2 shows an example of such graph, where n = 9 and T = 6. For instance, v (i.e., g ) can be ∈ 1 7 Bk reconstructed by adding u , i [4]. Given a node s in the i O I ∈ − × graph, we refer to the sets and as the outbound and where, for i [k 1], the matrix Bi, of dimension bi T, inbound sets of s respectivelys: the inbsound set contains the is constr(cid:104)ucted as follows (cid:105) nodes which have edges outgoing to node s, and the outbound set contains the nodes to which node s has outgoing edges. O { } Bi = 0bi×(i−1)(cid:100)Tk (cid:101) B¯ i 0bi×(k−1−i)(cid:100)Tk (cid:101) 0bi×Trem , Fanodr iInsta=nc{eu, w,iuth,ruef,euren}c.eFtoor Fthigisurpear2ti,culuar1 e=xamvp1l,ev,2t,hve3re v1 1 2 3 4 exists a scheme with T = 6 which can reconstruct any 2 ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine##

text: by:

text: (i)

text: breaking

text: the

text: binary

text: vector

text: of

text: length

text: T

text: into

text: parts,

text: (ii)

text: where

text: B¯

text: of

text: dimension

text: b

text: T

text: has

text: as

text: rows

text: all

text: non-zero

text: ptoroevaicdhingpaarltl,

text: creocrorenssptrouncdt

label: equation

text: k.,Toifhedriemfkoernesiwone

text: the

text: original

text: vector.

text: However,

text: the

text: two

text: schemes

text: differ

text: in

text: the

text: as

text: follows

text: following:

text: splits

text: the

text: vector

text: into

text: larger

text: but

text: fewer

text: paadrdtistitvhealny

text: Swchhielme

text: Bk

text: B¯

text: k

text: While

text: it

text: is

text: indeed

text: true

text: that

text: providing

text: all

text: possible

text: vectors

text: for

text: the

text: parts

text: in

text: would

text: lead

text: to

text: larger

text: partial

text: solutions

text: where

text: B¯

text: k,

text: of

text: dimension

text: bk

text: Trem,

text: has

text: as

text: rows

text: all

text: non-−zero

text: than

text: those

text: in

text: aggregating

text: those

text: solutions

text: additively

text: vectors

text: of

text: dimension

text: Trem.

text: Therefore

text: we

text: have

text: bk

text: eventually

text: leads

text: to

text: a

text: smaller

text: number

text: of

text: vectors

text: than

text: in

text: In

text: other

text: words,

text: the

text: matrix

text: Ak

text: is

text: constructed

text: as

text: a

text: block-

text: Figure

text: shows

text: a

text: comparison

text: between

text: the

text: improved

text: di∈agonal

text: matrix,

text: with

text: the

text: diagonal

text: elements

text: being

text: B¯

text: i

text: for

text: all

text: scheme

text: proposed

text: in

text: and

text: its

text: counterpart

text: in

text: for

text: full-

text: i

text: [k].

text: by

text: computing

text: space

text: covering.

text: The

text: remainder

text: of

text: this

text: section

text: proves

text: Theorem

text: by

text: k

text: showing

text: how

text: the

text: scheme

text: works

text: (i.e.

text: how

text: A

text: is

text: constructed).

text: Tk

text: bi

text: (k

text: Tk

text: Tk

text: k

text: Example:

text: We

text: ﬁrst

text: show

text: how

text: the

text: scheme

text: is

text: constructed

text: via

text: a

text: sremcaolnlsetrxuacmt

text: =it

text: wWhhiacthrfeomllaoiwnss

text: v

text: can

text: be

text: the

text: ﬁrst

text: are

text: of

text: length

text: and

text: the

text: remaining

text: part

text: is

text: of

text: reconstructed

text: by

text: adding

text: at

text: mos·t·

text: ·k

text: vectors

text: of

text: Ak.

text: T∈o

text: sh−ow

text: this,

text: length

text: T

text: (k

text: T

text: =k

text: We

text: then

text: construct

text: A

text: as

text: k

text: we

text: can

text: express

text: it

text: as

text: v

text: vk]

text: where

text: vi,

text: i

text: [k

text: are

text: disjoint

text: sections,

text: whekre

text: each

text: section

text: allowsus

text: to

text: rkeconstruct

text: parts

text: of

text: the

text: vector

text: v

text: each

text: of

text: length

text: Tk

text: while

text: vk

text: is

text: the

text: last

text: one

text: part

text: of

text: the

text: vector.

text: Speciﬁcally,

text: we

text: construct

text: A

text: as

text: part

text: of

text: v

text: of

text: length

text: Then

text: write

text: k

text: B¯

text: k

text: v

text: v¯

text: v¯

text: Ak

text: B¯

text: i

text: ∈K

text: i

text: B¯

text: (v)

text: where

text: v¯

text: v

text: for

text: i

text: where

text: i

text: (i

text: Tk

text: i

text: (k

text: Tk⊆

text: Trem

text: [k

text: v¯

text: v

text: and

text: (v)

text: [k]

text: is

text: the

text: set

text: k

text: (k

text: T

text: k

text: 0

text: 1

text: of

text: indices

text: for

text: which

text: vi

text: isk

text: no∈t

text: aKll-zero.

text: Then,

text: according

text: to

text: the

text: 0

text: 0

text: construction

text: of

text: A

text: for

text: all

text: i

text: (v),

text: the

text: corresponding

text: vector

text: k

text: B¯

text: B¯

text: B¯

text: vbyi

text: iast

text: omnoesotfkthveecrtoowrss

text: oinf

text: BAik,.and

text: therefore

text: we

text: can

text: construct

text: IV.

text: PARTIAL-SPACE

text: COVERING

text: Here

text: we

text: study

text: some

text: speciﬁc

text: instances

text: of

text: the

text: problem,

text: Then

text: any

text: vector

text: v

text: can

text: be

text: reconstructed

text: by

text: picking

text: at

text: most

text: which

text: we

text: will

text: later

text: use

text: in

text: our

text: algorithms.

text: We

text: ﬁrst

text: represent

text: k

text: vectors

text: out

text: of

text: Ak,

text: one

text: from

text: each

text: section.

text: For

text: example,

text: let

text: the

text: problem

text: through

text: a

text: bipartite

text: graph

text: as

text: follows.

text: We

text: assume

text: v

text: Then

text: this

text: vector

text: can

text: be

text: by

text: that

text: the

text: rank

text: of

text: the

text: matrix

text: G

text: is

text: T.

text: Then,

text: there

text: exists

text: a

text: adding

text: vectors

text: number

text: and

text: from

text: Ak.

text: set

text: of

text: T

text: linearly

text: independent

text: vectors

text: in

text: G;

text: without

text: loss

text: of

text: Proof

text: of

text: Theorem

text: Let

text: Trem

text: T

text: (k

text: T

text: Then

text: generality,

text: denote

text: them

text: as

text: to

text: UgT∪.VWEe

text: can

text: th|eUn|

text: represent

text: we

text: can

text: write

text: k

text: t|Vhe|

text: probl−em

text: as

text: a

text: bipartit∈e

text: gUraph

text: with

text: ∈T

text: and

text: n

text: T,

text: where

text: u

text: represents

text: vector

text: g

text: for

text: i

text: [T],

text: V

text: i

text: i

text: B1

text: vi

text: represents

text: vector

text: gi+T

text: for

text: i

text: [n

text: T],

text: and

text: an

text: edge

text: exists

text: from

text: node

text: ui

text: to

text: node

text: vj

text: if

text: gi

text: is

text: one

text: of

text: the

text: component

text: Ak

text: vectors

text: of

text: gj+T

text: Figure

text: shows

text: an

text: example

text: of

text: such

text: graph,

text: where

text: n

text: and

text: T

text: For

text: instance,

text: v

text: (i.e.,

text: g

text: can

text: be

text: Bk

text: reconstructed

text: by

text: adding

text: u

text: i

text: Given

text: a

text: node

text: s

text: in

text: the

text: i

text: O

text: I

text: graph,

text: we

text: refer

text: to

text: the

text: sets

text: and

text: as

text: the

text: outbound

text: and

text: where,

text: for

text: i

text: [k

text: the

text: matrix

text: Bi,

text: of

text: dimension

text: bi

text: T,

text: inbound

text: sets

text: of

text: s

text: respectivelys:

text: the

text: inbsound

text: set

text: contains

text: the

text: is

text: as

text: follows

text: nodes

text: which

text: have

text: edges

text: outgoing

text: to

text: node

text: s,

text: and

text: the

text: outbound

text: set

text: contains

text: the

text: nodes

text: to

text: which

text: node

text: s

text: has

text: outgoing

text: edges.

text: O

text: Bi

text: B¯

text: i

text: Fanodr

text: iInsta=nc{eu,

text: w,iuth,ruef,euren}c.eFtoor

text: exists

text: a

text: scheme

text: with

text: T

text: which

text: can

text: reconstruct

text: any

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##


text: ∈ and pose the index coding problem as that of minimizing the xxx , j K . The decoder at the ith receiver is a function j i broadcast rate (ratio of codeword length to message length) A| | × A | | → A D : Ri m Ki m, for a given desired value of locality (Section ). We then show i that the minimum locality of any unicast index coding problem and the estimate of the message xxx at the ith receiver (i, K ) ∈ i i is 1, and the optimum index code for this value of locality is D (ccc , (xxx , j K )). The tuple (E, D , . . . , D ) of en- i Ri j i 1 N is the code derived from the optimum fractional coloring coding and decoding functions denotes a valid index code for of the interference graph of the given problem (Section ). the index coding problem represented by the side information V E ∈ ∈ We then provide several constructions of locally decodable graph G = ( , ) if D (ccc , (xxx , j K )) = xxx for all i i ∈RAi j i i index codes by covering the side-information graph using [N] and all (xxx , . . . ,xxx ) mN, where ccc = E(xxx , . . . ,xxx ). 1 N 1 N acyclic subgraphs and subgraphs of small minrank. We also The receiver (i, K ) decodes xxx using the sub-vector | | i i show how the traditional partition multicast [1], [7] and cycle ccc , and hence, R is the number of symbols queried or Ri i covering [6], [9] solutions to index coding can be modiﬁed downloaded by this receiver when using the index code | | to yield locally decodable index codes (Section ). Using (E, D , . . . , D ). For fairness, we normalize R by the 1 N i these coding techniques and information-theoretic inequalities number of symbols m in the desired message xxx to deﬁne | | i ∈ we derive the exact trade-off between locality and broadcast the locality r of the ith receiver as r = R /m, for i [N]. i i i rate of the 3-user unicast index coding problem whose side Deﬁnition 1. The locality or the overall locality of the index information graph is a directed cycle (Section ). Finally in code (E, D , . . . , D ) 1 N Section we discuss the relation of locally decodable index | | R codes with the problems of sparse representation of vectors r = max r = max i (1) and privacy-preserving index codes and conclude the paper. i∈[N] i i∈[N] m Notation: For any positive integer N, we will denote the { } is the maximum number of coded symbols queried by any set 1, . . . , N by [N]. Row vectors will be denoted by bold of the N receivers per decoded information symbol. lower case letters, for example xxx. For any length N vector ⊂ xxx = (x , . . . , x ) and a set R [N], we deﬁne xxx to be the The broadcast rate of this index code is β = (cid:96)/m, and 1 N ∈ R sub-vector (x , j R). For a set of vectors xxx , . . . ,xxx and a measures the bandwidth or time required by the source to ⊂ j 1 N ∈ subset K [N], we deﬁne xxx to be the vector (xxx , j K). broadcast the coded symbols to all the receivers. ∅K j The empty set is denoted by . For a matrix AAA, the component Without loss of generality we will consider only those index ∪ · · · ∪ in jth row and ith column is denoted as AAA . codes for which R R = [(cid:96)] since any codeword j,i 1 N II. DEFINITIONS AND PRELIMINARIES symbol c which is not utilized at any of the receivers, i.e., ∈j \ ∪ · · · ∪ c for j [(cid:96)] (R R ), need not be generated or j 1 N The index coding problem [1], [2] consists of a single trans- transmitted by the encoder. mitter jointly encoding N independent messages xxx1, . . . ,xxxN For a given locality r, it is desirable to use an index code to broadcast a codeword ccc to multiple receivers through with as small a value of β as possible and vice versa, which a noiseless broadcast channel. We consider the family of leads us to the following deﬁnition. unicast index coding problems, where each message xxx is dwkenhsoeiwrreendKtaoit⊂tehxe[aNcrte]lcyiesiovthneeer saoesft sotihfdeeinrdieniccfeeoisrvmeorafst,tihodene.mnWoetseistdhaogauesst (aliol,rseKsiadio)yf, Dobpreotﬁiamndciatalisobtnrroa2ate.dscGaamisvteornnagtaealuflunmnicceatsisostangineβdG∗leex(nrg)ctohidssimnthge≥pirn1oﬁbamlneudmmalGlovf, attlhhidee generality, we assume that i ∈/ K . The side information index codes with locality at the most r. i graph oVf tEhis index coding problemVis the directed graph The function β∗ (r) captures the trade-off between the G = ( , ), where the vertex set = [N] and the edge reduction in the nGumber of channel uses possible through E { | ∈ ∈ } set = (i, j) for all j K , i [N] . Throughout this coding and the number of codeword symbols that a receiver i paper we will consider only unicast index coding problems has to query to decode each message symbol. and denote a problem by its side information graph G. We will rely on information-theoretic inequalities to obtain ∗ We assume that the messages Axxx1, . . . ,xxx|AN| are vectors of bounds on βG(r), and to do so we will assume that the length m over a ﬁnite alphabet , with > 1, and the messages xxx , . . . ,xxx are random, independent of each other 1 N A codeword ccc is a vector of length (cid:96) over the same alphabet, and are uniformly distributed in m. The logarithms used in ∈ A ∈ ∈ A i.e., xxx m, i [N], and ccc (cid:96). We will assume that measuring mutual information and entropy will be calculated i A |A| the alphabet is arbitrary but ﬁxed for a given index coding to the base . For example, the entropy of xxx is H(xxx ) = m A i i problem. since xxx is uniformly distributed in m. i ∗ The transmitted codeword ccc = (c , c , . . . , c ) is a function We will now prove some properties of β (r). 1 2 (cid:96) A → G of the messages ccc = E(xxx , . . . ,xxx ), where E : mN A 1 N Lemma 1. The locality r of any valid index coding scheme (cid:96) denotes the encoder. Instead of observing the entire ≥ satisﬁes r 1. codeword ccc, the ith receiver observes only a sub-vector ∈ ⊂ ccc = (c , j R ), where R [(cid:96)], and the receiver desires Proof: This can be shown using the fact I(xxx ;ccc ,xxx ) = Ri j i i i Ri Ki to estimate the message xxx using ccc and its side information H(xxx ) = m, which arises when considering the decoder at the i Ri i ##LTLine##

text: and

text: pose

text: the

text: index

text: coding

text: problem

text: as

text: that

text: of

text: minimizing

text: the

text: xxx

text: j

text: K

text: The

text: decoder

text: at

text: the

text: ith

text: receiver

text: is

text: a

text: function

text: j

text: i

text: broadcast

text: rate

text: (ratio

text: of

text: codeword

text: length

text: to

text: message

text: length)

text: A|

text: A

text: A

text: D

text: Ri

text: m

text: Ki

text: m,

text: for

text: a

text: given

text: desired

text: value

text: of

text: locality

text: (Section

text: We

text: then

text: show

text: i

text: that

text: the

text: minimum

text: locality

text: of

text: any

text: unicast

text: index

text: coding

text: problem

text: and

text: the

text: estimate

text: of

text: the

text: message

text: xxx

text: at

text: the

text: ith

text: receiver

text: (i,

text: K

text: i

text: i

text: is

text: and

text: the

text: optimum

text: index

text: code

text: for

text: this

text: value

text: of

text: locality

text: is

text: D

text: (ccc

text: (xxx

text: j

text: K

text: The

text: tuple

text: (E,

text: D

text: D

text: of

text: en-

text: i

text: Ri

text: j

text: i

text: N

text: is

text: the

text: code

text: derived

text: from

text: the

text: optimum

text: fractional

text: coloring

text: coding

text: and

text: decoding

text: functions

text: denotes

text: a

text: valid

text: index

text: code

text: for

text: of

text: the

text: interference

text: graph

text: of

text: the

text: given

text: problem

text: (Section

text: the

text: index

text: coding

text: problem

text: represented

text: by

text: the

text: side

text: information

text: V

text: E

text: We

text: then

text: provide

text: several

text: constructions

text: of

text: locally

text: decodable

text: graph

text: G

text: if

text: D

text: (ccc

text: (xxx

text: j

text: K

text: xxx

text: for

text: all

text: i

text: i

text: ∈RAi

text: j

text: i

text: i

text: index

text: codes

text: by

text: covering

text: the

text: side-information

text: graph

text: using

text: [N]

text: and

text: all

text: (xxx

text: ,xxx

text: mN,

text: where

text: ccc

text: E(xxx

text: ,xxx

text: N

text: N

text: acyclic

text: subgraphs

text: and

text: subgraphs

text: of

text: small

text: minrank.

text: We

text: also

text: The

text: receiver

text: (i,

text: K

text: decodes

text: xxx

text: using

text: the

text: sub-vector

text: i

text: i

text: show

text: how

text: the

text: traditional

text: partition

text: multicast

text: and

text: cycle

text: ccc

text: and

text: hence,

text: R

text: is

text: the

text: number

text: of

text: symbols

text: queried

text: or

text: Ri

text: i

text: covering

text: solutions

text: to

text: index

text: coding

text: can

text: be

text: modiﬁed

text: downloaded

text: by

text: this

text: receiver

text: when

text: using

text: the

text: index

text: code

text: to

text: yield

text: locally

text: decodable

text: index

text: codes

text: (Section

text: Using

text: (E,

text: D

text: D

text: For

text: fairness,

text: we

text: normalize

text: R

text: by

text: the

text: N

text: i

text: these

text: coding

text: techniques

text: and

text: information-theoretic

text: inequalities

text: number

text: of

text: symbols

text: m

text: in

text: the

text: desired

text: message

text: xxx

text: to

text: deﬁne

text: i

text: we

text: derive

text: the

text: exact

text: trade-off

text: between

text: locality

text: and

text: broadcast

text: the

text: locality

text: r

text: of

text: the

text: ith

text: receiver

text: as

text: r

text: R

text: /m,

text: for

text: i

text: [N].

text: i

text: i

text: i

text: rate

text: of

text: the

text: unicast

text: index

text: coding

text: problem

text: whose

text: side

text: Deﬁnition

text: The

text: locality

text: or

text: the

text: overall

text: locality

text: of

text: the

text: index

text: information

text: graph

text: is

text: a

text: directed

text: cycle

text: (Section

text: Finally

text: in

text: code

text: (E,

text: D

text: D

text: N

text: Section

text: we

text: discuss

text: the

text: relation

text: of

text: locally

text: decodable

text: index

text: R

text: codes

text: with

text: the

text: problems

text: of

text: sparse

text: representation

text: of

text: vectors

text: r

text: max

text: r

text: max

text: i

text: and

text: privacy-preserving

text: index

text: codes

text: and

text: conclude

text: the

text: paper.

text: i∈[N]

text: i

text: i∈[N]

text: m

text: Notation:

text: For

text: any

text: positive

text: integer

text: N,

text: we

text: will

text: denote

text: the

text: is

text: the

text: maximum

text: number

text: of

text: coded

text: symbols

text: queried

text: by

text: any

text: set

text: N

text: by

text: [N].

text: Row

text: vectors

text: will

text: be

text: denoted

text: by

text: bold

text: of

text: the

text: N

text: receivers

text: per

text: decoded

text: information

text: symbol.

text: lower

text: case

text: letters,

text: for

text: example

text: xxx.

text: For

text: any

text: length

text: N

text: vector

text: xxx

text: (x

text: x

text: and

text: a

text: set

text: R

text: [N],

text: we

text: deﬁne

text: xxx

text: to

text: be

text: the

text: The

text: broadcast

text: rate

text: of

text: this

text: index

text: code

text: is

text: β

text: and

text: N

text: R

text: sub-vector

text: (x

text: j

text: R).

text: For

text: a

text: set

text: of

text: vectors

text: xxx

text: ,xxx

text: and

text: a

text: measures

text: the

text: bandwidth

text: or

text: time

text: required

text: by

text: the

text: source

text: to

text: j

text: N

text: subset

text: K

text: [N],

text: we

text: deﬁne

text: xxx

text: to

text: be

text: the

text: vector

text: (xxx

text: j

text: K).

text: broadcast

text: the

text: coded

text: symbols

text: to

text: all

text: the

text: receivers.

text: ∅K

text: j

text: The

text: empty

text: set

text: is

text: denoted

text: by

text: For

text: a

text: matrix

text: AAA,

text: the

text: component

text: Without

text: loss

text: of

text: generality

text: we

text: will

text: consider

text: only

text: those

text: index

text: in

text: jth

text: row

text: and

text: ith

text: column

text: is

text: denoted

text: as

text: AAA

text: codes

text: for

text: which

text: R

text: R

text: since

text: any

text: codeword

text: j,i

text: N

text: II.

text: DEFINITIONS

text: AND

text: PRELIMINARIES

text: symbol

text: c

text: which

text: is

text: not

text: utilized

text: at

text: any

text: of

text: the

text: receivers,

text: i.e.,

text: ∈j

text: c

text: for

text: j

text: (R

text: R

text: need

text: not

text: be

text: generated

text: or

text: j

text: N

text: The

text: index

text: coding

text: problem

text: consists

text: of

text: a

text: single

text: trans-

text: transmitted

text: by

text: the

text: encoder.

text: mitter

text: jointly

text: encoding

text: N

text: independent

text: messages

text: ,xxxN

text: For

text: a

text: given

text: locality

text: r,

text: it

text: is

text: desirable

text: to

text: use

text: an

text: index

text: code

text: to

text: broadcast

text: a

text: codeword

text: ccc

text: to

text: multiple

text: receivers

text: through

text: with

text: as

text: small

text: a

text: value

text: of

text: β

text: as

text: possible

text: and

text: vice

text: versa,

text: which

text: a

text: noiseless

text: broadcast

text: channel.

text: We

text: consider

text: the

text: family

text: of

text: leads

text: us

text: to

text: the

text: following

text: deﬁnition.

text: unicast

text: index

text: coding

text: problems,

text: where

text: each

text: message

text: xxx

text: is

text: saoesft

text: (aliol,rseKsiadio)yf,

text: attlhhidee

text: generality,

text: we

text: assume

text: that

text: i

text: K

text: The

text: side

text: information

text: index

text: codes

text: with

text: locality

text: at

text: the

text: most

text: r.

text: i

text: graph

text: oVf

text: tEhis

text: index

text: coding

text: problemVis

text: the

text: directed

text: graph

text: The

text: function

text: β∗

text: (r)

text: captures

text: the

text: trade-off

text: between

text: the

text: G

text: where

text: the

text: vertex

text: set

text: [N]

text: and

text: the

text: edge

text: reduction

text: in

text: the

text: nGumber

text: of

text: channel

text: uses

text: possible

text: through

text: E

text: set

text: (i,

text: j)

text: for

text: all

text: j

text: K

text: i

text: [N]

text: Throughout

text: this

text: coding

text: and

text: the

text: number

text: of

text: codeword

text: symbols

text: that

text: a

text: receiver

text: i

text: paper

text: we

text: will

text: consider

text: only

text: unicast

text: index

text: coding

text: problems

text: has

text: to

text: query

text: to

text: decode

text: each

text: message

text: symbol.

text: and

text: denote

text: a

text: problem

text: by

text: its

text: side

text: information

text: graph

text: G.

text: We

text: will

text: rely

text: on

text: information-theoretic

text: inequalities

text: to

text: obtain

text: We

text: assume

text: that

text: the

text: messages

text: ,xxx|AN|

text: are

text: vectors

text: of

text: bounds

text: on

text: βG(r),

text: and

text: to

text: do

text: so

text: we

text: will

text: assume

text: that

text: the

text: length

text: m

text: over

text: a

text: ﬁnite

text: alphabet

text: with

text: and

text: the

text: messages

text: xxx

text: ,xxx

text: are

text: random,

text: independent

text: of

text: each

text: other

text: N

text: A

text: codeword

text: ccc

text: is

text: a

text: vector

text: of

text: length

text: over

text: the

text: same

text: alphabet,

text: and

text: are

text: uniformly

text: distributed

text: in

text: m.

text: The

text: logarithms

text: used

text: in

text: A

text: A

text: i.e.,

text: xxx

text: m,

text: i

text: [N],

text: and

text: ccc

text: We

text: will

text: assume

text: that

text: measuring

text: mutual

text: information

text: and

text: entropy

text: will

text: be

text: calculated

text: i

text: A

text: |A|

text: the

text: alphabet

text: is

text: arbitrary

text: but

text: ﬁxed

text: for

text: a

text: given

text: index

text: coding

text: to

text: the

text: base

text: For

text: example,

text: the

text: entropy

text: of

text: xxx

text: is

text: H(xxx

text: m

text: A

text: i

text: i

text: problem.

text: since

text: xxx

text: is

text: uniformly

text: distributed

text: in

text: m.

text: i

text: The

text: transmitted

text: codeword

text: ccc

text: (c

text: c

text: c

text: is

text: a

text: function

text: We

text: will

text: now

text: prove

text: some

text: properties

text: of

text: β

text: (r).

text: A

text: G

text: of

text: the

text: messages

text: ccc

text: E(xxx

text: ,xxx

text: where

text: E

text: mN

text: A

text: N

text: Lemma

text: The

text: locality

text: r

text: of

text: any

text: valid

text: index

text: coding

text: scheme

text: denotes

text: the

text: encoder.

text: Instead

text: of

text: observing

text: the

text: entire

text: satisﬁes

text: r

text: codeword

text: ccc,

text: the

text: ith

text: receiver

text: observes

text: only

text: a

text: sub-vector

text: ccc

text: (c

text: j

text: R

text: where

text: R

text: and

text: the

text: receiver

text: desires

text: Proof:

text: This

text: can

text: be

text: shown

text: using

text: the

text: fact

text: I(xxx

text: ;ccc

text: ,xxx

text: Ri

text: j

text: i

text: i

text: i

text: Ri

text: Ki

text: to

text: estimate

text: the

text: message

text: xxx

text: using

text: ccc

text: and

text: its

text: side

text: information

text: H(xxx

text: m,

text: which

text: arises

text: when

text: considering

text: the

text: decoder

text: at

text: the

text: i

text: Ri

text: i

text: ##LTLine##


text: [5] A. Blasiak, R. D. Kleinberg, and E. Lubetzky, “Index coding via linear programming,” arXiv preprint, 2010. [Online]. Available: http://arxiv.org/abs/1004.1379 [6] M. A. R. Chaudhry, Z. Asad, A. Sprintson, and M. Langberg, “On the complementary index coding problem,” in 2011 IEEE International Symposium on Information Theory Proceedings, July 2011, pp. 244–248. [7] A. S. Tehrani, A. G. Dimakis, and M. J. Neely, “Bipartite index coding,” in 2012 IEEE International Symposium on Information Theory Proceedings, July 2012, pp. 2246–2250. [8] A. Blasiak, R. Kleinberg, and E. Lubetzky, “Broadcasting with side information: Bounding and approximating the broadcast rate,” IEEE Transactions on Information Theory, vol. 59, no. 9, pp. 5811–5823, Sept 2013. [9] M. J. Neely, A. S. Tehrani, and Z. Zhang, “Dynamic index coding for wireless broadcast networks,” IEEE Trans. Inf. Theory, vol. 59, no. 11, pp. 7525–7540, Nov 2013. [10] K. Shanmugam, A. G. Dimakis, and M. Langberg, “Local graph coloring and index coding,” in Information Theory Proceedings (ISIT), 2013 IEEE International Symposium on, July 2013, pp. 1152–1156. [11] ——, “Graph theory versus minimum rank for index coding,” in Infor- mation Theory Proceedings (ISIT), 2014 IEEE International Symposium on, 2014. [12] F. Arbabjolfaei and Y. H. Kim, “Local time sharing for index coding,” in 2014 IEEE International Symposium on Information Theory, June 2014, pp. 286–290. [13] H. Maleki, V. R. Cadambe, and S. A. Jafar, “Index coding – an interference alignment perspective,” IEEE Transactions on Information Theory, vol. 60, no. 9, pp. 5402–5432, Sept 2014. [14] A. Agarwal and A. Mazumdar, “Local partial clique covers for index coding,” arXiv preprint arXiv:1603.02366, 2016. [15] I. Haviv and M. Langberg, “On linear index coding for random graphs,” in 2012 IEEE International Symposium on Information Theory Proceed- ings, July 2012, pp. 2231–2235. [16] M. Karmoose, L. Song, M. Cardone, and C. Fragouli, “Preserving privacy while broadcasting: k-limited-access schemes,” arXiv preprint arXiv:1705.08437, 2017. [17] C. Godsil and G. F. Royle, Algebraic graph theory. Springer Science & Business Media, 2013, vol. 207. [18] S. H. Dau, V. Skachek, and Y. M. Chee, “On the security of index coding with side information,” IEEE Transactions on Information Theory, vol. 58, no. 6, pp. 3975–3988, June 2012. [19] S. A. Jafar, “Topological interference management through index cod- ing,” IEEE Transactions on Information Theory, vol. 60, no. 1, pp. 529– 568, Jan 2014.

label: reference

text: A.

text: Blasiak,

text: R.

text: D.

text: Kleinberg,

text: and

text: E.

text: Lubetzky,

text: “Index

text: coding

text: via

text: linear

text: programming,”

text: arXiv

text: preprint,

text: [Online].

text: Available:

text: M.

text: A.

text: R.

text: Chaudhry,

text: Z.

text: Asad,

text: A.

text: Sprintson,

text: and

text: M.

text: Langberg,

text: “On

text: the

text: complementary

text: index

text: coding

text: problem,”

text: in

text: IEEE

text: International

text: Symposium

text: on

text: Information

text: Theory

text: Proceedings,

text: July

text: pp.

text: A.

text: S.

text: Tehrani,

text: A.

text: G.

text: Dimakis,

text: and

text: M.

text: J.

text: Neely,

text: “Bipartite

text: index

text: coding,”

text: in

text: IEEE

text: International

text: Symposium

text: on

text: Information

text: Theory

text: Proceedings,

text: July

text: pp.

text: A.

text: Blasiak,

text: R.

text: Kleinberg,

text: and

text: E.

text: Lubetzky,

text: “Broadcasting

text: with

text: side

text: information:

text: Bounding

text: and

text: approximating

text: the

text: broadcast

text: rate,”

text: IEEE

text: Transactions

text: on

text: Information

text: Theory,

text: vol.

text: no.

text: pp.

text: Sept

text: M.

text: J.

text: Neely,

text: A.

text: S.

text: Tehrani,

text: and

text: Z.

text: Zhang,

text: “Dynamic

text: index

text: coding

text: for

text: wireless

text: broadcast

text: networks,”

text: IEEE

text: Trans.

text: Inf.

text: Theory,

text: vol.

text: no.

text: pp.

text: Nov

text: K.

text: Shanmugam,

text: A.

text: G.

text: Dimakis,

text: and

text: M.

text: Langberg,

text: “Local

text: graph

text: coloring

text: and

text: index

text: coding,”

text: in

text: Information

text: Theory

text: Proceedings

text: (ISIT),

text: IEEE

text: International

text: Symposium

text: on,

text: July

text: pp.

text: “Graph

text: theory

text: versus

text: minimum

text: rank

text: for

text: index

text: coding,”

text: in

text: Infor-

text: mation

text: Theory

text: Proceedings

text: (ISIT),

text: IEEE

text: International

text: Symposium

text: on,

text: F.

text: Arbabjolfaei

text: and

text: Y.

text: H.

text: Kim,

text: “Local

text: time

text: sharing

text: for

text: index

text: coding,”

text: in

text: IEEE

text: International

text: Symposium

text: on

text: Information

text: Theory,

text: June

text: pp.

text: H.

text: Maleki,

text: V.

text: R.

text: Cadambe,

text: and

text: S.

text: A.

text: Jafar,

text: “Index

text: coding

text: an

text: interference

text: alignment

text: perspective,”

text: IEEE

text: Transactions

text: on

text: Information

text: Theory,

text: vol.

text: no.

text: pp.

text: Sept

text: A.

text: Agarwal

text: and

text: A.

text: Mazumdar,

text: “Local

text: partial

text: clique

text: covers

text: for

text: index

text: coding,”

text: arXiv

text: preprint

text: I.

text: Haviv

text: and

text: M.

text: Langberg,

text: “On

text: linear

text: index

text: coding

text: for

text: random

text: graphs,”

text: in

text: IEEE

text: International

text: Symposium

text: on

text: Information

text: Theory

text: Proceed-

text: ings,

text: July

text: pp.

text: M.

text: Karmoose,

text: L.

text: Song,

text: M.

text: Cardone,

text: and

text: C.

text: Fragouli,

text: “Preserving

text: privacy

text: while

text: broadcasting:

text: k-limited-access

text: schemes,”

text: arXiv

text: preprint

text: C.

text: Godsil

text: and

text: G.

text: F.

text: Royle,

text: Algebraic

text: graph

text: theory.

text: Springer

text: Science

text: Business

text: Media,

text: vol.

text: S.

text: H.

text: Dau,

text: V.

text: Skachek,

text: and

text: Y.

text: M.

text: Chee,

text: “On

text: the

text: security

text: of

text: index

text: coding

text: with

text: side

text: information,”

text: IEEE

text: Transactions

text: on

text: Information

text: Theory,

text: vol.

text: no.

text: pp.

text: June

text: S.

text: A.

text: Jafar,

text: “Topological

text: interference

text: management

text: through

text: index

text: cod-

text: ing,”

text: IEEE

text: Transactions

text: on

text: Information

text: Theory,

text: vol.

text: no.

text: pp.

text: Jan


text: | − | ∗ ≥ ≥ entropies, we have H(ccc xxx ) H(ccc xxx ,xxx ) = m. Us- Further, β (G) = 2, and hence, β (r) 2 for all r 1. Ri i+1 | Ri ≤i i+1 ≤ | | opt G ing this with the upper bound H(ccc xxx ) H(ccc ) R , Combining this with the above inequality we have the converse Ri i+1 Ri i we arrive at ∗ ≥ { − } ≥ β (r) max 6 3r, 2 for all r 1. | ≤ | | − G H(ccc xxx ,xxx ) R m. Ri i i+1 i Using the above inequality and the fact that cccRi is a deter- VI. CONCLUSION AND DISCUSSION ministic function of all three messages xxx ,xxx ,xxx , we have | | i ≤i|+1 | −i+2 I(ccc ;xxx xxx ,xxx ) = H(ccc xxx ,xxx ) R m. Hence, Ri i+2 i i+1 Ri i i+1 i Relation to other problems | − | ≤ | | − H(xxx xxx ,xxx ) H(xxx ccc ,xxx ,xxx ) R m. Locally decodable index codes are related to privacy- i+2 i i+1 i+2 Ri i i+1 i | preserving broadcasting and the problem of sparse repre- Since H(xxxi+2 xxxi,xxxi+1) = m, we obtain the lower bound sentation of sets of vectors. In [16], the authors consider | ≥ − | | scalar linear index codes with locality r under a privacy H(xxxi+2 cccRi,xxxi,xxxi+1) 2m Ri . (11) preserving communication scenario using the terminology r- limited access schemes. The motivation for using r-limited access schemes is to reduce the amount of information that Our objective now is to use the above inequality to obtain | ∩ | any receiver can infer about the demands of other receivers an upper bound on R R , which can then be translated i i+2 in the network. This is achieved by restricting the knowledge into a lower bound on (cid:96), and hence, a lower bound on β. of the scalar linear encoder matrix BBB at any receiver to at the To do so, observe that ccc is composed of the following two Ri most r columns instead of revealing the entire matrix. Thus sub-vectors ccc ∩ and ccc \ . Using (11), we obtain Ri Ri+2 Ri Ri+2 each receiver knows the values of at the most r columns of the H(xxx |ccc ∩ ,xxx ) ≥ H(xxx |ccc ,xxx ,xxx ) ≥ 2m − |R |. encoder matrix BBB, and hence, is required to perform decoding i+2 Ri Ri+2 i i+2 Ri i i+1 i by querying at the most r codeword symbols which correspond | Using this inequality, and the relation H(xxx ccc ,xxx ) = 0 to these columns. (to satisfy the demands of the (i + 2)th reci+ei2veRr)i,+w2 e iobtain A scalar linear index code with locality r is characterized by the following a valid encoder matrix BBB with a corresponding ﬁtting matrix | \ | ≥ AAA such that any column of AAA is some linear combination of at Ri+2 Ri ≥ H(cccRi+2\Ri) | the most r columns of BBB. Thus the columns of BBB serve as an I(x ;ccc \ ccc ∩ ,xxx ) overcomplete basis for a sparse representation of the columns = H(xxxi+2 |cccRi+∩2 Ri ,Rxxxi)Ri+2 i of AAA. i+2 −Ri Ri+2 |i H(xxx ccc \ ,ccc ∩ ,xxx ) | i+2 R−i+2 Ri Ri| Ri+2 i Conclusion = H(xxx ccc ∩ ,xxx ) H(xxx ccc ,xxx ) ≥ −i+|2 R| i Ri+2 i i+2 Ri+2 i We introduced the problem of designing index codes that 2m Ri . are locally decodable and have identiﬁed several techniques | | | | | | to construct such codes. We have also identiﬁed the optimum Since R = R = R , we now have 1 2 3 broadcast rate corresponding to unit locality for any unicast | ∩ | | | − | \ | index coding problem, and the complete locality-rate trade- R R = R R R i i+2 i+2 i+2 i ≤ | | − − | | off curve for the problem represented by a directed 3-cycle. R (2m R ) i| | − i Stronger achievability and/or converse results may be required = 2 ( Ri m) . to gain further insights into the locality-rate trade-off of a | ∩ | general index coding problem. Finally, using the fact that R R is independent of i, i i+2 |(cid:88) ∪ ∪(cid:88)| (cid:96) = R R R ACKNOWLEDGMENT 1 2 3 ≥ 3 | | − 3 | ∩ | The ﬁrst author thanks Prof. B. Sundar Rajan for discussions R R R regarding the topic of this paper. j j j+2 j=1 i=1 | | − | ∩ | = 3 R 3 R R APPENDIX A i i i+2 ≥ | | − × | | − PROOF OF LEMMA 2 3 R 3 2( R m) i− | | i The non-increasing property of β∗ follows immediately = 6m 3 Ri . from its deﬁnition. We will use timeG-sharing to prove con- ≥ Dividing both sides by the message length m, and remember- vexity. Assume r , r 1 and let (cid:15) > 0. For each j = 1, 2, 1 2 ≤ ∗ ing that all the receivers have the same locality r, we have there exists an index code with broadcast rate β β (r )+(cid:15) ≥ − j G j β = (cid:96)/m 6 3r. Thus we have and locality at the most r . We will denote the blocklength of j βG∗ (r) ≥ 6 − 3r for all r ≥ 1. tthhiesincdoidceesbuyse(cid:96)dj,bmy ethsseaNge rleecnegitvherbsyasmRj1,ajn, .d. .th, eRNsu,jb,swethseoref

text: entropies,

text: we

text: have

text: H(ccc

text: xxx

text: H(ccc

text: xxx

text: ,xxx

text: m.

text: Us-

text: Further,

text: β

text: (G)

text: and

text: hence,

text: β

text: (r)

text: for

text: all

text: r

text: Ri

text: Ri

text: ≤i

text: opt

text: G

text: ing

text: this

text: with

text: the

text: upper

text: bound

text: H(ccc

text: xxx

text: H(ccc

text: R

text: Combining

text: this

text: with

text: the

text: above

text: inequality

text: we

text: have

text: the

text: converse

text: Ri

text: Ri

text: i

text: we

text: arrive

text: at

text: β

text: (r)

text: max

text: for

text: all

text: r

text: G

text: H(ccc

text: xxx

text: ,xxx

text: R

text: m.

text: Ri

text: i

text: i

text: Using

text: the

text: above

text: inequality

text: and

text: the

text: fact

text: that

text: cccRi

text: is

text: a

text: deter-

text: VI.

text: CONCLUSION

text: AND

text: DISCUSSION

text: ministic

text: function

text: of

text: all

text: three

text: messages

text: xxx

text: ,xxx

text: ,xxx

text: we

text: have

text: i

text: I(ccc

text: ;xxx

text: xxx

text: ,xxx

text: H(ccc

text: xxx

text: ,xxx

text: R

text: m.

text: Hence,

text: Ri

text: i

text: Ri

text: i

text: i

text: Relation

text: to

text: other

text: problems

text: H(xxx

text: xxx

text: ,xxx

text: H(xxx

text: ccc

text: ,xxx

text: ,xxx

text: R

text: m.

text: Locally

text: decodable

text: index

text: codes

text: are

text: related

text: to

text: privacy-

text: i

text: Ri

text: i

text: i

text: preserving

text: broadcasting

text: and

text: the

text: problem

text: of

text: sparse

text: repre-

text: Since

text: m,

text: we

text: obtain

text: the

text: lower

text: bound

text: sentation

text: of

text: sets

text: of

text: vectors.

text: In

text: the

text: authors

text: consider

text: scalar

text: linear

text: index

text: codes

text: with

text: locality

text: r

text: under

text: a

text: privacy

text: Ri

text: preserving

text: communication

text: scenario

text: using

text: the

text: terminology

text: r-

text: limited

text: access

text: schemes.

text: The

text: motivation

text: for

text: using

text: r-limited

text: access

text: schemes

text: is

text: to

text: reduce

text: the

text: amount

text: of

text: information

text: that

text: Our

text: objective

text: now

text: is

text: to

text: use

text: the

text: above

text: inequality

text: to

text: obtain

text: any

text: receiver

text: can

text: infer

text: about

text: the

text: demands

text: of

text: other

text: receivers

text: an

text: upper

text: bound

text: on

text: R

text: R

text: which

text: can

text: then

text: be

text: translated

text: i

text: in

text: the

text: network.

text: This

text: is

text: achieved

text: by

text: restricting

text: the

text: knowledge

text: into

text: a

text: lower

text: bound

text: on

text: and

text: hence,

text: a

text: lower

text: bound

text: on

text: β.

text: of

text: the

text: scalar

text: linear

text: encoder

text: matrix

text: BBB

text: at

text: any

text: receiver

text: to

text: at

text: the

text: To

text: do

text: so,

text: observe

text: that

text: ccc

text: is

text: composed

text: of

text: the

text: following

text: two

text: Ri

text: most

text: r

text: columns

text: instead

text: of

text: revealing

text: the

text: entire

text: matrix.

text: Thus

text: sub-vectors

text: ccc

text: and

text: ccc

text: Using

text: we

text: obtain

text: Ri

text: Ri

text: each

text: receiver

text: knows

text: the

text: values

text: of

text: at

text: the

text: most

text: r

text: columns

text: of

text: the

text: H(xxx

text: |ccc

text: ,xxx

text: H(xxx

text: |ccc

text: ,xxx

text: ,xxx

text: |R

text: encoder

text: matrix

text: BBB,

text: and

text: hence,

text: is

text: required

text: to

text: perform

text: decoding

text: Ri

text: i

text: Ri

text: i

text: i

text: by

text: querying

text: at

text: the

text: most

text: r

text: codeword

text: symbols

text: which

text: correspond

text: Using

text: this

text: inequality,

text: and

text: the

text: relation

text: H(xxx

text: ccc

text: ,xxx

text: to

text: these

text: columns.

text: (to

text: satisfy

text: the

text: demands

text: of

text: the

text: (i

text: e

text: iobtain

text: A

text: scalar

text: linear

text: index

text: code

text: with

text: locality

text: r

text: is

text: characterized

text: by

text: the

text: following

text: a

text: valid

text: encoder

text: matrix

text: BBB

text: with

text: a

text: corresponding

text: ﬁtting

text: matrix

text: AAA

text: such

text: that

text: any

text: column

text: of

text: AAA

text: is

text: some

text: linear

text: combination

text: of

text: at

text: Ri

text: the

text: most

text: r

text: columns

text: of

text: BBB.

text: Thus

text: the

text: columns

text: of

text: BBB

text: serve

text: as

text: an

text: I(x

text: ;ccc

text: ccc

text: ,xxx

text: overcomplete

text: basis

text: for

text: a

text: sparse

text: representation

text: of

text: the

text: columns

text: Ri

text: i

text: of

text: AAA.

text: −Ri

text: |i

text: H(xxx

text: ccc

text: ,ccc

text: ,xxx

text: Ri

text: Ri|

text: i

text: Conclusion

text: H(xxx

text: ccc

text: ,xxx

text: H(xxx

text: ccc

text: ,xxx

text: R|

text: i

text: i

text: i

text: We

text: introduced

text: the

text: problem

text: of

text: designing

text: index

text: codes

text: that

text: Ri

text: are

text: locally

text: decodable

text: and

text: have

text: identiﬁed

text: several

text: techniques

text: to

text: construct

text: such

text: codes.

text: We

text: have

text: also

text: identiﬁed

text: the

text: optimum

text: Since

text: R

text: R

text: R

text: we

text: now

text: have

text: broadcast

text: rate

text: corresponding

text: to

text: unit

text: locality

text: for

text: any

text: unicast

text: index

text: coding

text: problem,

text: and

text: the

text: complete

text: locality-rate

text: trade-

text: R

text: R

text: R

text: R

text: R

text: i

text: i

text: off

text: curve

text: for

text: the

text: problem

text: represented

text: by

text: a

text: directed

text: R

text: R

text: i|

text: i

text: Stronger

text: achievability

text: and/or

text: converse

text: results

text: may

text: be

text: required

text: Ri

text: m)

text: to

text: gain

text: further

text: insights

text: into

text: the

text: locality-rate

text: trade-off

text: of

text: a

text: general

text: index

text: coding

text: problem.

text: Finally,

text: using

text: the

text: fact

text: that

text: R

text: R

text: is

text: independent

text: of

text: i,

text: i

text: R

text: R

text: R

text: ACKNOWLEDGMENT

text: The

text: ﬁrst

text: author

text: thanks

text: Prof.

text: B.

text: Sundar

text: Rajan

text: for

text: discussions

text: R

text: R

text: R

text: regarding

text: the

text: topic

text: of

text: this

text: paper.

text: j

text: j

text: R

text: R

text: R

text: APPENDIX

text: A

text: i

text: i

text: PROOF

text: OF

text: LEMMA

text: R

text: R

text: m)

text: i−

text: i

text: The

text: non-increasing

text: property

text: of

text: β∗

text: follows

text: immediately

text: Ri

text: from

text: its

text: deﬁnition.

text: We

text: will

text: use

text: timeG-sharing

text: to

text: prove

text: con-

text: Dividing

text: both

text: sides

text: by

text: the

text: message

text: length

text: m,

text: and

text: remember-

text: vexity.

text: Assume

text: r

text: r

text: and

text: let

text: For

text: each

text: j

text: ing

text: that

text: all

text: the

text: receivers

text: have

text: the

text: same

text: locality

text: r,

text: we

text: have

text: there

text: exists

text: an

text: index

text: code

text: with

text: broadcast

text: rate

text: β

text: β

text: (r

text: j

text: G

text: j

text: β

text: Thus

text: we

text: have

text: and

text: locality

text: at

text: the

text: most

text: r

text: We

text: will

text: denote

text: the

text: blocklength

text: of

text: j

text: βG∗

text: (r)

text: for

text: all

text: r

text: ethsseaNge

text: .d.

text: .th,

text: eRNsu,jb,swethseoref


text: ∈ j = 1, 2. For some choice of non-negative integers k and symbols (c , t C ). This decoding method uses R = C for 1 ∈ t i i i k , consider a time-sharing scheme where the ﬁrst index code all i [N] and has locality r = 1. 2 is used k m times, and the second index code is used k m 1 2 2 1 times. For this composite scheme, the overall message length is APPENDIX C m = k m m +k m m = m m (k +k ). The blocklength PROOF OF LEMMA 9 1 2 1 2 1 2 1 2 1 2 is (cid:96) = k1m2(cid:96)1+k2m1(cid:96)2, and the number of codeword symbols Since σ is an automorphism of G, so is σn for any n ∈ [N]. u| tili|zed by th|e ith |receiver t|o de|code its desired message is Note that the group {σ, σ2, . . . , σN = 1} acts transitively Ri = k1m2 Ri,1 + k2m1 Ri,2 . The locality of this time- on the vertex set of G. Let (E, D , . . . , D ) be an index sharing system can be upper bounded as 1 N code for G with rate β and receiver localities r , . . . , r . We | | | | | | 1 N R k R k R will consider N index coding schemes (E(n), D(n), . . . , D(n)), max i = max 1 i,1 + 2 i,2 ∈ 1 N i m i (k1 + k2)m1 (k1 + k2)m2 n [N], each of which is derived from (E, D1, . . . , DN) by ≤ k k+1 k r1 + k k+2 k r2. ptheermnuthtinegnctohdeerroEle(sn)ofisthtehemeenscsoagdeesr xxxE1,a.p.p.li,exxxdNt.oStpheecinﬁtchallelyft, 1 2 1 2 cyclic shift of the message tuple xxx , . . . ,xxx , i.e., Similarly, the broadcast rate of this time-sharing scheme can (cid:0) 1 N (cid:1) be shown to be equal to k β /(k + k ) + k β /(k + k ), E(n) ( (xxx , . . . ,xxx ) ) = E( (xxx ,xxx , . . . ,xxx ,xxx , . . . ,xxx ) ) 1 1 1 2 2 2 1 2 1 N n+1 n+2 N 1 n which is upper bounded by = E (xxx , . . . ,xxx ) . σn(1) σn(N) k ∗ k ∗ ∈ k +1 k βG(r1) + k +2 k βG(r2) + (cid:15). For any i −[N], in the above expression of E−(n), the mes−sage 1 2 1 2 xxx is the (i n)th argument of E where (i n) = (i n) D→enoting k1r1/(k1+k2)+k2r2/(k1+k2) by r, and by letting ifi(i − n) ≥ 1 anNd (i − n)N = i − n + N otherwNise. Hence, (cid:15) 0, we observe that the encoding function E(n) operates on the message xxx in the i ∗ ≤ k ∗ k ∗ same manner asE operates on the message xxx − . Using βG(r) k +1 k βG(r1) + k +2 k βG(r2). the fact that σ is an automorphism of G, it is ea(siynto)Nsee that, 1 2 1 2 when the nth code is used, the ith receiver can decode xxx as Convexity follows by approximating any real number in the i D − (ccc ,xxx ). Thus, the codeword symbols queried idnetseirrveadl a(c0c,u1r)acbyybytheusirnagtiosnuaflﬁcniuenmtlbyerlakrg1e/(kk11 a+ndk2k)2.to any bwyh(iethrene)mNith irsRe(ctihe−einv)meNreisnsKatgihee lnenthgctho.de is |R(i−n)N | = m r(i−n)N , Now consider a time sharing scheme that utilizes each of the APPENDIX B FRACTIONAL COLORING SOLUTION HAS UNIT LOCALITY N encoders E(1), . . . , E(N) exactly once. The overall message length for this schem(cid:88)e is mN, the broadca(cid:88)st rate is β, and the We will now recall the fractional coloring solution [5] to number of codeword symbols queried by the ith receiver is an index coding problem G and observe that r = 1 for this ⊂ { } | (cid:48)| | | scheme. Let C , . . . , C 1, . . . , a be an a : b coloring of R = R − = m r . G¯ such that χ1 (G¯ ) =N a/b. Set codeword length (cid:96) = a and i ∈ (i n)N ∈ n u f u n [N(cid:88)] n [N] message length m = b. Denote the components of the message ∈ ∈ A ∈ A Similarly, for any i [N] and j = i mod N + 1, we have vectors xxx m using the variables w as follows: i ∈ i,t xxxeaich=co(wloir,tt, tin thCAei)s,eti.eC.,i.oEnnedosywm(cid:80)tbhoelsweti,At cwoirtrhesapnoyndaibnegliaton |Ri(cid:48) ∩ Rj(cid:48) | = n(cid:88)∈[N] |R(i−n)N ∩ R(i−n+1)N | group structure ( , +). The symbols of the codeword ccc = | ∩ | ∈ (c1D, .e.c.o,dcin(cid:96))g araet gtehneerraetceedivaesrct(i=, K )i:tc∈aCni wbei,t,pfeorrfotrme[d(cid:96)].as = n∈[N] Rn R(n+1)N , i follow∈s. Note that xxxi is composed of all symbols wi,t such which is independent of i. that t C . In order to decode w , the receiver retrieves the i (cid:88)i,t code symbol ct which is related to wi,t as REFERENCES c = w + w . (12) t i,t j,t [1] Y. Birk and T. Kol, “Informed-source coding-on-demand (ISCOD) over (cid:54) j=∈i broadcast channels,” in Proc. 17th Annu. Joint Conf. IEEE Computer and j:t Cj Communications Societies (INFOCOM), vol. 3, Mar. 1998, pp. 1257– 1264. For any choice of the index j in the summation term above, [2] Z. Bar-Yossef, Y. Birk, T. S. Jayram, and T. Kol, “Index coding with side (cid:54) ∈ ∩ we have i = j and t C C . Since C , . . . , C is a coloring information,” IEEE Trans. Inf. Theory, vol. 57, no. 3, pp. 1479–1494, of G¯ and C ∩ C (cid:54)= i∅, jwe deduce1 that {iN, j} ∈/ E¯ , or Mar. 2011. u i ∈ j (cid:54) ∈u [3] R. Peeters, “Orthogonal representations over ﬁnite ﬁelds and the equivalently, j K . Hence, for each j = i such that t C , chromatic number of graphs,” Combinatorica, vol. 16, no. 3, pp. 417– i j the receiver (i, K ) knows the value of w , and thus, can 431, Sep 1996. [Online]. Available: https://doi.org/10.1007/BF01261326 i j,t [4] N. Alon, E. Lubetzky, U. Stav, A. Weinstein, and A. Hassidim, “Broad- recover w from c using (12). Using a similar procedure i,t t casting with side information,” in Proc. 49th IEEE Symp. Foundations (i, K ) can decode all the m symbols in xxx from the m coded of Computer Science (FOCS), Oct. 2008, pp. 823–832. i i ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine## ##LTLine##

text: j

text: For

text: some

text: choice

text: of

text: non-negative

text: integers

text: k

text: and

text: symbols

text: (c

text: t

text: C

text: This

text: decoding

text: method

text: uses

text: R

text: C

text: for

text: t

text: i

text: i

text: i

text: k

text: consider

text: a

text: time-sharing

text: scheme

text: where

text: the

text: ﬁrst

text: index

text: code

text: all

text: i

text: [N]

text: and

text: has

text: locality

text: r

text: is

text: used

text: k

text: m

text: times,

text: and

text: the

text: second

text: index

text: code

text: is

text: used

text: k

text: m

text: times.

text: For

text: this

text: composite

text: scheme,

text: the

text: overall

text: message

text: length

text: is

text: APPENDIX

text: C

text: m

text: k

text: m

text: m

text: +k

text: m

text: m

text: m

text: m

text: (k

text: +k

text: The

text: blocklength

text: PROOF

text: OF

text: LEMMA

text: is

text: and

text: the

text: number

text: of

text: codeword

text: symbols

text: Since

text: σ

text: is

text: an

text: automorphism

text: of

text: G,

text: so

text: is

text: σn

text: for

text: any

text: n

text: [N].

text: u|

text: tili|zed

text: by

text: th|e

text: ith

text: |receiver

text: t|o

text: de|code

text: its

text: desired

text: message

text: is

text: Note

text: that

text: the

text: group

text: {σ,

text: σN

text: acts

text: transitively

text: Ri

text: The

text: locality

text: of

text: this

text: time-

text: on

text: the

text: vertex

text: set

text: of

text: G.

text: Let

text: (E,

text: D

text: D

text: be

text: an

text: index

text: sharing

text: system

text: can

text: be

text: upper

text: bounded

text: as

text: N

text: code

text: for

text: G

text: with

text: rate

text: β

text: and

text: receiver

text: localities

text: r

text: r

text: We

text: N

text: R

text: k

text: R

text: k

text: R

text: will

text: consider

text: N

text: index

text: coding

text: schemes

text: (E(n),

text: D(n),

text: D(n)),

text: max

text: i

text: max

text: N

text: i

text: m

text: i

text: n

text: [N],

text: each

text: of

text: which

text: is

text: derived

text: from

text: (E,

text: DN)

text: by

text: k

text: k

text: k

text: k

text: cyclic

text: shift

text: of

text: the

text: message

text: tuple

text: xxx

text: ,xxx

text: i.e.,

text: Similarly,

text: the

text: broadcast

text: rate

text: of

text: this

text: time-sharing

text: scheme

text: can

text: N

text: be

text: shown

text: to

text: be

text: equal

text: to

text: k

text: β

text: /(k

text: k

text: k

text: β

text: /(k

text: k

text: E(n)

text: (xxx

text: ,xxx

text: E(

text: (xxx

text: ,xxx

text: ,xxx

text: ,xxx

text: ,xxx

text: N

text: N

text: n

text: which

text: is

text: upper

text: bounded

text: by

text: E

text: (xxx

text: ,xxx

text: σn(N)

text: k

text: k

text: k

text: k

text: k

text: k

text: For

text: any

text: i

text: −[N],

text: in

text: the

text: above

text: expression

text: of

text: E−(n),

text: the

text: mes−sage

text: xxx

text: is

text: the

text: (i

text: n)th

text: argument

text: of

text: E

text: where

text: (i

text: n)

text: (i

text: n)

text: D→enoting

text: by

text: r,

text: and

text: by

text: letting

text: ifi(i

text: n)

text: anNd

text: (i

text: n)N

text: i

text: n

text: N

text: otherwNise.

text: Hence,

text: we

text: observe

text: that

text: the

text: encoding

text: function

text: E(n)

text: operates

text: on

text: the

text: message

text: xxx

text: in

text: the

text: i

text: k

text: k

text: same

text: manner

text: asE

text: operates

text: on

text: the

text: message

text: xxx

text: Using

text: βG(r)

text: k

text: k

text: k

text: k

text: the

text: fact

text: that

text: σ

text: is

text: an

text: automorphism

text: of

text: G,

text: it

text: is

text: ea(siynto)Nsee

text: that,

text: when

text: the

text: nth

text: code

text: is

text: used,

text: the

text: ith

text: receiver

text: can

text: decode

text: xxx

text: as

text: Convexity

text: follows

text: by

text: approximating

text: any

text: real

text: number

text: in

text: the

text: i

text: D

text: (ccc

text: ,xxx

text: Thus,

text: the

text: codeword

text: symbols

text: queried

text: idnetseirrveadl

text: any

text: bwyh(iethrene)mNith

text: irsRe(ctihe−einv)meNreisnsKatgihee

text: lnenthgctho.de

text: is

text: |R(i−n)N

text: m

text: r(i−n)N

text: Now

text: consider

text: a

text: time

text: sharing

text: scheme

text: that

text: utilizes

text: each

text: of

text: the

text: APPENDIX

text: B

text: FRACTIONAL

text: COLORING

text: SOLUTION

text: HAS

text: UNIT

text: LOCALITY

text: N

text: encoders

text: E(N)

text: exactly

text: once.

text: The

text: overall

text: message

text: length

text: for

text: this

text: is

text: mN,

text: the

text: rate

text: is

text: β,

text: and

text: the

text: We

text: will

text: now

text: recall

text: the

text: fractional

text: coloring

text: solution

text: to

text: number

text: of

text: codeword

text: symbols

text: queried

text: by

text: the

text: ith

text: receiver

text: is

text: an

text: index

text: coding

text: problem

text: G

text: and

text: observe

text: that

text: r

text: for

text: this

text: scheme.

text: Let

text: C

text: C

text: a

text: be

text: an

text: a

text: b

text: coloring

text: of

text: R

text: R

text: m

text: r

text: G¯

text: such

text: that

text: χ1

text: (G¯

text: =N

text: a/b.

text: Set

text: codeword

text: length

text: a

text: and

text: i

text: (i

text: n)N

text: n

text: u

text: f

text: u

text: n

text: n

text: [N]

text: message

text: length

text: m

text: b.

text: Denote

text: the

text: components

text: of

text: the

text: message

text: A

text: A

text: Similarly,

text: for

text: any

text: i

text: [N]

text: and

text: j

text: i

text: mod

text: N

text: we

text: have

text: vectors

text: xxx

text: m

text: using

text: the

text: variables

text: w

text: as

text: follows:

text: i

text: i,t

text: xxxeaich=co(wloir,tt,

text: tin

text: cwoirtrhesapnoyndaibnegliaton

text: |R(i−n)N

text: group

text: structure

text: The

text: symbols

text: of

text: the

text: codeword

text: ccc

text: araet

text: gtehneerraetceedivaesrct(i=,

text: K

text: )i:tc∈aCni

text: n∈[N]

text: Rn

text: i

text: follow∈s.

text: Note

text: that

text: xxxi

text: is

text: composed

text: of

text: all

text: symbols

text: wi,t

text: such

text: which

text: is

text: independent

text: of

text: i.

text: that

text: t

text: C

text: In

text: order

text: to

text: decode

text: w

text: the

text: receiver

text: retrieves

text: the

text: i

text: code

text: symbol

text: ct

text: which

text: is

text: related

text: to

text: wi,t

text: as

text: REFERENCES

text: c

text: w

text: w

text: t

text: i,t

text: j,t

text: Y.

text: Birk

text: and

text: T.

text: Kol,

text: “Informed-source

text: coding-on-demand

text: (ISCOD)

text: over

text: j=∈i

text: broadcast

text: channels,”

text: in

text: Proc.

text: Annu.

text: Joint

text: Conf.

text: IEEE

text: Computer

text: and

text: j:t

text: Cj

text: Communications

text: Societies

text: (INFOCOM),

text: vol.

text: Mar.

text: pp.

text: For

text: any

text: choice

text: of

text: the

text: index

text: j

text: in

text: the

text: summation

text: term

text: above,

text: Z.

text: Bar-Yossef,

text: Y.

text: Birk,

text: T.

text: S.

text: Jayram,

text: and

text: T.

text: Kol,

text: “Index

text: coding

text: with

text: side

text: we

text: have

text: i

text: j

text: and

text: t

text: C

text: C

text: Since

text: C

text: C

text: is

text: a

text: coloring

text: information,”

text: IEEE

text: Trans.

text: Inf.

text: Theory,

text: vol.

text: no.

text: pp.

text: of

text: G¯

text: and

text: C

text: C

text: i∅,

text: jwe

text: that

text: {iN,

text: j}

text: E¯

text: or

text: Mar.

text: u

text: i

text: j

text: ∈u

text: R.

text: Peeters,

text: “Orthogonal

text: representations

text: over

text: ﬁnite

text: ﬁelds

text: and

text: the

text: equivalently,

text: j

text: K

text: Hence,

text: for

text: each

text: j

text: i

text: such

text: that

text: t

text: C

text: chromatic

text: number

text: of

text: graphs,”

text: Combinatorica,

text: vol.

text: no.

text: pp.

text: i

text: j

text: the

text: receiver

text: (i,

text: K

text: knows

text: the

text: value

text: of

text: w

text: and

text: thus,

text: can

text: Sep

text: [Online].

text: Available:

text: i

text: j,t

text: N.

text: Alon,

text: E.

text: Lubetzky,

text: U.

text: Stav,

text: A.

text: Weinstein,

text: and

text: A.

text: Hassidim,

text: “Broad-

text: recover

text: w

text: from

text: c

text: using

text: Using

text: a

text: similar

text: procedure

text: i,t

text: t

text: casting

text: with

text: side

text: information,”

text: in

text: Proc.

text: IEEE

text: Symp.

text: Foundations

text: (i,

text: K

text: can

text: decode

text: all

text: the

text: m

text: symbols

text: in

text: xxx

text: from

text: the

text: m

text: coded

text: of

text: Computer

text: Science

text: (FOCS),

text: Oct.

text: pp.

text: i

text: i

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##

text: ##LTLine##