Egison 作者のブログ

Egison 2020年の抱負

2019年12月25日

この記事は,2019年Egisonアドベントカレンダーの25日目の記事です.

2019年を振り返り,2020年の抱負をまとめます.

2019年にできたこと

2019年はEgison開発に協力してくれる方々に助けられて,とても充実した一年になりました. 2019年にあった進捗のうち,大きなものをまとめてみます.

パターンマッチ指向プログラミングを提唱する論文を書けた

新しいプログラミング・パラダイム「パターンマッチ指向」を提唱する論文です. Egisonのパターンマッチを活かしたプログラミング・テクニックをまとめています.

この論文を書き始めたのは2018年の11月で,2019年を通して一番がんばったのはこの論文の執筆でした. 無事 <programming> 2020 に採択されて,現在 camera ready (最終提出原稿) 用意しているところです.

これから,3-10年の間にこの論文の内容を,世界中のプログラミング研究者の間で常識にするのが目標です. そのために,よい研究をして,もっとよい論文を書き続けていきたいと思います.

Read this article...


Haskell ライブラリ MiniEgison の紹介

2019年12月11日

今年の11月に miniEgison というプログラミング言語 Egison のパターンマッチを提供する Haskell ライブラリを Hackage からリリースしました. このライブラリのソースコードはGitHubでも公開されています. この記事では,このライブラリの使い方を紹介します.

Read this article...


Egisonのパターンマッチ式

2019年12月3日

この記事は,2019年Egisonアドベントカレンダーの3日目の記事です.

パターンマッチを記述するためのいくつかの構文をEgisonは提供しています. そのうちもっとも基本的な構文はmatchAll式です.

matchAll式は,ターゲット(上記の場合, [1,2,3] ),マッチャー(上記の場合, list something ),マッチ節(上記の場合, $x :: $xs -> (x,xs) )から構成されます. マッチ節は,パターン(上記の場合, $x :: $xs )とボディ(上記の場合, (x,xs) )からなります. matchAll式は,既存のプログラミング言語のマッチ式と同様に,ターゲットとパターンのパターンマッチを試みて,もしマッチしたらそのマッチ節のボディを評価します.

Read this article...


プログラミング言語Egisonとは

2019年12月1日

まえおき

2019年Egisonアドベントカレンダーの空き日をEgisonの作者の江木が使って,Egisonの解説記事を書いていこうと思っています. これらの記事をまとめて近いうちにEgison入門書を作りたいと考えています. 1日目である本日は,Egisonの概略を紹介します.

Egisonとは?

Egisonはより直感的にアルゴリズムを表現できるプログラミング言語がほしいという動機で作られたプログラミング言語です. Egisonには,直感的なアルゴリズムの表現を達成するための2つの独自の機能が実装されています. 1つ目の機能は,ユーザーにより拡張可能でかつ,非線形パターン(パターン変数に束縛した値を同じパターン内で参照するパターン)をバックトラッキングにより効率的に処理するパターンマッチ機能です. 2つ目の機能は,微分幾何の計算を表現するのに便利なテンソルの添字記法をプログラム中で使うための機能です.

これらのEgisonの独自の機能は,筆者がいろいろなアルゴリズムのプログラムを書いているうちに,既存のプログラミング言語では思い通りに書けないと事柄をみつけたときに,その解決案を見つけるためにときに年単位で試行錯誤することによって実装されました. 本日は,Egison独自の1つ目の機能である拡張可能な非線形パターンマッチについてその動機を中心に紹介します.

Read this article...


Egisonで極座標のラプラシアンを3通りの方法で計算

2018年12月25日

これは,数理物理 Advent Calendar 2018の25日目の記事です.

この記事では,極座標のラプラシアンを計算するEgisonプログラムを3通り紹介します.

Egisonは

  • テンソルの添字記法
  • 未定義関数の引数を省略する記法( `f(x,y,z)` を `f` と表記する記法)
をプログラムの記述においてもサポートしています. そのおかげで,ラプラシアンの計算を含む微分幾何の計算を簡潔に記述できます.

単純に展開していく方法による計算

下記の公式が正しいことを、右辺の`u_(r r)`と`u_r`、`u_(theta theta)`を展開することにより確かめています。

`u_(x x) + u_(y y) = u_(r r) + (1 / r) u_r + (1 / r^2) u_(theta theta)`

リーマン幾何学の公式を使う計算法

リーマン幾何学の共変微分の概念を使うと、一般の座標のラプラシアンは以下のように定義できます。

この公式は以下のように展開できます。

`Delta = (1 / sqrt(g)) del_i sqrt(g) g^(i j) del_j`

下記のプログラムでは、この公式を用いてラプラシアンを計算しています。

微分形式の幾何学の公式を使う計算法

微分形式は,座標系によらない微分方程式の表現を実現することに役に立つ. ベクトル解析で登場するgrad・rot・divの一般化であるウェッジ積(∧)・外微分(d)・内部積(ι)・ホッジ作用素(*)という限られたオペレーターを組み合わせて,任意の座標系で成り立つ微分方程式を記述できる. Egisonはこれらの微分形式のためのオペレーターの定義も簡潔に記述できる. そのおかげで微分形式によるラプラシアンの記述も簡潔に記述できる. 微分形式を使うとラプラシアンは以下のように表現される.

`Delta = d delta + delta d`

Egisonでゲージ理論 - 量子と古典の物理と幾何@九大

2017年12月1日

2017年11月19日に九州大学で開催された研究会「量子と古典の物理と幾何@九大」にて,Egisonについて講演させていただきました. 最新のEgisonは,独自のアイデアにより,テンソルの添字記法や微分形式による微分方程式の表現など微分幾何学で使われている数学の表現をサポートしています. この機能により,ゲージ理論の教科書にのっているような計算を,数式に近い簡潔な記述で表現できます. 本講演では,これらのアイデアとその応用として具体的なプログラムの例を紹介しました.

#1

おはようございます.ご紹介にあずかりました江木です.
本日は,テンソルの添字記法や微分形式による微分方程式の表現など微分幾何学で使われている数学の表現を,プログラム上で表現するために私が開発した手法についてお話します.

Read this article...


Egisonでリーマン幾何学

2016年12月24日

これは,言語実装 Advent Calendar 2016の24日目の記事です.

この記事では,リーマン幾何学の簡単な説明と,リーマン幾何学の計算を簡潔に記述するための,Egisonで新しくプログラミングに導入された記法について簡単に説明します.

リーマン幾何学とは

非ユークリッド幾何学という言葉を聞いたことはあるでしょうか? 曲面の幾何学と呼ばれていて,例えば,球面上で三角形の内角の和は180度以上になったり,平行線の公理が成り立たなくなるという話があります.

球面などの2次元の曲面が曲がっていることは,3次元の空間を認識している我々からしたら当たり前のように思えます. しかしここで過去の数学者達は,より高次元の空間を認識できる存在から見ると,今我々が認識している3次元空間も,実は曲がっているのではないかという発想しました. その発想を推し進めて発展したのがリーマン幾何学です.

リーマン幾何学が発展する過程で,実際に我々の住む宇宙が曲がっているのかどうか検証しようとする試みがあったようです. 例えば,我々が住むこの空間で巨大な三角形を書いたときの内角の和を計測してみて,180度より大きいのか小さいのかを確かめることにより,我々が住むこの空間が曲がっているのかどうか確かめようする試みが,ガウスによりなされたようです.

結論としては,時間軸までを含めた4次元時空が,ある規則に則って曲がっていることと仮定すると,天体の動きや見え方が合理的に説明できることが発見されました. それを説明する理論が有名な相対性理論です. 相対性理論によると,星の重力の原因は,星の持つエネルギーによる時空の歪みとして説明されます.

リーマン幾何学に現れる計算は,ベクトル・行列の上位概念であるテンソルについての計算と偏微分を組み合わせると記述できます.

2016年,Egisonでこれらの計算を簡潔に記述できるようにすることを一つの目標として,Egisonにシンボリックな数式を扱うことができる数式処理機能を実装しました.

特にテンソル解析については,既存の数式処理システムでは扱えていなかった記法までより上手に表現できるようになりました. それにより相対性理論の計算も,既存のシステムに較べてEgisonでは簡単に記述できるようになっています. 本記事では,この記法について簡単に解説できたらと考えています.

Egisonでプログラミングに導入されたテンソル解析の記法

以下の数式は,リーマン曲率テンソルという空間の曲がり具合を表すテンソルについての公式です. 例えば,これを表現するのに,Egisonでは既存の数式処理システムよりも簡潔に記述できます.

`R_(j k l)^i = (del Gamma_(j k)^i)/(del x^l) - (del Gamma_(j l)^i)/(del x^k) + Gamma_(j_k)^m Gamma_(m_l)^i - Gamma_(j_l)^m Gamma_(m_k)^i`

以下では,最も広く使われている数式処理システムであるWolfram言語(Mathematica)と比較しています.

Wolfram
Egison

Wolfram言語とEgisonによる記述の間の本質的な差異は,上記の式を計算する際に,Wolfram言語はTable式を用いるのに対し,Egisonは添字記法を用いることにより,数式を直接記述できているところにあります.

特に,上記のようなテンソル同士の掛け算を含む計算について,Wolfram言語による記述では,Table式とSum式による二重ループがプログラム中に現れてしまいます. しかし,アインシュタインの縮約記法もサポートするEgisonによる記述では,数式と同様にフラットにこの式を記述できます.

以上のように,プログラムの行数については大きな違いはないですが,数式をより直接的に表現している点においては,Wolfram言語よりもEgisonによる記述のほうに分があります.

上記の記法をプログラミングに導入するための機構については,現在論文を執筆中です. 1月初旬には,書き上がる予定です. もし興味を持ってくださった場合,私宛にコンタクト取って頂けましたら,論文のコピーをお送りしますので,メール頂けましたらありがたいです.

簡単に説明しますと,スカラー仮引数,テンソル仮引数という2種類の仮引数の概念をプログラミング言語に導入することによりこれを行いました.

テンソル仮引数は,引数として与えられたテンソルを,テンソルとしてそのまま扱います. 関数の仮引数がテンソル仮引数の場合,仮引数の先頭には,%が付加されます.

スカラー仮引数は,引数として与えられたテンソルが与えられた場合,テンソルのそれぞれの要素に関数の作用を自動でマップします. 関数の仮引数がテンソル仮引数の場合,仮引数の先頭には,$が付加されます.

スカラー仮引数・テンソル仮引数という2種類の仮引数を導入すると,テンソルの添字記法を自然にプログラミングに導入することができます.

テンソル仮引数が使われるのは,テンソルに関係する関数だけです. しかし,この2種類の仮引数を持たない言語では,全ての引数がテンソル仮引数であることが多いです. スカラー仮引数の概念を持たない言語で,テンソルにも対応したプログラムを書く場合,テンソルと関係ない関数を記述する際にも,テンソルのことを常に意識したプログラミングをする必要が生じます.

Egisonでは,∇は以下のように定義できます.(∂/∂の定義はここを参照してください.)

リーマン曲率テンソル

2016年4月からEgison数学ノートというサイトを立ち上げました.

このサイトでは,Egisonでプログラムを書いて検証した数学の計算を記事にしてまとめていっています. 幾何学以外の分野でも,プログラムを書いているのでぜひ覗いてみてください.

リーマン幾何学では,リーマン曲率テンソルという重要な概念が登場するのですが,これの値を色々な図形について求めるプログラムを書いています.

上記のシュワルツシルト計量のページでは,宇宙の中心に一つだけ星があり,他の場所は全て真空であるような宇宙の形について計算するためのプログラムを掲載しています. このページのプログラムとその計算結果を見ながら,相対性理論の教科書を読むと,教科書を理解するのが非常に簡単になります. 例えば,地球上のものが下に落ちようとする理由が,場所によって時間が流れる速さに違うことから説明できることが幾何学的に理解できるようになります.

その一つ下のフリードマン・ルメートル・ロバートソン・ウォーカー計量のページでは,宇宙の至る場所で一様に質量が存在するような宇宙の形について計算するためのプログラムを掲載しています. このプログラムで計算されている内容を初めて計算する人が人手で行うと半日以上はかかると思われるのですが,プログラムで計算すると1,2分で計算することができます. この計算結果を分析すると,膨張する宇宙のモデルを得ることができるようです.

また,以下のリポジトリでは,Wolfram言語とEgisonとの両方でトーラス`T^2`のリーマン曲率テンソルを計算したプログラムを置いています. ぜひこちらでも,Wolfram言語によるプログラムとEgisonによるプログラムを比べてみてください.

最後に

私が所属している楽天技術研究所では,Egison開発や,Haskellでのソフトウェア開発に興味ある方も募集しています. もし興味ある方がいらっしゃいましたら,私宛にコンタクト取って頂けますと幸いです.


プログラミング言語研究の動機

2016年11月7日(2017年7月24日修正)

既存の言語では,我々の頭の中のイメージをそのまま表現できないことがある. このような不都合は,我々が頭の中でおこなっている抽象化を,言語では表現できないときに生じる. このような抽象化を表現可能にする新しい構文を発見して,言語に組み込むことができれば,この問題は解決される. 実際,プログラミング言語について,このような抽象化をひとつ見つけて,作りはじめたのがEgisonである.

そもそも,すべてのイメージを表現できるような言語を作ることが本当にできるのかという問題は非常に難しい. というのは,我々の頭の中のイメージは,対象に対する我々の理解が深まると同時に変化するものであるからである. その変化と同時に,我々にとって便利な表現も自然と変わっていく.

このことを実感するために,ある極端な例を考えてみる.

数の概念はすでに知っているけれども,たし算やかけ算の概念は知らないひとがいるとする. そのひとにとっては,10進法は理解不能な概念であり,10進表記もまったく理解不能な表記である. しかし,たし算やかけ算の概念とその性質をある程度知っているひとにとっては,10進表記は非常に便利で,直感的な数の表現である.

たし算・かけ算を知らないというのは極端な例に思うかもしれない. しかし,我々がまだ知らない重要な概念は科学史をふりかえってみるとまだまだあってもおかしくない. このような概念が発見され,自然に対する我々の認識が深まれば,それを表現するために新しい表記法が言語に生まれる. 逆に,このようにして生まれた新しい表記法は我々が自然をより深く理解することを助け,その結果,さらなる新しい表記法が生まれる. このように,表記法の進化と科学の発展は表裏一体の関係にある.

ゆえに,表記法について研究することには大きな意義があるだろう. 「新しい表記法を見つけるための一般的な方法はあるのだろうか?」,「よりよい表記法が満たす一般的法則はあるのだろうか?」,「表記法の表現力を測る一般的な方法はあるのだろうか?」など興味深い問題はいくつも存在する. これらの問題の答えが見えたとき,まったく新しい世界観が生まれると筆者は期待している. 新しいプログラミング言語を作ることをとおして,これらの問題の答えに近づきたいというのが,Egisonを作ったそもそもの動機である.


第10回日本OSS奨励賞受賞LT

2015年10月23日

この度、Egisonについて日本OSS奨励賞という国内で有名な賞を頂けることになりました。 その受賞LTのために作成したプレゼンテーションを公開します。

#1

こんばんは。ご紹介に与りました江木です。 本日は「プログラミング言語Egisonと表記法の進化について」というタイトルでお話します。

Read this article...


ソフトウエアジャパンアワード授賞式

2015年2月12日

先週、ソフトウエアジャパンアワード授賞式に出席しスピーチしました。 楽天技術研究所の同僚と情報処理学会の方に撮っていただいた写真を公開します。

受賞スピーチについては前の記事にスクリプトを含めて公開しております。 ぜひ読んでみてください。

今後について

今後は、プログラミングの研究者の間でEgisonの価値が広く認められていくことが重要だと考えています。 論文執筆や、学会での発表に今後は特に力を入れていくつもりです。

直近では、3月4-6日に開かれるPPL2015という国内のプログラミングの学会で「パターンマッチ指向プログラミング言語Egisonチュートリアル」というタイトルで発表する予定です。

Egisonの今後にご期待頂けますと幸いです。

受賞スピーチについてはこちらを御覧ください。


ソフトウエアジャパンアワード受賞スピーチ

2015年2月3日

この度、Egisonについてソフトウエアジャパンアワードという大きな賞を頂けることになりました。 その受賞スピーチのために作成した15分のプレゼンテーションを公開します。 スピーチはソフトウエアジャパンにて2月3日の18:20-18:35に行われます。

#1

こんばんは。ご紹介に与りました江木です。 本日は「プログラミング言語Egison-表現の新たな抽象化の発見」というタイトルでスピーチさせて頂きます。

Read this article...


Egisonによる関数型プログラミング入門

2014年1月5日

「Egisonによる関数型プログラミング入門──パターンマッチ指向プログラミング言語Egison紹介(第2回)」 というタイトルでCodeIQ MAGAZINEに寄稿させていただきました。

是非読んでみてください!


新しいプログラミング言語を作る理由

2014年10月14日

「新しいプログラミング言語を作る理由──パターンマッチ指向プログラミング言語Egison紹介(第1回)」 というタイトルでCodeIQ MAGAZINEに寄稿させていただきました。

是非読んでみてください!


人工知能

2010年10月14日

人間と機械のもっと本質的な違いは,人間にとっては思考自体も観察の対象であるというところである.

思考は人間にとって気付いたときには既に組み込まれているものであり,ひとは皆,思考とは何か具体的にはわからないまま手探りで思考を行っている. 思考のルールを完全に把握して思考している人間は今のところいない. もしそのような人間がいたとすると,そのひとにとっては全ての問題が計算問題になる. 人間は特定の対象について考えるとき,その思考自体についても知見を得る. それにより,当初考えもしなかった考えを思い付くことができる.

この思考の「イデア」のようなものを,機械に組み込むことをしなければ,人工知能は実現できない. これを行うことは非常に難しい. これを行うプログラマは思考のルールを全て把握して記述する必要がある. ニューロン単位によるシミュレーションなどでも,人工知能が実現可能かもしれない. しかし,もしそのようなシミュレーションができたとすると,そのシミュレーションプログラムを読めば,どのようにしてそのプログラムが人工知能を生み出したのか 全て把握できるはずである.(人間の思考とは違い,プログラムの全ての動作は定式的に理解可能なため.) プログラムを書いた人は当然そのコードを読んでいるので,思考のルールを全て把握するのと同じことをしているはずである.

結局何がいいたいのかというと,思考のルールを把握していく以外に,人工知能は実現するいい方法はないということであり,それはつまり逆に考えると,人工知能を実現する研究は,それを読んだ人間に思考をどのように行えばいいのか,目からウロコが落ちるような示唆を必ず与えてくれるようなものであるはずであるということである. という考えで,日々最強を目指して思考のルールを把握しようと研究している.


This website in other langauge: English, 日本語