Simplicityの式は他のプログラミング言語と異なり、combinator (コンビネータ) と呼ばれる小さな式を組み合わせたもので、何らかの入力を受け取って出力にマップする関数を表します。最も単純なSimplicityプログラムは以下の通りです：

main := iden
これは空の入力を受け取り、空の出力を生成します。もう少し実用的な例として、1ビットの入力を受け取って反転させるプログラムを見てみましょう：

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

この例では、最後のSimplicity式がmain関数となっています。上から下ではなく、下から上に読み進めると、main関数が複数の関数の組み合わせであること、main関数を構築する各関数もunit combinatorと呼ばれる部品で組み立てられていることが分かります。常に空の出力を生成するunit combinatorは、受け取った入力をそのまま出力するiden、外部から取得した値を出力するwitnessと組み合わせることで、あらゆるSimplicityの式の基礎となります。このサンプルコードでは、型のアノテーションを記述することで、どんなデータが式から式へと受け渡しされるかを明示しています。”1”はunitの型を示し、上記で「空の出力」と呼ぶものに該当します。“2”は1ビットを指し、0または1の値を取ります。このサンプルコードが完全に理解できなくても心配無用です。これはあくまでも、Simplicityのコードがどのようなものかを説明するための例です。本記事後半で、より実践的なプログラムを詳細に解説します。

仕様を書くための言語

プログラミング言語とは、極論すれば、小さな計算を組わせて大きな計算を記述するためのものです。Bitcoin Scriptは (ForthやPostScriptのように) リスト化されたデータを各計算が順番に操作するスタックマシンを使う一方、EthereumにおけるEVMは、データを入力として受け取って出力として返す関数が、関数呼び出しを介して、 (同一コントラクトだけでなく、別コントラクトに存在する) 関数を呼び出すアーキテクチャを採用しています。現在主流となっているプログラミング言語の大半は、後者のモデルです。

プログラミング言語は、実行中のトランザクション内容の読み取りなどネットワーク外部とのやり取りに、side effects (副作用) を利用します。EVMにおけるコントラクトは、キーバリュー型データストアにもアクセス可能で、明示的にデータを受け渡しせずとも複数トランザクションにまたがって状態を維持できます。

Bitcoin ScriptもEVMも、ビット反転は単一のオペコードで実行できます (ただしBitcoin版ではビット以外の多様な入力に対応する一方、EVM版では常に256ビット単位で実行されます) 。なぜSimplicityでは、単純な操作に多量のコード記述を求めるのでしょうか？

私たちがSimplicityを開発する目的は、プログラム内の関数が何を表し、どのような計算リソースを利用するかという形式仕様の記述を可能にすることです。Bitcoin ScriptやEVMのように、動作する言語を形式仕様として定めることも原理上は可能かもしれません。しかし、非常に複雑なため、実装もその検証も困難を極め、現実的ではありません。Simplicityは複数の関数を数学的に組み合わせた基本的なcombinatorの小集合です。そのため、言語のセマンティクスはTシャツに印刷可能なほどコンパクトです。

実務上、ビット反転のような利用頻度の多いコードを逐一記述するのは煩雑なため、通常は一度記述したら、後はそれを使い回します。ビット反転のコードは既に私たちが記述し、言語にプリミティブとして搭載したので、コードを書く際は、上記コードの代わりに、jet_notショートカットを記述してください。ショートカットのjetsの詳細は後述いたします。

将来的には、ほとんどの人がSimplicityで独自コードを記述する必要はなくなるでしょう。Simplicityはブロックチェーン上にプログラムを作成するための基礎となりますが、あくまでも基礎です。複雑なコードは、より高級な言語で記述し、それが正しく動作するという証明とともに、Simplicityコードへとコンパイルされるようになるでしょう。

プログラムと式の違い

入力値と出力値が単純な式をprogram (プログラム) と呼びます。入力値と出力値を1:1で結びつける関数は、数学的に1つしかないため、Simplicityでプログラムを書くメリットは一見なさそうです。ところが、Simplicityでの記述は有益なだけでなく、ブロックチェーン上で関数を柔軟に記述するには必然なのです。

なぜSimplicityでなければいけないのでしょう？ポイントは2つあります。1つはSimplicityプログラムにはholeと呼ばれる「穴」があり、この穴はコインが消費されるときにしか埋まらないことです。もう1つは、Simplicityプログラムがside effects (副作用)を通して、ブロックチェーンデータの読み取りや、早期終了など純粋な数学的関数では実現できない動作を可能にすることです。

Holeを指定する方法としては：disconnectおよびwitnessコンビネータの2つがあります。disconnectは少し細かい動作をするので、詳細は過去の解説をご参照ください。一方のwitnessコンビネータは非常にシンプルで、witnessと呼ばれる特定の型の値を返します (電子署名、ハッシュのプリイメージ、または特定の署名鍵) 。

またside effects (副作用) への対応法も2つあります。1つはトランザクションデータのイントロスペクション (別記事で解説予定)、もう1つはassertionです。Assertionはプログラムの実行を停止します。Bitcoin Scriptにおいては、VERIFYオペコードがassertionに利用され、例えば不正な署名やデータを検知するとプログラムを終了させます。EVMでは、同じ目的でSTOPオペコードが使われます。

ここまで読んでいただけたら、一見単純な入力と出力をもつプログラムが有益な計算を行う仕組みを理解できたのではないでしょうか。Witnessがプログラムへの入力、Assertionが成功・失敗という形でのプログラムの出力になります。

以下、2つのwitnessの同一性を比較検証するプログラム例を見てみましょう：

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

前例と同様、プログラムを下から上に見ていきます。まず、プログラム本体であるmain関数 (型は1->1) があります。型は入力と出力のデータ型を示します。”1”型は単一値で、特に情報を持ちません。”2”型は2つの値を取ることができるため1ビットを表し、”2^32”型なら32ビットの文字列を表します。

最終行のプログラムは、cp3とjt4という２つの式のcomposition (組み合わせ) であることがわかります。上の行の定義から、cp3自体もpr1とjt2の組み合わせであることがわかります。プログラム全体で、計5種のコンビネータが利用されています：

• comp (composition) は2つの式を受け取り、最初の式の出力を次の式に入力して評価します。
  
• pairは2つの式を受け取り、左側に1つ目の式の出力、右側に2つ目の式の出力を持つペアを出力する新たな式を返します。
  
• witnessは入力を受け付けず、出力は多態性を持つためプログラムの動作に必要な型として解釈されます。出力値はプログラム実行時に提供されます。
  
• jet_eq_32はjetと呼ばれる、より大きなSimplicity式を短縮して1つのコンビネータとして表現したものです。置き換えられた元の式はspecificationと呼ばれます。Simplicityのインタプリタがjetを評価する際は、specificationを実行、あるいは全く同じ挙動をする最適化された機械語を実行することになります。jet_eq_32は2つの32ビットの値を入力として受け取り、2つの値が同一なら1、異なれば0という1ビットの値を返します。
  
• jet_verifyもjetです。1ビットの入力を受け取り、それが0であればプログラムを強制終了します。出力値はありません。

結論

少し難しかったかもしれませんが、Simplicityのコードを読み解くことで、一見単純な機能でも明示的に記述すると複雑に見えることを実感いただけたのではないしょうか。この複雑性は、実行中の処理を忠実に反映したものです。仕様を記述するための言語であるSimplicityは、すべての処理を明示的に指定することで、数学的なモデリングや必要な性質の証明を行います。これにより、堅牢性が保証された一連の処理を、アプリ開発者が安心して再利用できるようになります。

Simplicityには本記事で解説した以外にも、複数のコンビネータとjetがあります。それらについては、今後、別の記事で紹介させていただきます。言語開発の進捗にあわせ、より現実的なコード例や、プログラムの性質を証明するとはどういうことかなど解説する予定です。

次記事では、2つの同一式を1つに統合するsharing (シェアリング) というコンセプトを取り上げ、同一式という概念そのものについて詳細に説明します。

Simplicityに関する質問やフィードバックは、GitHub上でSimplicityに関するディスカッションからお寄せください。ブログ記事の更新情報は、Twitterの@blksresearchでお知らせします。