Weihrauch還元

Weihrauch reduction

定義

$ \mathcal A\colon X \rightrightarrows Y $ \mathcal B : V \rightrightarrows Wについて，

$ \mathcal B \preceq_W \mathcal A \iff

計算可能な$ \Phi\colon V \to X, $ \Psi\colon X \times Y \to Wが存在して，

$ \forall v \in V\, \, \forall y \in Y\, [y \in \mathcal A(\Phi(v)) \to \Psi(v,y) \in \mathcal B(v)]

を満たす．

$ \Psi(v,y)を$ vに依存しないものに制限したとき強Weihrauch還元可能である．

$ \mathcal B \preceq_{sW} \mathcal A

$ A(x^{X},y^{Y}), $ B(v^V,w^W)を次を満たす論理式とする．

$ A(x, y) \iff y \in \mathcal A(x)

$ B(v,w) \iff w \in \mathcal B(v)

Weihrauch還元$ \mathcal B \le_W \mathcal Aの witness $ \Phi, \Psiは論理式

$ \forall x^X \exists y^Y A(x,y) \to \forall v^V \exists w^W B(v,w)

のダイアレクティカ解釈における witness である．

次の形に変形する．

$ \exists v \forall w \lnot B(v,w) \to \exists x \forall y \lnot A(x,y)

$ \exists \Phi^{V \to X}\, \exists \Psi^{X \times Y \to W}\, \forall v^V \,\forall y^Y [\lnot B(v, \Psi v y) \to \lnot A(\Phi v, y)]

よって，

$ \exists \Phi^{V \to X}\, \exists \Psi^{X \times Y \to W}\, \forall v^V \,\forall y^Y [A(\Phi v, y) \to B(v, \Psi v y)]