言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella

フォーマルなタートル幾何学

昔小学校で LOGO を触ったという方も結構いらっしゃるかと思います。初めて見た時は衝撃を受けたタートル幾何学。そのうちに丸や三角やフラクタルくらいしか描ける物が無くてすぐに飽きちゃったというのが正直なところでは無いでしょうか。このタートル幾何学をもう少し真面目に考えてみようと思うのです。

幾何学の本家と言えばユークリッド幾何学です。わずか五つずつの公理と公準を基点に、あらゆる図形の証明をしてしまおうという恐ろしい物です。元々測量の為だそうで、大変真面目なのです。それと比較してタートル幾何学、可愛い亀さんに絵を描かせるという、なんと牧歌的な遊びでしょうか。だけどそれだけに留めるのは勿体無い。形式化と組み合わせることによって、もっとユニークな物になるに違いありません。

ユークリッド幾何学では定規とコンパスを手に直感を働かせながら図形の証明をしますが、コンピュータにコンパスは使えないので、出来るのは記号の置き換えだけです。この記号処理と、タートルの概念だけを使ってユークリッド幾何学を置き換えようというのがこの企みです。フォーマルなタートル幾何学を使えば、例えばこんな事が出来る(予定)です。直径の決まった円を、進むと回るだけの手続き的な方法で描くことが出来ます。図形の証明をプログラムをによって行う事が出来ます。

用語と記法

まず用語の定義から、タートルとは、位置と向きを持った点です。二つのタートルの位置と向きが同じとき、そのタートルを「同じ」と言います。これが「同じ」の定義です。タートル幾何学における証明とは、二つのタートルが「同じ」事を示す事です。タートルは「進む」と「回る」の二つの事が出来ます。進んだり回ったりしたタートル t1 を、「別のタートル t2 になった」事にします。このことを次のように書きます。

  • t1.f(100) // タートル1 が100歩進む (forward)
  • t1.r(60) // タートル1 が60度回転する (rotate)
  • t2 = t1.f(100).r(60) // タートル2 は タートル1 が100歩進んで30度まがった奴と「同じ」。

以下の「定理」を定めます。

  • t = t.f(0) // ゼロ歩進むのは進まないのと同じ
  • t = t.r(0) = t.r(360) // タートルは一回転すると同じになる。
  • t.f(a).f(b) = t.f(a + b) // タートルはまとめて進んでも分けて進んでも同じ。
  • t.r(a).r(b) = t.r(a + b) // タートルはまとめて回っても一度に回っても同じ。
  • t.f(a) = t.r(180).f(-a).r(180) // 真っ直ぐ進むのは逆向いてバックと同じ。

もっとマニアックに考えていくと、進むや回ると言った「操作」もタートル自身と同一視する事が出来ます。どのタートル t も、ある原点タートル I (Identity) からの操作

  • t = I.r(a).f(b).r(c) = r(a).f(b).r(c) // 回って、進んで、もう一度回る

と表現する事が出来るからです。座標と方向を表現するためには三つの次元が必要な事に着目してください。これを使うと上の定理はもっとシンプルに書けますし、「同じ操作」を定義する事が出来ます。

  • I = f(0) = r(0) = r(360) // 立ち止まって動かない。
  • f(a).f(b) = f(a + b) // まとめて進んだり分けて進んだり。
  • r(a).r(b) = r(a + b) // まとめて回ったり分けて回ったり。
  • f(a) = r(180).f(-a).r(180) // バック歩きの定理

注: f, r, I は定義された記号です。あとは変数です。

便利な公式

計算(記号の置き換え)をするのに便利な公式を書いておきます。

  • t1.f(a) = t2.r(b) のとき、 t1 = t1.f(a).f(-a) = t2.r(b).f(-a)
  • t1.r(a) = t2.f(b) のとき、 t1 = t1.r(a).r(-a) = t2.f(b).r(-a)
  • f(-a) = r(180).f(a).r(180)

図形の性質をタートル式で表す。

一辺 100 の正六角形の対角線の長さを求めてみましょう。

ここから幾何学を構築するためには、まだ基本定理(仮定)が足りないわけですが、一日考えても十分シンプルで強力な定理を見つける事が出来なかったので後の宿題とします。ここでは手を抜いて、とりあえず正三角形が描けるという事は証明されているとします。

I = f(a).r(120).f(a).r(120).f(a).r(120) // a 歩進んで120度曲がるを三度やると元に戻る。

使いやすいように正三角形の定理を変形します。

I = f(a).r(120).f(a).r(120).f(a).r(120)
f(a) = r(-120).f(-a).r(-120).f(-a).(-120)
     = r(-120).r(180).f(a).r(180).r(-120).r(180).f(a).r(180).(-120)
     = r(60).f(a).r(-120).f(a).r(60) -- 式1

I = f(a).r(120).f(a).r(120).f(a).r(120)
f(a).r(120).f(a) = r(-120).f(-a).r(-120)
                 = r(-120).r(180).f(a).r(180).r(-120)
                 = r(60).f(a).r(60) -- 式2

タートル t1 の一辺 100 の正六角形は以下のように表現できます。

t1.f(100).r(60).f(100).r(60).f(100).r(60).f(100).r(60).f(100).r(60).f(100).r(60)

対角線にいるタートル t2 は、半分まで進んだ所なのでこんな感じ。

t2 = t1.f(100).r(60).f(100).r(60).f(100).r(60)

これを変形して f() を全部まとめれば距離が出るでしょう。

t2 = t1.f(100).r(60).r(60).f(100).r(-120).f(100).r(60).r(60).f(100).r(60) // 式1 より
   = t1.f(100).r(120).f(100).r(-120).f(100).r(120).f(100).r(60)
   = t1.r(60).f(100).r(60)  .r(-120).r(60).f(100).r(60)  .r(60) // 式2 より
   = t1.r(60).f(100).                      f(100).r(120)
   = t1.r(60).f(200).r(120)

というわけで、対角線の長さは 200 であることが分かりました。簡単でしょ?え?余計ややこしい?これは手でやるよりも、コンピュータにやらせる事を想定してるので我慢してください。紙にタートルを書いて図形的な意味を理解しながらやると全然難しくありませんよ。

課題

ユークリッド幾何学の公理公準に相当する公理を設定する事が大きな課題として残ります。また、円を扱うためには極限を導入する必要があります。極限を導入したタートル幾何学により、円周率の計算等をより直感的な説明で行う事が出来るでしょう。あと先行研究を全然調べてないので、同じような試みがあれば知りたいです。