Lean日報: ProofWidgets の #html コマンドでグラフなどを表示
はじめに
この Lean 日報ではシリーズ記事として、Lean について新たに学んだことを書いていきます。定期更新ではありません。
Lean とは何か
Lean は、プログラミング言語の一種です。しかしただの言語ではなくて、純粋関数型プログラミング言語かつ定理証明支援系でもあるという特徴を持ちます。数学の形式化や自動証明の構成、数学的問題について推論するAIの開発などに応用が期待されています。[1]
コマンドとは何か
まず前提として、Lean 4 ではプログラムを実行するのに Jupyter Notebook のような特別な環境を必要としません。#eval コマンドなど、特定のコマンドを実行することでエディタ内で即座にフィードバックが得られるようになっています。
この手の「Lean から対話的にフィードバックを得る」系のコマンドは # で始まることが多く、hash command と呼ばれたり diagnostic command と呼ばれたりします。私はよく「対話的コマンド」と呼んでいます。
hash command の代表的なものが、さきほども名前を挙げた #eval コマンドであり、これはその名の通り式をインタプリタに食べさせて評価します。
infoview とは何か
Lean には、証明を行っている間に「示すべきことは何か」「今までに得られた結果は何か」を都度表示していくために、infoview という仕組みが用意されています。次のスクショでいうと、右側の 1 goal とか Tactic state とか書かれている部分が infoview です。
#html コマンド
今回は #html コマンドについてです。Lean には ProofWidgets4 というライブラリがあり、#html はそこで定義されているコマンドです。
このコマンドはその名の通り、HTML 要素をそのまま infoview に表示することができます。たとえば、以下のように画像を表示したりできます。
単に HTML 要素を表示できるだけではなく、JSX ライクな構文が使えます。さらに React のコンポーネントのように、特定の用途に対するコンポーネントも用意されています。ここでは代表的なものとして LineChart を紹介します。
これは Recharts というライブラリのラッパになっています。（ProofWidgets4 から既存の JS ライブラリを利用できます）スクリーンショットのように、関数のグラフを描画することができます。
自分でコンポーネントを自作することもできるのですが、今回は「コンポーネント自作なしで」既存のコンポーネントに載って何ができるのかだけ紹介しました。
コードについて
ここまでコード不在で話をしてきましたが、ZENN では Lean のコードの構文ハイライトは効かないようですし、お手軽に実行することもできません。私の書いている日本語 Lean ドキュメントである Lean by Example の該当ページへのリンクを貼っておきます。
Lean by Example では、右上にある再生ボタンのようなボタンを押すことでほぼすべてのページからオンラインプレイグラウンドに飛ぶことができ、環境構築不要で Lean コードが実行できるようになっています。
終わりに
Lean は詳しく学ぶ価値のあるプログラミング言語です。数学、形式証明、自動証明、関数型プログラミングなどのどれかに興味があれば、Lean から多くの学びを得ることができると思います。興味があればぜひご自分でも調べてみてください。
-
別の記事でも説明しましたが、まだ Lean 言語の知名度が低いので毎回説明することにしています。 ↩︎
Discussion