小さな計算体系を簡単に作れる言語 ron の紹介

言語実装 Advent Calendar 2022 の18日目の記事です。

小さな計算体系（あるいは言語）を簡単に作れることを目指す言語を ron という名前で作っています。
https://github.com/mitsuchi/ron

ron のプログラムの雰囲気はこんな感じです。

op 20 : let rec _ _ = _ in _

# let rec による関数定義
c |- let rec f x = e1 in e2 => v {
    c, f = [c |- f = x -> e1] |- e2 => v
}

# 実際にフィボナッチ関数を定義して計算してみる（v = 34 が返る）
main {
    0 |- let rec fib n = if n < 2 then n else fib (n - 1) + fib (n - 2) in fib 9 => v
}

これは OCaml風の言語を定義するプログラムの抜粋です。後半の main と書かれた部分でフィボナッチ数列を計算する関数を定義していて、実行すると数列の9番目である 34 が返ります。

ron は以下のような特徴を持っています。

• 論理型言語（実際は Prolog に翻訳しているだけ）
• mixfix 記法によって自然な文法で推論規則が書ける
• main { ... } のような、C言語っぽい見た目

以下では、実際に小さな言語を作りながら ron の使い方を紹介したいと思います。

ステップ１：自然数の足し算だけができる言語

まずは自然数の足し算だけができる言語をつくります。短いのでまず全部のコードをお見せすると次のとおりです。

# 関数を宣言
op 70 : S _
op 50 : _ + _ = _
 
# 規則1
Z + n = n

# 規則2
(S n) + m = S k {
    n + m = k
}

# 1 + 2 を計算する（x = S S S Z が返る。つまり 3）
main {
    S Z + S S Z = x
}

ron では、おおまかにいうと次の手順で言語を定義します。

1. 言語が扱うデータ（例：自然数）を定義する
2. データが計算（例：足し算）によって満たす関係を定義する
3. 実際に問い合わせをする

記法や特徴が違うものの、ron の中身はほぼ Prolog です。なので以下で紹介することはだいたい Prolog の特徴なのですが、なじみがない方もおられると思います。ここでは論理型言語の知識を仮定せず、上記のコードの内容を説明します。

自然数を定義する

いまは自然数の上の足し算を定義したいので、まずは自然数を定義する必要があります。普通の言語では基本的なデータ型として int のような数が用意されているのですが、ron には特にないので自分で用意することになります。

そのための方法が、項を関数によって組み合わせて構造を作ることです。
項とは次のものを指します。

1. アトム：A, B, apple, bar など。英大文字1文字か、小文字で始まる2文字以上の文字列。
2. 変数：x, y, x1, y1 など。英小文字1文字か、その後に数字が続く文字列。
3. 項を関数によって組み合わせたもの：S Z, if true then x else y など。

1.と2.を基本的な項とし、3.によって項を組み合わせた項をつくるわけです。ただ、3.でいう関数のニュアンスがちょっと不思議かもしれません。

ron での関数とは、項を受け取って単にそれらを組み合わせた項を作るものです^[1]。

たとえば S _ という関数を項 t に適用すると項 S t になります。S _ を Z に適用すると S Z になり、S _ を S Z に適用すると S (S Z) になります。
また、if _ then _ else _ という関数は、true, S Z, y に適用すると if true then S Z else y になります。つまり関数によっていくらでも複雑な項を作ることができるわけです。

ron では関数 S _ を次のように宣言することができます。

op 70 : S _

70の部分は優先順位を表しています（後で説明します）。また、デフォルトで右結合となります。つまり S (S Z) は S S Z と書くことができるわけです。そこで、以下では S に関するカッコは省略することにします。

項 Z と関数 S _ を使うと、自然数を次のように表現することができます。

0 : Z
1 : S Z
2 : S S Z
3 : S S S Z
...

つまりペアノ自然数です。数 0 にあたる Z はアトムなので項の定義1により項です。数 1 にあたる S Z は 項 Z に関数 S _ を適用したものなので項です。2 以上も同様に項になります。

以上で自然数が用意できました。

足し算の満たす関係を定義する

つぎは、足し算が満たす関係を述語によって定義していきます。述語は、項を受け取ってそれらを組み合わせた項をつくるという点で関数と同じですが、項が特定の関係を満たすことの表明でもあります。

たとえば「a に b を足すと c になる」という関係を _ + _ = _ という述語で表すことにしましょう。すると「1 に 2 を足すと 3 になる」という関係は、 _ + _ = _ に S Z, S S Z, S S S Z を適用した結果として S Z + S S Z = S S S Z という項で表されます。

ron では述語 _ + _ = _ を関数と同じように宣言できます。

op 50 : _ + _ = _

50の部分は優先順位です。さきほどの S _ では 70 でしたので S のほうが結合が強いことになります。そこで S Z + S Z = S S Z とさえ書けば (S Z) + (S Z) = (S S Z) と解釈されることになります。

「a に b を足すと c になる」という関係が実際に満たされるかを推論できるようにするために、推論の規則を定義します。規則は一般に次の形をしています。

結論

もしくは

結論 {
   前提1
   前提2
   ...
}

前者は、常にその結論が成り立つことを表します。後者は、前提がすべて満たされるときに結論が導かれることを表しています。結論や前提はすべて述語を使って表します。

たとえば、一般に 0 + n = n はつねに成り立つ関係です。いまの表記では次のように書けます。

規則1

Z + n = n

また、n + m = k ならば (n + 1) + m = (k + 1) も成り立つので、次のように書けることになります。

規則2

(S n) + m = S k {      # 結論
    n + m = k          # 前提
}

上の2つの規則があれば、S Z + Z = S Z が正しい関係かどうかを次の手順で機械的に推論することができます。が、細かい話なので折りたたんでおきます。

推論の詳細

1. 結論が S Z + Z = S Z という形にマッチする規則があるか探す。
2. 規則2の結論で n $\larr$ Z, m $\larr$ Z, k $\larr$ Z とすればマッチすることがわかる。
3. その場合に規則2の前提を満たすかどうか調べる
4. Z + Z = Z が真かどうかを調べればよいので、結論がその形にマッチする規則を探す
5. 規則1の結論で、n $\larr$ Z とすればマッチすることがわかる。
6. 規則1はマッチした時点で真なので、つまり手順3でいう前提は真、よって手順2でいう結論も真。よって S Z + Z = S Z も真。

上の2つの規則で推論できるポイントは、各ステップで推論がより小さな形の項に対する推論に帰着できるようになっていたことです。
実際、規則2に含まれる述語の最初の引数を見ると、結論の S n に対して仮定では n と、より小さな形になっています。そして規則1で最初の引数が最も小さい形（Z）の場合について記述しているので、これが帰納法でいうベースケースになってうまくいくというわけです。

問い合わせをする

ここまでで足し算を計算するための準備ができました。実際に 1 + 2 を計算するためには問い合わせを行います。問い合わせとは、述語に項を適用した項（例：Z + S Z = S Z）が真となるかを ron に推論させることです。項が変数を含む場合には（例：S Z + S S Z = x）、真となる場合の変数の値も併せて返します。

ron では結論が main である規則がある場合、main に対する問い合わせを自動的に行います。たとえば main が次のように定義されている場合、

main {
    S Z + S S Z = x
}

S Z + S S Z = x が真になるかが推論されます。その結果、x $\larr$ S S S Z とすれば真になることが分かり、x = S S S Z と表示されます。つまり 1 + 2 が 3 と計算されたことになります。

以上でこの章の冒頭のプログラムを説明できました。ron の基本的な概念、機能はこれだけです。

ステップ2： true, false と　&& と if だけの言語

次は、少しでもプログラミング言語っぽい見た目を持つものとして true, false と && と if _ then _ else _ だけがある言語を作ってみます。たとえば

if true && false then true else false

が false になるようなものです。

この言語において扱うデータは真偽値である true, false と、それらを && や if then else で組み合わせた式です。そこで、式をつぎのように再帰的に定義します。

1. true と false は式
2. 式 e1, e2 について、e1 && e2 は式
3. 式 e1, e2, e3 について、if e1 then e2 else e3 は式

式を項として表現するため、関数 _ && _ と if _ then _ else _ を宣言します。

op 50 : _ && _
op 30 : if _ then _ else _

これで、if _ then _ else _ に true, false, true を適用してやれば、if true then false else true が項として表現できることになります。

いまやりたいことは、式の評価です。そこで「式 e を評価すると真偽値 v になる」という関係を考え、それを述語 _ => _ で表します。左辺の式を評価すると右辺の値になる、の意味です。

op 10 : _ => _

評価に関する規則を考えます。まず、true, false を評価した結果はそれ自身です。

false => false
true => true

if の評価はどうなるでしょうか。たとえば if true && true then false && false else true を評価するには、まず条件部分を評価します。すると true になるので、つぎに then 部分を評価します。結果は false になり、それが if 式の全体の値となります。

このことを、条件部分が false に評価される場合についても考えてまとめるとこうなります。

if e1 then e2 else e3 => v {
    e1 => true
    e2 => v
}
if e1 then e2 else e3 => v {
    e1 => false
    e3 => v
}

e1 && e2 を評価した結果は、e1 と e2 を評価した結果が両方とも true なら true、そうでなければ false です。

op 40 : _ is _

e1 && e2 => v {
   e1 => v1
   e2 => v2
   v1 && v2 is v
}

false && false is false
false && true is false
true && false is false
true && true is true

&& の評価に関する推論のベースケースは、&& の両辺がともに真偽値の場合です。そこで、その場合の関係を定義するために _ is _ という述語を新たに定義しています。

main {
    if true && false then true else false => v
}

実際に上のように問い合わせると v = false が返ります。以上がプログラムの全体です。

ところで、以上のことを操作的意味論の推論規則の形で表現すると次のようになるでしょう。

$$\frac{}{\text{false } \rArr \text{ false}} \;\;\;\;\;\;\;\;\;\;\;\; \frac{}{\text{true } \rArr \text{ true}}$$

$$\frac{e_1 \rArr \text{ true } \;\;\;\;\; e_2 \rArr v}{\text{if } \; e_1 \text{ then } \; e_2 \; \text{ else } \; e_3 \;\rArr\; v}$$

$$\frac{e_1 \rArr \text{ false } \;\;\;\;\; e_3 \rArr v}{\text{if } \; e_1 \text{ then } \; e_2 \; \text{ else } \; e_3 \;\rArr\; v}$$

$$\frac{e_1 \rArr v_1 \;\;\;\;\; e_2 \rArr v_2 \;\;\;\; v_1 \text{ \&\& } v_2 \;\text{ is }\; v}{e_1 \text{ \&\& } e_2 \;\rArr\; v}$$

ここで、横棒の上側が前提、下側が結論です。
それに対して ron での規則の表現は次のとおりです。

false => false;  true => true;      # 改行の代わりに ; でも区切れる

if e1 then e2 else e3 => v {
    e1 => true;  e2 => v;
}
if e1 then e2 else e3 => v {
    e1 => false;  e3 => v;
}
e1 && e2 => v {
   e1 => v1;  e2 => v2;  v1 && v2 is v;
}

前提と結論の上下が逆になっているものの、記法そのものはほぼ同じように書けています。これが ron でやりたいと思っていることです。つまり言語の操作的意味が推論規則として与えられたときに、それをだいたいそのままの形で ron によって参照実装にできたらいいなあと思っています。

使い勝手はひどい

いまのところ、冒頭のようなフィボナッチ数列を計算する関数を定義するところまでは動いています。ただし使い勝手はひどいものです。ただしく関数や規則を定義できればいいものの、少しでも間違えるとまったく意味不明なエラーが表示されたり、だまって無限ループに入り込んだりします。

ひとまず、少しでもまともに使えるようにして、いろいろな言語機能の実装をためしてみたいと思います。

脚注

1. ここでは関数という語を使っていますが、Prolog では functor という語を使います。関数的なもの、くらいの意味のようで圏論の関手とは関係ないそうです。