No.2540 同値性判定

注意

この問題の実行時間制限は2500[ms]です。

問題文

まずは用語の説明です。ここでは命題変数と言ったら $P$ に $6$ 未満の非負整数の添字をつけた文字列、すなわち $P_0, P_1, P_2, P_3, P_4, P_5$ のいずれかを表します。

良い命題とは、 $1$ 個以上の命題変数に論理演算 $\land, \lor, \Rightarrow$ を $0$ 回以上適用して得られる命題のことです。ただし構文の曖昧さをなくすため、論理演算の適用時には両側をカッコ $(,)$ でくくります。例えば $(P_0 \land P_0)$ は良い命題ですが、 $\neg P_0$ は良い命題ではありません。

以下、命題を知らない人向けに良い命題の定義について再帰を用いた説明を書きます。（クリックで開く）

命題変数とカッコ $(, )$ と記号 $\land, \lor, \Rightarrow$ のみからなる文字列が良い命題であるということを以下のように再帰的に定めます：

命題変数は良い命題である。
任意の良い命題 $a$ と $b$ に対し、文字列 $($ と $a$ と $\land$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \land b)$ は良い命題である。
任意の良い命題 $a$ と $b$ に対し、文字列 $($ と $a$ と $\lor$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \lor b)$ は良い命題である。
任意の良い命題 $a$ と $b$ に対し、文字列 $($ と $a$ と $\Rightarrow$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \Rightarrow b)$ は良い命題である。

以下、集合などの再帰的定義について詳しくない人向けの説明を書きます。（クリックで開く）

$X$ を集合とします。例えば $X$ は特定の文字のみからなる文字列の集合などです。今回説明するのは、 $X$ の部分集合などを再帰的に定義する際の数学特有の言い回しです。

例えば $X$ の要素 $c$ と非負整数 $n_0,m_0,n_1,m_1$ と写像 $F_0 \colon X^{n_0} \times X^{m_0} \to X$ と $F_1 \colon X^{n_1} \times X^{m_1} \to X$ を用いて次のような書き方をすることがあります：

$X$ の部分集合 $X_0$ を以下のように再帰的に定める：

$c \in X_0$ である。

任意の $(a,t) \in X_0^{n_0} \times X^{m_0}$ に対し、 $F_0(a,t) \in X_0$ である。

任意の $(a,t) \in X_0^{n_1} \times X^{m_1}$ に対し、 $F_1(a,t) \in X_0$ である。

これはあくまで例であって、今回は $3$ つの条件としましたが一般には $3$ つとは限りませんし、写像を用いるのではなく関係を用いることもあります。再帰的定義の一般の定式化^{[1] 6.1.1 Definition}はかなり抽象的なので、今回はこの問題を解く上で必要な例のみを考えることにします。

ここで重要なのは、この定義文は $X_0$ が単に $3$ つの条件を全て満たす $X$ の任意の部分集合であるという意味を持つのではなく、次の定義文を表すということです：^{[1] 6.1.2 Definitionおよびその直後の段落参照}

$X$ の部分集合 $X_0$ を、以下の $3$ 条件を全て満たす $X$ の部分集合 $Y$ 全体の共通部分と定める：

$c \in Y$ である。

任意の $(a,t) \in Y^{n_0} \times X^{m_0}$ に対し、 $F_0(a,t) \in Y$ である。

任意の $(a,t) \in Y^{n_1} \times X^{m_1}$ に対し、 $F_1(a,t) \in Y$ である。

$Y = X$ とすると確かに上の $3$ 条件を満たすので、条件を満たす $Y$ 全体の集合は空でなく共通部分が定義されます。そして $X_0$ は $3$ 条件を満たす $Y$ のうち最小のものである、ということが結果的に従います。

このように、部分集合の再帰的定義はただの条件の列挙ではなく最小性も含意するよう約束されていることに注意しましょう。ただしこれはあくまで再帰的定義に限った約束であり、通常の定義では最小性はもちろん含意されませんし、そもそも再帰的定義のような自己言及を通常の定義で行うと多くの場合循環論法となり定義が破綻します。

さて、 $X$ 上の $1$ 項関係は $X$ の部分集合と等価であるため、 $X$ 上の $1$ 項関係の再帰的定義においても同様の規則が適用されます。具体的には、

$X$ の要素が良い項であるということを以下のように再帰的に定める：

$c$ は良い項である。

任意の $(a,t) \in X^{n_0} \times X^{m_0}$ に対し、 $a$ の任意の成分が良い項であるならば、 $F_0(a,t)$ も良い項である。

任意の $(a,t) \in X^{n_1} \times X^{m_1}$ に対し、 $a$ の任意の成分が良い項であるならば、 $F_1(a,t)$ も良い項である。

のように「良い項である」という $1$ 項関係の再帰的定義を書いた場合、これは「良い項である」という述語が $3$ 条件を満たす任意の $1$ 項関係を表すという意味ではありません。上の定義文は次の定義文と等価なものになります：

$X$ の要素 $x$ が良い項であるということを、以下の $3$ 条件を全て満たす $X$ の任意の部分集合 $Y$ に対し $x \in Y$ が成り立つということと定める：

$c \in Y$ である。

任意の $(a,t) \in Y^{n_0} \times X^{m_0}$ に対し、 $F_0(a,t) \in Y$ である。

任意の $(a,t) \in Y^{n_1} \times X^{m_1}$ に対し、 $F_1(a,t) \in Y$ である。

以上を踏まえると、今回の良い命題の再帰的定義は次の定義文と等価です：

命題変数とカッコ $(, )$ と $\land, \lor, \Rightarrow$ のみからなる文字列 $s$ が良い命題であるということを、命題変数とカッコ $(, )$ と $\land, \lor, \Rightarrow$ のみからなる文字列のみからなる任意の集合 $Y$ に対し $Y$ が以下の $3$ 条件を全て満たすならば $s \in Y$ が成り立つということと定める：

命題変数は $Y$ の要素である。

$Y$ の任意の要素 $a$ と $b$ に対し、文字列 $($ と $a$ と $\land$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \land b)$ は $Y$ の要素である。

$Y$ の任意の要素 $a$ と $b$ に対し、文字列 $($ と $a$ と $\lor$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \lor b)$ は $Y$ の要素である。

$Y$ の任意の要素 $a$ と $b$ に対し、文字列 $($ と $a$ と $\Rightarrow$ と $b$ と $)$ をこの順に結合して得られる文字列 $(a \Rightarrow b)$ は $Y$ の要素である。

元の言い回しと比べてだいぶ複雑な言い回しとなりましたね。このような複雑な言い回しを避けるために、数学では今回紹介した簡潔な言い回しが定義され採用されているわけです。

例えば後で参考文献として挙げる

[1] における $1$ 項関係「be an $\mathcal{L}$ -term」や「be an $\mathcal{L}$ -formula」の再帰的定義など
[2] における集合 $T$ および $1$ 項関係「be a principal term」の再帰的定義など
[3] における集合 $B(\alpha,\beta)$ や $\textrm{K}_{\kappa}(\gamma)$ の再帰的定義など

で実際にそういった言い回しが採用されています。

参考文献

W. Pohlers, "Proof Theory - The first step into impredicativity", Springer, 2010.
W. Buchholz, "A New System of Proof-Theoretic Ordinal Functions", Annals of Pure and Applied Logic 32 (1986), pp. 195--207.
M. Rathjen, "Ordinal Notations Based on a Weakly Mahlo Cardinal", Archive for Mathematical Logic 29 (1990), pp. 249--263.

入力の最初に $2$ 個の正整数 $N, Q$ が与えられます。

$N$ 未満の各非負整数 $k$ に対し良い命題 $X_k$ が $P_{k \bmod 6}$ として与えられています。ただし $k \bmod 6$ は $k$ を $6$ で割った余りを表します。

以下で説明する $Q$ 個のクエリを与えられた順に処理してください。

各クエリは、

$N$ 未満の非負整数 $h$
landかlorかRightarrowのいずれかの文字列 $o$
$0 \leq \ell \leq r < N$ を満たす整数 $\ell,r$
$0 \leq \ell' \leq r' < N$ を満たす整数 $\ell',r'$

の組 $(h,o,\ell,r,\ell',r')$ です。クエリ $(h,o,\ell,r,\ell',r')$ は以下のように処理してください：

まず良い命題 $Y$ を、この時点での $X_h$ の値と定める。
次に論理演算 $O$ を、 $o$ がlandならば $\land$ 、lorならば $\lor$ 、Rightarrowならば $\Rightarrow$ と定める。
そして $\ell \leq k \leq r$ を満たす各非負整数 $k$ に対し、 $X_k$ の値を $(X_k O Y)$ の値に置き換えることで更新する。
最後に更新後の値について「 $\ell' \leq k_0 < k_1 \leq r'$ を満たす非負整数 $k_0, k_1$ であって $X_{k_0}$ と $X_{k_1}$ が同値であるものが存在する」という命題の真偽を判定する。（以下、この真偽をこのクエリに対する回答と呼ぶ）

$Y$ の値は各クエリ処理の最初に固定され、 $\ell \leq k \leq r$ を満たす各非負整数 $k$ に対する $X_k$ の更新では変化しないことに注意してください。

２つの命題が同値であることの定義はこちらです。（クリックで開く）

まず論理に詳しくない人向けの大雑把な説明をします。命題 $a$ と $b$ に対し、「 $a$ と $b$ が同値である」とは

$a$ が真であると仮定すると $b$ が真である。
$b$ が真であると仮定すると $a$ が真である。

の両方が成り立つということだと思ってください。

例えば $P_1 \land P_1$ と $P_1 \lor P_1$ は同値な命題です。実際 $P_1 \land P_1$ が真であると仮定すると $P_1$ が真となるので $P_1 \lor P_1$ も真となり、逆に $P_1 \lor P_1$ が真であると仮定するとやはり $P_1$ が真となるので $P_1 \lor P_1$ も真となります。一方で $P_1$ と $P_2$ は同値ではありません。実際 $P_1$ が真であるとしても $P_2$ は必ずしも真ではありません。

次に論理に詳しい（古典論理と直観主義論理の違いを知っている）人向けの厳密な説明をします。ここでは「 $a$ と $b$ が同値である」ということを、

古典論理において、 $a$ を仮定すると $b$ が証明可能である。
古典論理において、 $b$ を仮定すると $a$ が証明可能である。

の両方が成り立つことと定義します。従って両向きの含意を証明するためには背理法、二重否定除去則、排中律はいずれも使って構いません。

入力

以下、 $Q$ 以下の任意の正整数 $q$ に対し $q$ 個目のクエリを $(h_q,o_q,\ell_q,r_q,\ell'_q,r'_q)$ と置きます。

入力は以下の形式で標準入力から $1 + Q$ 行で与えられます：

$1$ 行目に $N, Q$ が半角空白区切りで与えられます。
$Q$ 以下の各正整数 $q$ に対し、 $1 + q$ 行目に $h_q,o_q,\ell_q,r_q,\ell'_q,r'_q$ が半角空白区切りで与えられます。

 $N$   $Q$ 
 $h_1$   $o_1$   $\ell_1$   $r_1$   $\ell'_1$   $r'_1$ 
 $\vdots$ 
 $h_Q$   $o_Q$   $\ell_Q$   $r_Q$   $\ell'_Q$   $r'_Q$

制約

この問題はeasy版の制約とhard版の制約が設定されています。easy版の制約を満たすケースで全て AC が取れていればその提出自体が AC として扱われます。つまりeasy版の制約を満たさずhard版の制約を満たすケースはジャッジされますが提出自体のステータスには影響しません。easy版の制約で物足りない人やコンテスト中に時間を持て余した人はぜひhard版の制約に挑戦してみてください。

easy版の入力は以下の制約を満たします：

$N$ は $1 \leq N \leq 10^6$ を満たす整数である。
$Q$ は $1 \leq Q \leq \textcolor{blue}{10^4}$ を満たす整数である。
$Q$ 以下の任意の正整数 $q$ に対し、

$h_q$ は $0 \leq h < N$ を満たす整数である。
$o_q$ はlandかlorかRightarrowのいずれかの文字列である。
$\ell_q, r_q$ は $0 \leq \ell_q \leq r_q < N$ を満たす整数である。
$\ell'_q, r'_q$ は $0 \leq \ell'_q \leq r'_q < N$ を満たす整数である。

$Q$ 以下の各正整数 $q$ を渡る $r'_q - \ell'_q$ の総和は $\textcolor{blue}{10^7}$ 以下である。

hard版の制約はこちらです。（クリックで開く）

入力は以下の制約を満たします：

$N$ は $1 \leq N \leq 10^6$ を満たす整数である。
$Q$ は $1 \leq Q \leq \textcolor{red}{10^5}$ を満たす整数である。
$Q$ 以下の任意の正整数 $q$ に対し、

$h_q$ は $0 \leq h < N$ を満たす整数である。
$o_q$ はlandかlorかRightarrowのいずれかの文字列である。
$\ell_q, r_q$ は $0 \leq \ell_q \leq r_q < N$ を満たす整数である。
$\ell'_q, r'_q$ は $0 \leq \ell'_q \leq r'_q < N$ を満たす整数である。

$Q$ 以下の各正整数 $q$ を渡る $r'_q - \ell'_q$ の総和は $\textcolor{red}{10^8}$ 以下である。

なおhard版に挑戦する際は高速な言語の使用を推奨します。writer解の実行時間はc++では190[ms]とcLayでは167[ms]ですが、Python3とPyPy3ではいずれも10000[ms]以内に実行が終わらず TLE となります。

出力

$Q$ 以下の各正整数 $q$ に対し、 $q$ 個目のクエリに対する回答が真ならばYesを、偽ならばNoを $q$ 行目に出力してください。

最後に改行してください。

サンプル

サンプル1

入力

1 1
0 land 0 0 0 0

出力

No

最初は $X_0 = P_0$ として与えられています。

クエリ $(h_1,o_1,\ell_1,r_1,\ell'_1,r'_1)$ の各成分が半角空白区切りで0 land 0 0 0 0と与えられます。 $Y$ がこの時点での $X_0$ すなわち $P_0$ と定義され $X_0$ の値が

$(X_0 \land Y) = (P_0 \land P_0)$

に置き換わります。更新後の $X_0 = (P_0 \land P_0)$ についてクエリに回答します。

ここで、 $0 = \ell'_1 \leq k_0 < k_1 \leq r'_1 = 0$ を満たす整数の組 $(k_0, k_1)$ がそもそも存在しません。従ってクエリへの回答は偽であり、Noと出力します。

サンプル2

入力

7 1
3 lor 1 5 0 6

出力

Yes

最初は $(X_0,X_1,X_2,X_3,X_4,X_5,X_6) = (P_0,P_1,P_2,P_3,P_4,P_5,P_0)$ として与えられています。 $X_6$ が $P_0$ であることに注意しましょう。

クエリ $(h_1,o_1,\ell_1,r_1,\ell'_1,r'_1)$ の各成分が半角空白区切りで3 lor 1 5 0 6と与えられます。 $Y$ がこの時点での $X_3$ すなわち $P_3$ と定義され $(X_0,X_1,X_2,X_3,X_4,X_5,X_6)$ の値が

$(X_0,(X_1 \lor Y),(X_2 \lor Y),(X_3 \lor Y),(X_4 \lor Y),(X_5 \lor Y),X_6) = (P_0,(P_1 \lor P_3),(P_2 \lor P_3),(P_3 \lor P_3),(P_4 \lor P_3),(P_5 \lor P_3),P_0)$

に置き換わります。更新後の $(X_0,X_1,X_2,X_3,X_4,X_5,X_6) = (P_0,(P_1 \lor P_3),(P_2 \lor P_3),(P_3 \lor P_3),(P_4 \lor P_3),(P_5 \lor P_3),P_0)$ についてクエリに回答します。

今回は $0 = \ell'_1 \leq k_0 < k_1 \leq r'_1 = 6$ を満たす整数の組 $(k_0, k_1)$ として $(0,6)$ が選べます。 $X_{k_0} = X_0 = P_0$ かつ $X_{k_1} = X_6 = P_0$ であるので命題として $X_0$ と $X_6$ は一致し、特に $X_0$ と $X_6$ は同値です。従ってクエリへの回答は真であり、Yesと出力します。

サンプル3

入力

2 2
1 Rightarrow 0 1 0 1
1 Rightarrow 0 0 0 1

出力

No
Yes

最初は $(X_0,X_1) = (P_0,P_1)$ として与えられています。

まずクエリ $(h_1,o_1,\ell_1,r_1,\ell'_1,r'_1)$ の各成分が半角空白区切りで1 Rightarrow 0 1 1 1と与えられます。 $Y$ がこの時点での $X_1$ すなわち $P_1$ と定義され $(X_0,X_1)$ の値が

$((X_0 \Rightarrow Y), (X_1 \Rightarrow Y)) = ((P_0 \Rightarrow P_1), (P_1 \Rightarrow P_1))$

に置き換わります。更新後の $(X_0,X_1) = ((P_0 \Rightarrow P_1), (P_1 \Rightarrow P_1))$ についてクエリに回答します。

$0 = \ell'_1 \leq k_0 < k_1 \leq r'_1 = 1$ を満たす整数の組 $(k_0, k_1)$ は $(0,1)$ に限られ、この $(k_0,k_1)$ に対しては $(X_{k_1} \Rightarrow X_{k_0})$ が必ずしも成り立たないので $X_0$ と $X_1$ は同値ではありません。従ってこのクエリへの回答は偽であり、Noと出力します。

次にクエリ $(h_2,o_2,\ell_2,r_2,\ell'_2,r'_2)$ の各成分が半角空白区切りで1 Rightarrow 0 0 0 1と与えられます。 $Y$ がこの時点での $X_1$ すなわち $(P_1 \Rightarrow P_1)$ と定義され $(X_0,X_1)$ の値が

$((X_0 \Rightarrow Y),X_1) = (((P_0 \Rightarrow P_1) \Rightarrow (P_1 \Rightarrow P_1)), (P_1 \Rightarrow P_1))$

に置き換わります。更新後の $(X_0,X_1) = (((P_0 \Rightarrow P_1) \Rightarrow (P_1 \Rightarrow P_1)), (P_1 \Rightarrow P_1))$ についてクエリに回答します。

今回は $0 = \ell'_1 \leq k_0 < k_1 \leq r'_1 = 1$ を満たす整数の組 $(k_0, k_1)$ として $(0,1)$ が選べます。

まず $X_{k_1} = X_1 = (P_1 \Rightarrow P_1)$ は常に成り立つため、 $(Z \Rightarrow X_{k_1})$ は良い命題 $Z$ によらず成り立ち、特に $(X_{k_0} \Rightarrow X_{k_1})$ も成り立ちます。

次に $X_{k_0} = X_0 = (P_0 \Rightarrow (P_1 \Rightarrow P_1))$ は $(P_0 \Rightarrow X_{k_1})$ に他ならないため、 $X_{k_1}$ が成り立つならば $X_{k_0}$ も成り立ちます。すなわち $(X_{k_1} \Rightarrow X_{k_0})$ が成り立ちます。

以上より $(X_{k_0} \Rightarrow X_{k_1})$ と $(X_{k_1} \Rightarrow X_{k_0})$ の両方が成り立つことが分かったので、 $X_{k_0}$ と $X_{k_1}$ は同値です。従ってこのクエリへの回答は真であり、Yesと出力します。

yukicoder