常用的不可定中间语言

  • BARBER LBARBER={⟨M⟩:Mdoes not accept ⟨M⟩}L_{BARBER} = \{ \langle M \rangle : M \text{does not accept } \langle M \rangle \}
  • HALT LHALT={(⟨M⟩,x):M halts on w}L_{HALT} = \{ (\langle M\rangle, x) : M \text{ halts on } w \}
  • ACC LACC={⟨M⟩:M accepts L(M)}L_{ACC} = \{ \langle M \rangle : M \text{ accepts } L(M) \}

单string停机问题

虽然不能解决通用停机问题，但是我们是否可以解决单string停机问题？即对于给定的一个string，判断一个特定的图灵机是否能停机。从简单的角度考虑，我们来看语言 Lϵ−HALTL_{\epsilon-HALT} 是否可决定
如果我们要用到图灵归纳的方法，用不可定推导不可定的推导方向应该是 LHALT≤TLϵ−HALTL_{HALT}\le_T L_{\epsilon-HALT}
那么我们就需要假设一个预言机(oracle) Dϵ−HALTD_{\epsilon-HALT} 能解决 Lϵ−HALTL_{\epsilon-HALT} ，那么我们就可以构造一个图灵机 DHALTD_{HALT} 来解决 LHALTL_{HALT}
并且我们的老演员 LHALTL_{HALT} 是 DHALTD_{HALT} 的预言机
我们需要利用oracle 来构建 LHALTL_{HALT} 即判断 M(x)M(x) 是否停机

Dϵ−HALTD_{\epsilon-HALT} 的功能

  • input: ⟨M⟩\langle M\rangle
  • logic: 若 M(ϵ)M(\epsilon) 停机，则 accept；否则 reject

DHALTD_{HALT} 的功能

  • input: (⟨M⟩,x)(\langle M\rangle, x)
    从预言机的特性来看，似乎与输入的string x 无关，那么我们就要强行将 xx 写入到 MM 中，再将其传入 Dϵ−HALTD_{\epsilon-HALT} 中，才能用上 xx
    即令 Mx(w)M_x(w) 为新图灵机，满足 Mx(w)M_x(w) halts 对于 w=ϵw = \epsilon, 而 Mx(w)M_x(w) loop 对于 w≠ϵw \neq \epsilon

\begin{align*} (\langle M\rangle, x) \in L_{HALT} \Leftrightarrow & M(x) \text{ halts} \\ \Leftrightarrow & M_x(w) \text{ halts for any string } w \\ \Leftrightarrow & D_{\epsilon-HALT}(\langle M_x\rangle) \text{ accept} \\ \Leftrightarrow & D_{HALT}(\langle M\rangle, x) \text{ accept} \end{align*}

从上面的这个例子我们可以看出，如果我们有一个预言机能判断某个问题的子集（尤其是单个元素的判定机），我们就可以将原图灵机的输入 (⟨M⟩,x)(\langle M \rangle, x) 转化为新图灵机的输入 ⟨Mx⟩\langle M_x \rangle ，从而利用预言机来解决原问题

例2: LAccL_{Acc} 判定 L376L_{376}

假设语言 L376={⟨M⟩:M accepts 376}L_{376} = \{ \langle M \rangle : M \text{ accepts } 376 \} 如何证明其不可判定?

LAccL_{Acc} 的硬码机特点

由于要用到 undecidable 的归纳方向, LAccL_{Acc} 必然是在图灵归纳的左边, 那么我们的归纳等式必然有形如 (⟨M⟩,x)∈LAcc⇔M(x) accepts(\langle M\rangle, x) \in L_{Acc} \Leftrightarrow M(x) \text{ accepts} 的开头
我们称形如 Mx(w)M_x(w) 的图灵机为硬码机，即其在不同 ww 的输入上有一致的行为
那么对于 (⟨M⟩,x)∈LAcc(\langle M\rangle, x) \in L_{Acc} ，可以得到 M(x)M(x) accepts，即 Mx(w)M_x(w) accepts for any ww
那么如果要判定一个新的语言，我们就可以用特定输入来进行构造
如果是 L376L_{376}, 那么我们就可以构造 Mx(376)M_x(376), 这个输入必定 accept 从而得到预言机 D376(⟨Mx⟩)D_{376}(\langle M_x\rangle) 必定 accept (这里对于不同的预言机其输出可能是 必定 reject, 但是输出是确定的)
那么我们的 DAccD_{Acc} 就可以根据此结果 accept
而构造的图灵机形如:

1
2
3
4
5
6
7
8
def D_Acc(M, x):
	# 首先构造 M_x(376)
	def M_x(w):
	    return M(x)
	def D_376(M_x):
		return M_x(376)
    # 判断 M_x(376) 是否 accept
    return D_376(M_x)

L∅L_{\varnothing} 不接受型语言

language L∅={⟨M⟩:L(M)=∅}L_{\varnothing} = \{ \langle M \rangle : L(M) = \varnothing \}
即 (⟨M⟩)∈L∅(\langle M\rangle) \in L_{\varnothing} 当且仅当 M(x)M(x) rejects for all xx

例3: L∅L_{\varnothing} 判定 LEQL_{EQ}

假设语言 LEQ={⟨M1⟩,⟨M2⟩:L(M1)=L(M2)}L_{EQ} = \{ \langle M_1\rangle,\langle M_2 \rangle : L(M_1) = L(M_2) \} 如何证明其不可判定?
根据图灵归纳不可定语言的方向性，我们要证明 L∅≤TLEQL_{\varnothing} \le_T L_{EQ}
那么长等式的开头会形如 ⟨M⟩∈L∅⇔M(x) does not accept any string x\langle M\rangle \in L_{\varnothing} \Leftrightarrow M(x) \text{ does not accept any string } x
对于 LEQL_{EQ}, 我们假设有预言机 DEQ:DEQ(⟨M1⟩,⟨M2⟩)D_{EQ}: D_{EQ}(\langle M_1\rangle,\langle M_2 \rangle) 若对于任意 xx 输入，M1(x)=M2(x)M_1(x) = M_2(x) 则 accept
我们的目标是证明 ⟨M⟩∈L∅⇔M∅(x)\langle M\rangle\in L_\varnothing \Leftrightarrow M_{\varnothing}(x) does not accept any string xx
所以我们要用到 DEQD_{EQ} 来判断是不是一个输入的 ⟨M⟩\langle M\rangle 和标准的 M∅M_\varnothing 是否相等

1
2
3
4
5
6
7
def D_empty(M):
  def M_empty(x):
    return False
  def D_EQ(M, M_empty):
	for x in Sigma_star:  # Sigma_star is all string set
      return and_all (M(x) == M_empty(x))
  return D_EQ(M, M_empty)

硬码机类问题的统一思路

什么时候用硬码机？

当我们要用到图灵归纳，且目标语言为已知语言的子集，或者当前语言和目标语言的判断类型不一致（例如 用 halt 推导 acc类问题，前者返回的是 是否 halt, 后者需要的只有 acc 或者 rej

长等式的两端

首先要构造一个长等式，最左端是 ⟨M⟩∈Lx\langle M\rangle \in L_x, 最右端是 Dx(⟨M⟩)D_x(\langle M \rangle) accepts

左向右

从左向右的思路是 ⟨M⟩∈Lx⇔M(x)\langle M\rangle\in L_x\Leftrightarrow M(x) accepts/halts 之类

右向左

从右向左的思路是 Dx(⟨M⟩)D_x(\langle M \rangle) accepts ⇔Hx(s)\Leftrightarrow H_x(s) accepts 之类(即利用预言机返回值进行正向返回或者反向返回)
再前一步一定是判定 ss 是否属于 LxL_x 问题

硬码机的构造和应用

Tiling the Plane 问题

问题描述

给定一个二维无限平面，和一个有限的集合 TT, 问是否可以用 TT 中的图形无重叠地覆盖整个平面(设图形可以旋转)
tiling_the_plane.png

王浩大师简介

王浩是民国时期的数学家，本科毕业于西南联大数学系，硕士毕业于清华大学哲学系（师从冯友兰、金岳霖），博士毕业于哈佛大学逻辑学

王浩法解决 平铺问题

假设 TT 中的图形每条边各有一个颜色，两个图形的边可以重叠当且仅当:

  • 两个图形的边颜色相同
    拼接后未连接的部分边缘显示为白色，且正方形拼接后不可旋转
    然后我们尝试用 Mϵ−HALTM_{\epsilon-HALT} 来图灵归纳平铺问题
    定义预言机 DTileD_{Tile} 能判断 TT 是否可以平铺整个平面, 那么我们需要令 Mϵ−HALTM_{\epsilon-HALT} 利用 DTileD_{Tile} 来解决
    那么我们首先证明如下命题:
    TT 可以平铺第一象限 ⇔M(ϵ)\Leftrightarrow M(\epsilon) loops