Open12

Rustの型システムはTuring完全

Rust
さんたむさんたむ

Smallfuckという、Brainfuckの各メモリセルのとる値を0/1に制限したような言語のエミュレートでTuring完全を示していく

さんたむさんたむ

まずSmallfuckのプログラム

< | ポインタを戻す
> | ポインタを進める
* | ポインタのさすビットを反転
[ | ポインタの指すビットが0なら対応する]へ、そうでなければ次の指示へ
] | 対応する[に戻る

をRustで普通に実装していく

さんたむさんたむ

次のようなenumでSmallfuckのAST(抽象構文木)を表現できる

enum Program {
    Empty,
    Left(Box<Program>),
    Right(Box<Program>),
    Flip(Box<Program>),
    Loop(Box<(Program, Program)>),
}
さんたむさんたむ

また次のようにすれば実行中のSmallfuckプログラムのメモリ状況を表現できる

struct State {
    ptr: u16,
    bits: [u8; (std::u16::MAX as usize + 1) / 8],
}

これで、16bitで表現できる全てのアドレスに対応するbitを用意することができる。本来Turing完全なシステムは無限のメモリが必要だが、今回はこの実装と型レベルでの実装が一致していることを確認できさえすればいいのでこれでOK

さんたむさんたむ

メモリ状況を操作するために必要なメソッドを揃える

impl State {
    fn get_bit(&self, at: u16) -> bool {
        self.bits[(at >> 3) as usize] & (0x1 << (at & 0x7)) != 0
    }

    fn get_current_bit(&self) -> bool {
        self.get_bit(self.ptr)
    }

    fn flip_current_bit(&mut self) {
        self.bits[(self.ptr >> 3) as usize] ^= 0x1 << (self.ptr & 0x7);
    }
}

2^{16}個のbitをu8型の配列として実装したので、各bitへのアクセスに一工夫必要。(at >> 3) as usizeは目的のbitが含まれているu8型の値のインデックスで、(0x1 << (at & 0x7))はu8型の値の何bit目に目的のbitがあるかを表している。flip_current_bitの実装についてもほとんど同様で、XORはbit反転の役割を果たしている。

さんたむさんたむ

動作確認用のプログラム

fn main() {
    let mut state = State {
        ptr: 0,
        bits: [0; (u16::MAX as usize + 1) / 8],
    };
    state.bits[0] = 0b10000000;

    // Smallfuckのプログラムの例: *[>*]*
    // 1があるセルに辿り着くまで右に進み、通ったセルを1にする
    let program = Program::Flip(Box::new(Program::Loop(Box::new((
        Program::Right(Box::new(Program::Flip(Box::new(Program::Empty)))),
        Program::Flip(Box::new(Program::Empty)),
    )))));
    program.big_step(&mut state);

    // リトルエンディアンなら答えが255になるはず
    println!("{}", state.bits[0]);
}
さんたむさんたむ

型システムにおける単一化(Unification)の動作の説明。Prologのような論理プログラミング言語はこの単一化を基礎に動作しており、それがTuring完全となるのなら、同じく単一化を行っているRustの型システムもTuring完全なのでは？という話を提示している。

さんたむさんたむ

筆者が作成したDSLをRustの構造体やトレイトやimplに展開するtype_operator!マクロの動作を見ながら、SmallfuckをRustの型システムで実装していく。

さんたむさんたむ

次の例をもとに、Smallfuckの状態をRustの型で表現する方法について考えていく。

type_operators! {
    [ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ]
    
    concrete Bit => bool {
        F => false,
        T => true,
    }
}

最初の[ZZ, ZZZ, ZZZZ, ZZZZZ, ZZZZZZ]はRustのマクロが一意な型名を生成できないことに関連するおまじないのようなものなので、ここでは無視する。

さんたむさんたむ

type_operator!はconcreteとdataという2種類の擬似型定義を受け取る。この記事の中ではdataは登場しないが、concreteとの違いは、dataが生成するのはただのマーカートレイトで、下のconcreteの例のように型レベルの値を実際の値に変換するためのメソッド(reify)を持たない点が異なる。

さんたむさんたむ

上の例は次のようなコードに展開される。

pub trait Bit {
    fn reify() -> bool;
}

pub struct T;
pub struct F;

impl Bit for T {
    fn reify() -> bool { true }
}

impl Bit for F {
    fn reify() -> bool { false }
}

Bitsトレイトのreify()メソッドで型レベルの値(T, F)を実際の値に直すことができ、これはSmallfuckの実装を確認する上で役立つ。