かな入力とローマ字入力を定義するver.2

「かな入力とローマ字入力を定義する - tomoemonの日記」の続き
この前の定義だとそもそもかな入力すら正しく定義できなかったので考えなおしてみました。前の記事で言いたかった本題に変わりはありません。

この定義は、日本語入力配列について共通の枠組みの下で形式的に評価や議論ができるようになることを期待して作りました。枠組みは一つではないので、より実用的な枠組みがすでにあったり、新しく作られたら教えていただきたいです。

本題

n個の(入力→出力)の組み合わせを持った日本語入力配列 $J$ を以下のように定義する。
$J = \{(K_1,A_1,S_1),(K_2,A_2,S_2),\ldots,(K_n,A_n,S_n)\}$
$(K_i,A_i,S_i) \in J \hspace{20pt} (0 \leq i \leq n)$
は、キーボードを使った日本語入力システムimに $(K_i,A_i)$ の組を入力すると文字列 $S_i$ を出力する関係を持つ。 $K_i$ はキーの列、 $A_i$ は $K_i$ の各キーをいつまで押し下げ続けるかを表し、 $A_i$ に従って $K_i$ の要素であるキーを順に押し下げていくことでimへの入力を行う。
$im(K_i,A_i) \rightarrow S_i \hspace{20pt} (0 \leq i \leq n)$

$K_i, \hspace{10pt} A_i, \hspace{10pt} S_i$ をそれぞれ以下のように定義する。
$K_i = k_1k_2 \ldots k_l \hspace{20pt} (k_j \subseteq Keys, \hspace{10pt} 1 \leq j \leq l)$
$A_i = a_1a_2 \ldots a_l \hspace{20pt} (a_j \in \{0,1,\ldots,l\}, \hspace{10pt} 1 \leq j \leq l)$
$S_i = s_1s_2 \ldots s_m \hspace{20pt} (s_j \in \Sigma, \hspace{10pt} 1 \leq j \leq m)$
$(l \geq 1, \hspace{10pt} m \geq 1)$
ここで、 $Keys$ はキーボードで押下可能なキーの集合、 $\Sigma$ はすべての文字集合を表す。また、 $a_j \hspace{10pt} (a_j \in A_i)$ は、対応する $k_j \hspace{10pt} (k_j \in K_i)$ のキーを $k_({j+a_j})$ のキーを押すまで下げ続けることを意味する。
同時押しを定義できるようにするため、 $k_j$ は $Keys$ の要素ではなく部分集合（1つ以上のキーの組）と定義している。特に、 $k_j$ が複数のキーの組であるとき、「押し下げる」とは $k_j$ のすべてのキーが押し下げられている状態にすることを表す。