第24章

有理数演算による算術符号化

(やさしい版) Pearls of Functional Algorithm Design(関数プログラミングによるアルゴリズム設計の真珠)

どんな問題?

この章のテーマは 算術符号化(arithmetic coding) という データ圧縮 の方法です。

ハフマン符号のような普通の方法では、テキストの 1 文字ごとに「決まった長さのビット列」を割り当てます。それに対して算術符号化は、テキスト全体をまとめて 1 つの小数(0 以上 1 未満の数)で表す という、少し変わったやり方をします。

この章で扱うこと この章の実装は「単純だが時間と空間を食う」ものです。もっと現実的にする話は次章に譲ります。

はじめに

算術符号化の位置づけ

算術符号化は 1987 年に Witten・Neal・Cleary の「使いやすい実装」の論文が出て以降、圧縮方式の本格的なライバルになりました。以来 20 年ほどで、次のような特徴がわかってきました。

本章と次章の関係

算術符号化は「実装が厄介」と言われがちですが、この本では 2 章にわたって、基本アルゴリズムをきちんと導出していきます。

有理数演算による算術符号化

基本アイデア:区間を狭めていく

算術符号化の基本的な考え方はこうです。

  1. 元テキストを シンボル に分ける。シンボルは単語でもよいし、1 文字でもよい。ここでは、シンボルの種類は有限だけあるとする。
  2. それぞれのシンボルに、単位区間 [0, 1) の中の 半開区間 を対応づける。この対応づけを モデル と呼ぶ。
  3. テキストの各シンボルに対応する区間を使って、単位区間を 順番にだんだん狭めていく
  4. 最後に残った区間の中から、できるだけ短い(分母が小さい)分数 を 1 つ選ぶ。

基本のデータ型

Haskell では次のように書けます。

type Fraction = Ratio Integer type Interval = (Fraction, Fraction)
Dart // 任意精度整数の比として分数を表現する簡易クラス。 // Dart 標準には Rational 型がないので最小限を自前で用意する。 class Fraction { final BigInt num; final BigInt den; Fraction(BigInt n, BigInt d) : assert(d != BigInt.zero), num = _sign(d) * n ~/ _gcd(n.abs(), d.abs()), den = d.abs() ~/ _gcd(n.abs(), d.abs()); factory Fraction.of(int n, [int d = 1]) => Fraction(BigInt.from(n), BigInt.from(d)); static BigInt _sign(BigInt x) => x < BigInt.zero ? -BigInt.one : BigInt.one; static BigInt _gcd(BigInt a, BigInt b) => b == BigInt.zero ? a : _gcd(b, a % b); Fraction operator +(Fraction o) => Fraction(num * o.den + o.num * den, den * o.den); Fraction operator -(Fraction o) => Fraction(num * o.den - o.num * den, den * o.den); Fraction operator *(Fraction o) => Fraction(num * o.num, den * o.den); Fraction operator /(Fraction o) => Fraction(num * o.den, den * o.num); bool operator <(Fraction o) => num * o.den < o.num * den; bool operator <=(Fraction o) => num * o.den <= o.num * den; @override bool operator ==(Object o) => o is Fraction && num == o.num && den == o.den; @override int get hashCode => Object.hash(num, den); @override String toString() => den == BigInt.one ? '$num' : '$num/$den'; } typedef Interval = (Fraction, Fraction); // (左端, 右端)
記法のお約束

区間を狭める

▷ 演算子

ij は「区間 i を、区間 j ぶんだけ狭める」演算です。返ってくるのは i の部分区間で、i の中に j と同じ比率で置かれた区間 になります(j が単位区間 (0, 1) に対して占める割合と同じ比率で、i の中に配置される)。

(▷) :: Interval → Interval → Interval (ℓ₁, r₁) ▷ (ℓ₂, r₂) = (ℓ₁+(r₁−ℓ₁)∗ℓ₂, ℓ₁+(r₁−ℓ₁)∗r₂)
Dart // i ▷ j : 区間 i を、区間 j ぶんだけ狭める。 Interval narrow(Interval i, Interval j) { final (l1, r1) = i; final (l2, r2) = j; final w = r1 - l1; return (l1 + w * l2, l1 + w * r2); }
▷ の便利な性質

◁ 演算子(逆に広げる)

逆に、狭めた区間の中の分数を「もとの単位区間の中でどの位置か」に戻す操作が ◁ です。

(◁) :: Fraction → Interval → Fraction f ◁ (ℓ, r) = (f − ℓ) / (r − ℓ)
Dart // f ◁ i : 狭めた区間内の f を、単位区間内の相対位置に戻す。 Fraction widen(Fraction f, Interval i) { final (l, r) = i; return (f - l) / (r - l); }

これを使うと、▷ と ◁ の関係は次のように まとめられます

f ∈ i ▷ j ⇒ f ∈ i ∧ (f ◁ i) ∈ j (24.1)

実はこれは同値関係です。さらに ◁ を区間にも拡張して (ℓ, r) ◁ j = (ℓ ◁ j, rj) とすると、(ij) ◁ i = j となり、▷ は 数学的な群としての性質 をすべて備えます。

モデル

モデルとは

テキストを符号化するには、どのシンボルにどの区間を割り当てるか を決めておく必要があります。ここでは Model という抽象型を用意し、次の 2 つの関数を持たせます。

interval :: Model → Symbol → Interval symbol :: Model → Fraction → Symbol
Dart // Symbol は何でもよい。ここでは String(1 文字)で表現する。 typedef Symbol = String; // Model はシンボル -> 区間 と 分数 -> シンボル の 2 つの操作を提供する。 abstract class Model { Interval interval(Symbol x); Symbol symbol(Fraction f); Model adapt(Symbol x); // 後で使う }

各シンボルの区間は単位区間を すきまなく分割 しているとします。ですから、次の等式が任意の mf について成り立ちます。

x = symbol m f ≡ f ∈ interval m x (24.2)

適応的モデル

実用上の重要な工夫として、シンボルを 1 つ読むたびにモデルを変えてもよい という決まりがあります。これを 適応的(adaptive) 符号化と呼びます。

詳細な適応方法には踏み込まず、次の関数の存在だけを仮定します。

adapt :: Model → Symbol → Model
Dart // 上の Model 抽象クラスに含めた Model adapt(Symbol x) と同じ。 // シンボルを 1 つ読むたびに、新しいモデル(頻度を更新したもの)を返す。

そしてシンボル列を区間列に変える関数 intervals は次のようになります。

intervals m [] = [] intervals m (x : xs) = interval m x : intervals (adapt m x) xs
Dart // シンボル列 xs をモデル m で区間列に変換する。 // 読むたびにモデルを adapt して次に渡す(純粋関数的)。 List<Interval> intervals(Model m, List<Symbol> xs) { final out = <Interval>[]; var cur = m; for (final x in xs) { out.add(cur.interval(x)); cur = cur.adapt(x); } return out; }
大事なポイント 復号側でも、初期モデルと adapt のやり方さえわかっていれば、シンボルを 1 つ復元するたびに同じ手順でモデルを更新できます。だから モデル自体を一緒に送る必要はありません

符号化(encode)

encode の定義

準備がそろったので、符号化関数を書けます。

encode :: Model → [Symbol] → Fraction encode m = pick · foldl (▷) (0, 1) · intervals m
Dart // pick i : 区間 i の中から適当な分数を 1 つ選ぶ関数(後で定義)。 Fraction pick(Interval i); // 単位区間 (0, 1) から始め、区間列で順に狭めて最後に分数を 1 つ選ぶ。 Fraction encodeFrac(Model m, List<Symbol> xs) { final unit = (Fraction.of(0), Fraction.of(1)); final ivs = intervals(m, xs); var acc = unit; for (final j in ivs) { acc = narrow(acc, j); } return pick(acc); }

ここで pick i は「区間 i の中から適当な分数を 1 つ選ぶ関数」で、pick ii を満たすとします。全体の流れは

  1. シンボル列を区間の列に変える(intervals m
  2. 単位区間 (0, 1) を、その区間で 順番に狭めていくfoldl
  3. できあがった最終区間から 1 つ分数を選ぶ(pick

例:evergreen を符号化する

次の 5 文字のシンボルを持つ静的モデル m を考えます。

[(e, (0, 3/8)), (g, (3/8, 1/2)), (n, (1/2, 5/8)), (r, (5/8, 7/8)), (v, (7/8, 1))]

このモデルで "evergreen" を符号化すると、こうなります。

encode m "evergreen" = pick ((0, 1) ▷ (0, 3/8) ▷ (7/8, 1) ⋯ ▷ (1/2, 5/8)) = pick (11445828/2²⁵, 11445909/2²⁵)
結果

復号(decode)

仕様の書き方

素直に書くと decode の仕様は

xs = decode m (encode m xs)

となります(符号化してから復号すれば元に戻る)。しかし、あとで述べる理由から、この仕様は少し弱められて、

xs ⊑ decode m (encode m xs) (24.3)

だけを要求します。⊑ は「接頭辞である」という関係で、ys = xs ++ zs となる zs があれば xsys です。

なぜ弱めるのか decode は「元のシンボル列を必ず先頭に出す」ことは保証しますが、そこで止まる保証はしません(続けて余計なシンボルを出してしまう可能性がある)。停止をどうするかは後で扱います。

復号の考え方

入力を xs = [x₀, x₁, ..., xₙ₋₁] とし、初期モデルを m₀、初期区間を j₀ = (0, 1) と書きます。次のように置きます(0 ≤ k < n)。

m_{k+1} = adapt m_k x_k i_k = interval m_k x_k j_{k+1} = j_k ▷ i_{k+1}

encode の定義から、f = encode mxs ならば fjₙ です。n > 0 のとき、次のように順に推論できます。

f ∈ j_n ≡ {j_n の定義} f ∈ (j_{n−1} ▷ i_n) ⇒ {(24.1)} f ∈ j_{n−1} ∧ (f ◁ j_{n−1}) ∈ i_n ≡ {i_n の定義} f ∈ j_{n−1} ∧ (f ◁ j_{n−1}) ∈ interval m_n x_n ≡ {(24.2)} f ∈ j_{n−1} ∧ x_n = symbol m_n (f ◁ j_{n−1})

これを繰り返すことで、次の等式が成り立つとわかります。

x_k = symbol m_k (f ◁ j_{k−1}) (24.4)

この式を使えば、k = n−1 から 0 の逆順にも、k = 0 から n−1 の順にも、シンボルを復元できます。ただし復号側は シンボルが何個あるかを知らない ため、後者ではシンボルを永久に出し続けてしまいます。

Haskell での実装

復号は unfoldr(リストを生成する関数)で実装します。

unfoldr :: (b → Maybe (a, b)) → b → [a] unfoldr f b = case f b of Just (a, b') → a : unfoldr f b' Nothing → []
Dart // 状態 b から値 a を次々と生成するジェネレータ。 // 関数 f が null を返した時点で終了する(Haskell の Nothing に相当)。 Iterable<A> unfoldr<A, B>(B seed, (A, B)? Function(B) f) sync* { var b = seed; while (true) { final r = f(b); if (r == null) return; yield r.$1; b = r.$2; } }
decode :: Model → Fraction → [Symbol] decode m f = unfoldr step (m, (0, 1), f) step (m, i, f) = Just (x, (adapt m x, i ▷ interval m x, f)) where x = symbol m (f ◁ i)
Dart // 復号:モデルの状態 (m, i) と分数 f を持ち、1 シンボルずつ生成する。 // 注意:この step は Nothing を返さないので無限に走り続ける。停止方法は後述。 typedef DecState = (Model, Interval, Fraction); Iterable<Symbol> decodeFrac(Model m, Fraction f) { final unit = (Fraction.of(0), Fraction.of(1)); return unfoldr<Symbol, DecState>((m, unit, f), (s) { final (mm, ii, ff) = s; final x = mm.symbol(widen(ff, ii)); return (x, (mm.adapt(x), narrow(ii, mm.interval(x)), ff)); }); }

停止をどうするか

「決められた数だけ復号したら止める」ためには、次の 2 通りが考えられます。

実務では方法 B が多い ただし方法 B には欠点もあります。すべてのモデルに EOF 用の区間を確保しなければならず、他のシンボルに使える区間の合計幅がその分だけ狭められてしまいます。

逐次的な符号化と復号

分数のままだと不便

これまでの encodedecode は単純で美しいのですが、扱うのが 分数 です。ところが分母は あっという間に巨大化 してしまいます。できれば、

pick を 2 つに分解する

そこで pick を 2 段に分けます。

toBits :: Interval → [Bit] toFrac :: [Bit] → Fraction pick = toFrac · toBits
Dart // Bit は 0 か 1。ここでは int で表現する。 typedef Bit = int; Iterable<Bit> toBits(Interval i); // 実装は後述 Fraction toFrac(List<Bit> bs); // 実装は後述 Fraction pickViaBits(Interval i) => toFrac(toBits(i).toList());

すると encodedecode はビット列を扱う形に書き直せます。

encode :: Model → [Symbol] → [Bit] encode m = toBits · foldl (▷) (0, 1) · intervals m decode :: Model → [Bit] → [Symbol] decode m bs = unfoldr step (m, (0, 1), toFrac bs) step (m, i, f) = Just (x, (adapt m x, i ▷ interval m x, f)) where x = symbol m (f ◁ i)
Dart // 分数版から、ビット列版へ書き直したもの。中身の流れは同じ。 List<Bit> encodeBits(Model m, List<Symbol> xs) { final unit = (Fraction.of(0), Fraction.of(1)); var acc = unit; for (final j in intervals(m, xs)) { acc = narrow(acc, j); } return toBits(acc).toList(); } Iterable<Symbol> decodeBits(Model m, List<Bit> bs) { final unit = (Fraction.of(0), Fraction.of(1)); final f = toFrac(bs); return unfoldr<Symbol, DecState>((m, unit, f), (s) { final (mm, ii, ff) = s; final x = mm.symbol(widen(ff, ii)); return (x, (mm.adapt(x), narrow(ii, mm.interval(x)), ff)); }); }

toBitstoFrac の中身はまだ決めていませんが、toFrac (toBits i) ∈ i さえ守れば (24.3) は保証されます。

この新しい encode はまだ「入力を全部読んでから出力を出す」形です。次はこれを 逐次的(incremental) にする方法を考えます。

ストリーミング

stream 関数

次のような stream 関数を考えます。

stream f g s xs = unfoldr step (s, xs) where step (s, xs) = case f s of Just (y, s') → Just (y, (s', xs)) Nothing → case xs of x : xs' → step (g s x, xs') [] → Nothing
Dart // 生産関数 f と消費関数 g を交互に呼び、逐次的に出力を吐き出す。 // f s が (y, s') を返す間は y を出し続け、返せなくなったら入力を 1 つ食う。 Iterable<Y> stream<Y, S, X>( (Y, S)? Function(S) f, S Function(S, X) g, S s0, List<X> xs, ) sync* { var s = s0; var i = 0; while (true) { final r = f(s); if (r != null) { yield r.$1; s = r.$2; } else if (i < xs.length) { s = g(s, xs[i]); i++; } else { return; } } }

この関数は 出力を出したり、入力を読んだり を交互に繰り返します。

  1. まず生産関数 f を呼び、これ以上出力できなくなるまで 出力を吐く
  2. 次に消費関数 g に切り替え、入力を 1 つ読んで 新しい状態 を得る。
  3. 入力がなくなるまで繰り返す。

ストリーミング定理

定理 24.1(ストリーミング定理)
fg が次の ストリーミング条件
f s = Just (y, s') ⇒ f (g s x) = Just (y, g s' x)
を任意の s, x について満たすなら、任意の s と任意の有限リスト xs について
unfoldr f (foldl g s xs) = stream f g s xs
が成り立つ。
何が嬉しいのか ストリーミング条件が成り立てば、「入力を全部消費してから出力を作る」パターン(unfoldr ffoldl g s)を、そのまま「入力を少しずつ読みながら出力を出す」パターン(stream)に置き換えられます。証明は付録にあります。

encode に適用する

toBits をある関数 bit を使って toBits = unfoldr bit と書けるとし、bit が次を満たすとします。

bit i = Just (b, i_b) ⇒ bit (i ▷ j) = Just (b, i_b ▷ j) (24.5)

すると次が言えます。

encode m = stream bit (▷) (0, 1) · intervals m

これで encode逐次的アルゴリズム が得られます。

bit の定義

(24.5) が要求しているのは、「bit i がビット b を出すなら、i のどんな部分区間 i' に対しても bit i' は同じ b を出さねばならない」ということです。これは強い制約で、実質的に次のような定義しか許しません。

bit (ℓ, r) | r ≤ 1/2 = Just (0, (2∗ℓ, 2∗r)) | 1/2 ≤ ℓ = Just (1, (2∗ℓ−1, 2∗r−1)) | otherwise = Nothing
Dart // 区間 i から次のビットを出せるなら (bit, 2 倍に引き伸ばした区間) を返す。 // 1/2 をまたいでいて確定できない場合は null(Haskell の Nothing)。 final _half = Fraction.of(1, 2); final _one = Fraction.of(1); final _two = Fraction.of(2); (Bit, Interval)? bit(Interval i) { final (l, r) = i; if (r <= _half) { return (0, (_two * l, _two * r)); } else if (_half <= l) { return (1, (_two * l - _one, _two * r - _one)); } else { return null; } } // toBits は bit を種にした unfoldr。 Iterable<Bit> toBitsImpl(Interval i) => unfoldr<Bit, Interval>(i, bit);
この定義の直観

ビットを 1 つ出すときの区間の更新は次のように書けます。

(2∗ℓ, 2∗r) = (0, 2) ▷ (ℓ, r) (2∗ℓ−1, 2∗r−1) = (−1, 1) ▷ (ℓ, r)

つまり bit ib を出すとき、bit i = Just (b, jᵦ ▷ i) と書け(j₀ = (0, 2)、j₁ = (−1, 1))、▷ は結合的なので jᵦ ▷ (ij) = (jᵦ ▷ i) ▷ j となります。したがって (24.5) は iᵦ = jᵦ ▷ i と置くだけで満たされます。

toBits の長さの見積もり

toBits i の長さは有限で、次のように押さえられます。

length (toBits (ℓ, r)) ≤ ⌊log₂ 1/(r−ℓ)⌋
なぜか 幅が 1/2 より大きい区間は 1/2 を必ずまたぐので、そこでは bit は何も出しません。さらに 1 ビット出すたびに、次の bit前の区間の 2 倍の幅 の区間に対して呼ばれます。だから 1/2k+1 < r − ℓ ≤ 1/2k なら、多くとも k ビット出したところで止まります。

toFrac の定義

上の toBits と対になる toFrac は次のように定義します。

toFrac = foldr (λ b f → (b+f)/2) (1/2)
Dart // 右畳み込み:bs の末尾に 1 ビット追加し、二進小数として読む。 // 結果は (2n+1) / 2^(k+1)(k = bs.length, n = bs が表す二進整数)。 Fraction toFracImpl(List<Bit> bs) { var f = _half; // 初期値 1/2 for (var k = bs.length - 1; k >= 0; k--) { f = (Fraction.of(bs[k]) + f) / _two; } return f; }

これは「bs の末尾に 1 ビットを追加して、その結果を普通に二進小数として読む」のと同じことです。結果は toFrac bs = (2n+1) / 2k+1 となりますk = bs の長さ、n = bs が表す二進整数)。

pick i ∈ i の直接的な定義

pick = toFrac · toBits は「リストを作る関数」と「リストを消費する関数」の合成なので、中間のリストを消せます。すると次の直接的な定義が得られます。

pick (ℓ, r) | r ≤ 1/2 = pick (2∗ℓ, 2∗r)/2 | 1/2 ≤ ℓ = (1 + pick (2∗ℓ−1, 2∗r−1))/2 | otherwise = 1/2
Dart // toFrac ∘ toBits を融合して中間リストを消した直接定義。 // 再帰の深さは O(log(1/(r-l)))。 Fraction pickDirect(Interval i) { final (l, r) = i; if (r <= _half) { return pickDirect((_two * l, _two * r)) / _two; } else if (_half <= l) { return (_one + pickDirect((_two * l - _one, _two * r - _one))) / _two; } else { return _half; } }

pick ii(実際には 厳密に含まれる)の証明は 不動点帰納法 によります。仮説を仮定してから再帰呼び出しでも成り立つことを示す方法で、本質的には再帰の深さに関する帰納法です。詳しくは演習とされています。

復号を逐次化する話は?

この章ではやらない理由 decode も逐次的に動かせますが、本章では詳しくは扱いません。次章では有限精度の整数演算に基づいてまったく違うアプローチで実装し直すので、ここでの逐次化はどうせ捨てることになるからです。

動かしてみる

ここまでの部品をつなげて、"evergreen" を静的モデルで符号化・復号する例を Dart で走らせてみます。

Dart // 静的モデル:5 文字 e/g/n/r/v をそれぞれ固定区間に対応させる。 class StaticModel implements Model { static final _table = <String, Interval>{ 'e': (Fraction.of(0, 8), Fraction.of(3, 8)), 'g': (Fraction.of(3, 8), Fraction.of(4, 8)), 'n': (Fraction.of(4, 8), Fraction.of(5, 8)), 'r': (Fraction.of(5, 8), Fraction.of(7, 8)), 'v': (Fraction.of(7, 8), Fraction.of(8, 8)), }; @override Interval interval(Symbol x) => _table[x]!; @override Symbol symbol(Fraction f) { for (final e in _table.entries) { final (l, r) = e.value; if (l <= f && f < r) return e.key; } throw StateError('f not in [0,1)'); } @override Model adapt(Symbol x) => this; // 静的モデルなので変えない } void main() { final m = StaticModel(); final text = 'evergreen'.split(''); // 1) 分数版 encode / decode final f = encodeFrac(m, text); print('encoded fraction = $f'); final decoded = decodeFrac(m, f).take(text.length).toList(); print('decoded = ${decoded.join()}'); // evergreen // 2) ビット列版 encode / decode(pick を toFrac∘toBits に置き換える) // pick の実体をここで pickDirect に差し替えて使う想定。 // 参考: encodeBits / decodeBits は toBits / toFrac を使う。 final bits = toBitsImpl(_lastInterval(m, text)).toList(); print('bits = ${bits.join()}'); final back = decodeBits(m, bits).take(text.length).toList(); print('decoded from bits = ${back.join()}'); // evergreen } // テスト用ヘルパ:encode の最終区間だけを取り出す。 Interval _lastInterval(Model m, List<Symbol> xs) { var acc = (Fraction.of(0), Fraction.of(1)); for (final j in intervals(m, xs)) { acc = narrow(acc, j); } return acc; }

最後に

本章と次章の内容は Bird and Gibbons (2003)Stratford (2005) がもとになっています。「使いやすい実装」を書いたのは Witten et al. (1987) です。ハフマン符号やシャノン–ファノ符号は Huffman (1952)Fano (1961)、算術符号化の近年の話は Moffat et al. (1998)Mackay (2003) に詳しく書かれています。

ストリーミング定理は本書で新しく述べたもので、逐次的な符号化を定式化するために作られた ものですが、他にも応用があります(Gibbons (2007))。実践から新しい理論が生まれた良い例です。

参考文献

Bird, R. S. and Gibbons, J. (2003). Arithmetic coding with folds and unfolds. Advanced Functional Programming 4, Volume 2638 of Lecture Notes in Computer Science, ed. J. Jeuring and S. Peyton Jones. Springer-Verlag, pp. 1–26.

Fano, R. M. (1961). Transmission of Information. Cambridge, MA/New York, NY: MIT Press/Wiley.

Gibbons, J. (2007). Metamorphisms: streaming representation-changers. Science of Computer Programming 65, 108–39.

Huffman, D. A. (1952). A method for the construction of minimum-redundancy codes. Proceedings of the Institute of Radio Engineers 40 (9), 1098–101.

Mackay, D. (2003). Information Theory, Learning and Inference Algorithms. Cambridge, UK: Cambridge University Press.

Moffat, A., Neal, R. M. and Witten, I. H. (1998). Arithmetic coding revisited. ACM Transactions on Information Systems 16 (3), 256–94.

Stratford, B. (2005). A formal treatment of lossless data compression. DPhil thesis, Oxford University Computing Laboratory, Oxford, UK.

Witten, I. H., Neal, R. M. and Cleary, J. G. (1987). Arithmetic coding for data compression. Communications of the ACM 30 (6), 520–40.

付録:ストリーミング定理の証明の骨子

ストリーミング定理は、unfoldr に関するもっと一般的な定理に帰着させて示せます。次の 2 条件

h x = Nothing ⇒ f (g x) = Nothing h x = Just (y, x') ⇒ f (g x) = Just (y, g x')

が満たされるとき unfoldr f · g = unfoldr h が成り立つ、というものです。これは unfoldr融合則(fusion law)と呼ばれます。

これを

unfoldr step (s, xs) = unfoldr f (foldl g s xs)

という等式(xs は有限リスト)に適用したときの融合条件は、次のように書き下せます。

step (s, xs) = case f s of Just (y, s') → Just (y, (s', xs)) Nothing → case xs of x : xs → step (g s x, xs) [] → Nothing
step (s, xs) = Nothing ⇒ f (foldl g s xs) = Nothing
step (s, xs) = Just (y, (s', xs''))
⇒ f (foldl g s xs) = Just (y, foldl g s' xs'')

第 1 条件はすぐに確かめられ、第 2 条件は

f s = Just (y, s') ⇒ f (foldl g s xs) = Just (y, foldl g s' xs)

から従います。この最後の主張は、fg がストリーミング条件を満たすという仮定のもとで、xs に関する帰納法で証明できます。