半環による掛け算の定義 in Maude

あらまし

自然数の掛け算をプログラミング言語で素直に再帰的に定義すると (これはOCaml✨による定義)：

let rec ( * ) x y = if y = 0 then 0 else x * (y - 1) + x

のようにどちらかの引数を減らしていく定義になりがちです。

一方、我々は自然数の掛け算についてこうした順序は意識していないことが多いです。当然ながら結合法則・交換法則や分配法則は所与のものとして考えており、上記のような累加的な定義とどちらが公理であるかを意識することは少ないと思います。

どうにかして、掛け算の定義そのものから順序を追い出すことはできないでしょうか？

そのような掛け算の定義として、例えば 離散順序半環 というものがあるそうです。ここで順序半環の「順序」とは自然数の大小関係のことですが（ややこしい）、ただの計算に使うなら、大小関係のことはとりあえず考えないこととしても良さそうですね。

そこで、半環による定義をベースにした掛け算を実装できないか、という気持ちがプログラマの自然な発想として沸き起こってきます。

しかしながら、いかにしてそれを計算すべきかということは、数理論理学の公理から直接的に得られません。そもそも等式には方向がありません。また、等式をそのまま計算手続きとみなすと、例えば交換法則は無限に適用し続けることができてしまいます。

Maude を用いて半環の公理に基づく掛け算を実装する

今回は、書換え論理に基づく言語 Maude (もーど) で、半環の公理を元に、掛け算をなるべく素直に実装することを考えます。Maude は OBJ3 といった仕様記述言語や項書換え系といった計算モデルに源流をもつ言語処理系です。

• Maudeマニュアル

今回の文脈でいえば、項書換え系で知られるAC(結合法則と交換法則)を法とした書換えによる計算機能を備えており、今回の掛け算の実装には最適に思えます。

Maudeコード

Maudeはモジュール単位で計算を定義します。モジュールには functional モジュール fmod (純粋関数的な計算を eqで定義するモジュール) とシステムモジュール mod (並行計算など、もっと自由な書換えを定義するためのモジュール) がありますが、今回は純粋関数的な計算なのでfmodを使うのが適切でしょう。

プログラミング言語との対応は以下の通り：

• sort: 型の宣言。コンストラクタと一般の関数の区別はあまりない。
• op: 演算子の型宣言。2項演算子については assoc (結合法則) comm (交換法則) id (単位元) などの指定ができる。precで優先順位を指定する。
• eq: 等式の宣言。計算の実装をこれで与える。
  • 等式ではあるが左から右への書換えとして機能する。
  • 式のどの部分から計算するかは不定。このため書換え順序によって結果が異なることがある。これを防ぐために合流性の証明が必要。
  • 以下のように左辺がオーバーラップしていても怒られることはない。

以下コードにインラインでコメントを入れて解説します。一応、掛け算は動いているようですね。

fmod NAT-SEMIRING is
  *** 構造の定義。 0, 1, + は [ctor] (コンストラクタ) としてもよさそう
  sort Nat .
  op 0 : -> Nat .
  op 1 : -> Nat .
  *** 足し算と掛け算はそれぞれ結合法則・交換法則・単位元を入れておく。
  op _+_ : Nat Nat -> Nat [assoc comm id: 0 prec 33] .
  op _*_ : Nat Nat -> Nat [assoc comm prec 31] . *** 掛け算に id: 1 を入れると無限ループする…

  *** 等式で使う変数の宣言
  var X Y Z : Nat .
  
  *** 掛け算の単位元と零元。単位元は上記で id: 1 としたかったができなかった。
  eq X * 1 = X .
  eq X * 0 = 0 .

  *** 分配法則。
  eq X * (Y + Z) = X * Y + X * Z .

  *** 計算結果を見やすくする補助的なソートの定義 (下記)
  sort NatSZ .
  op z : -> NatSZ .
  op s : NatSZ -> NatSZ [iter] .
  op fromSZ : NatSZ -> Nat .
  op toSZ : Nat -> NatSZ .
  var W : NatSZ .
  eq fromSZ (z)= 0 .
  eq fromSZ (s(W)) = 1 + fromSZ (W) .
  eq toSZ (0) = z .
  eq toSZ (1 + X) = s (toSZ (X)) .
endfm

*** 試してみる
reduce in NAT-SEMIRING : 1 + 0 .
reduce in NAT-SEMIRING : 1 + 1 .
reduce in NAT-SEMIRING : 1 * 1 .
reduce in NAT-SEMIRING : (1 + 1) * 1 .
reduce in NAT-SEMIRING : (1 + 1) * (1 + 1) .
reduce in NAT-SEMIRING : (1 + 1) * (1 + 1) * 0 .
reduce in NAT-SEMIRING : (1 + 1 + 1) * (1 + 1 + 1) * (1 + 1).
reduce in NAT-SEMIRING : toSZ (1 + 1 + 1) .
reduce in NAT-SEMIRING : toSZ((1 + 1 + 1) * (1 + 1 + 1) * (1 + 1)).
reduce in NAT-SEMIRING : fromSZ (s^3(z)) .
reduce in NAT-SEMIRING : toSZ(fromSZ(s^3(z)) * fromSZ(s^3(z)) * fromSZ(s^2(z))) .

実行結果

reduce による項の簡約の入力と結果が出ています（上の入力を正規化したものを書き換えているっぽい）。

% maude.arm64 nat-semiring.maude
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
             Maude 3.4 built: Mar 16 2024 16:45:55
             Copyright 1997-2024 SRI International
                   Thu Apr 11 09:07:50 2024
==========================================
reduce in NAT-SEMIRING : 1 .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1
==========================================
reduce in NAT-SEMIRING : 1 + 1 .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1 + 1
==========================================
reduce in NAT-SEMIRING : 1 * 1 .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1
==========================================
reduce in NAT-SEMIRING : 1 * (1 + 1) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1 + 1

ここまでは普通ですが、定義の仕方によってはスタックオーバーフローしたり無限ループに陥ってしまうこともあります。
すこし試行錯誤した結果、ちゃんと止まるようになりました。

2*2 = 4

==========================================
reduce in NAT-SEMIRING : (1 + 1) * (1 + 1) .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1 + 1 + 1 + 1

2 * 0 * 2 = 0

==========================================
reduce in NAT-SEMIRING : (1 + 1) * 0 * (1 + 1) .
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 0

3 * 2 * 3 = 18

==========================================
reduce in NAT-SEMIRING : (1 + 1 + 1) * (1 + 1) * (1 + 1 + 1) .
rewrites: 18 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1

iter属性で答えを少し見やすくする

Maude のコンストラクタに iter という属性をつけると、ネストの回数を s^3(z) のようにコンパクトな内部表現で持つようになります。これを使って答えを見やすくしてみます。
ペアノ算術の自然数の表現をそのまま用いて、s(x) = x+1, z = 0 として、相互に変換する関数 fromSZ, toSZ を定義しました。

3

==========================================
reduce in NAT-SEMIRING : toSZ(1 + 1 + 1) .
rewrites: 4 in 0ms cpu (0ms real) (2000000 rewrites/second)
result NatSZ: s^3(z)

3 * 2 * 3 = 18 (少し見やすい)

==========================================
reduce in NAT-SEMIRING : toSZ((1 + 1 + 1) * (1 + 1) * (1 + 1 + 1)) .
rewrites: 37 in 0ms cpu (0ms real) (~ rewrites/second)
result NatSZ: s^18(z)

==========================================
reduce in NAT-SEMIRING : fromSZ(s^3(z)) .
rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: 1 + 1 + 1
==========================================
reduce in NAT-SEMIRING : toSZ(fromSZ(s^3(z)) * fromSZ(s^2(z)) * fromSZ(s^3(z))) .
rewrites: 44 in 0ms cpu (0ms real) (~ rewrites/second)
result NatSZ: s^18(z)

TODO

書換え規則のプログラミングとしてみた場合には停止性と合流性の証明が必要です。MaudeにはChurch-Rosser checkerがあるようなのでおいおい使ってみようと思います。

その他

• もう10年以上前に Maudeで遊んでいた頃の記事 もあります。参考にどうぞ。
• 参考: 数理情報学 6・講義ノート (名大 木平先生)