NGK2016Bで発表してきました

こんにちは、再びいっしーです。

12/17(土)に NGK2016Bというイベントで発表してきました。
Misocaの日常についてお話ししたので、内容を共有させていただきます。*1

資料

原稿

表紙

f:id:issi_0x0:20161220163130j:plain こんにちは、株式会社Misocaのissiです。
今日はMisocaの日常についてお話しします。

自己紹介

f:id:issi_0x0:20161220163402j:plain 私は11月からMisocaにJoinしました。
親会社である弥生の人間でもありますが、技術や文化の交流のために来ました。

大学時代にOCamlと型の話を嗜んでいたことが出向に選ばれた理由、かどうかは定かではありません。

宣伝

f:id:issi_0x0:20161220163445j:plain スポンサーセッションということで、宣伝です。

請求書作成サービス『Misoca』、みなさん、ぜひ登録してくださいね。

Misocaの開発

f:id:issi_0x0:20161220163707j:plain そんなMisocaがどうやって開発されているか、これもみなさんご存知だと思います。なので、次に行きます。

Misocaといえば

f:id:issi_0x0:20161220163717j:plain さて、Misocaといえばmzpさんや黒曜さんが有名です。

そんな2人と日常的に話すことといえば・・・

f:id:issi_0x0:20161220163827j:plain そう、型です。

問題点

f:id:issi_0x0:20161220163936j:plain ただ、ここは型の聖地名古屋なので、ただの型の話は飽きていらっしゃると思います。

解決策

f:id:issi_0x0:20161220164019j:plain なので、今日はすこし趣向を変えて、日本語と絡めてお話ししたいと思います。

本LTの結論

f:id:issi_0x0:20161220164115j:plain 結論からいうと、日本語などの自然言語の文というのはプログラムです。
・・・はて?と思った方いますよね。説明します。たとえば。

例文1:Misocaが請求書を作る。

f:id:issi_0x0:20161220164244j:plain 「Misocaが請求書を作る」という文があります。

特におかしいところのない文です。このように、ある文が文として形式的に成り立っていることは、プログラムで言うところのコンパイルが通る状態です。
では、「形式的に」とはどういうことか。

例文2:作るMisocaが請求書を。

f:id:issi_0x0:20161220164306j:plain 次の文です。「作るMisocaが請求書を。」
わからなくもないけど順番おかしくね?みたいなのが、形式的に成り立たない、ということです。これはコンパイルが通らないプログラムです。
・・・では、次はどうでしょう。

例文3:Misocaが請求書を食べる。

f:id:issi_0x0:20161220164322j:plain 「Misocaが請求書を食べる。」

形式的にはよさそうですが、比喩でもない限り意味不明です。これは、コンパイルは通るが期待と結果が違うプログラムといえます。

形式的に証明してみましょう

f:id:issi_0x0:20161220164353j:plain さて、ここまでは直観で話してきましたが、せっかくなので形式的に証明してみましょう。

準備1:規則を与える

f:id:issi_0x0:20161220164447j:plain まず、規則を与えます。
左の規則は、A/Bの右側にBがきたときAが導出されることを表しています。

逆に、右は、A\Bの左側にBがきたときAが導出される、という規則です。

準備2:単語に型をつける

f:id:issi_0x0:20161220164454j:plain 次に、単語に型をつけます。

ここではざっくり、名詞句にはNP、他動詞には(S\NP)\NPという型をつけます。
Sは文であることを表す型です。

例文1の形式的証明

f:id:issi_0x0:20161220164556j:plain 先ほどの、文として成り立っている例文です。 「請求書を」と「作る」に規則を適用して、S/NPが導かれ、さらに「Misocaが」に規則を適用するとSが導かれ、文であることが証明できました。

例文2の形式的証明

f:id:issi_0x0:20161220164650j:plain 文として成り立っていなかった例文は、規則が使えず、Sを導くことができないので文でないことが証明できます。

例文3の形式的証明

f:id:issi_0x0:20161220164659j:plain 意味不明な例文は、文であることは証明できました。
が、意味が正しいことを証明するには、もっと他の規則が必要になります。

他の文が気になる方へ

f:id:issi_0x0:20161220164749j:plain 意味の証明論やほかの文がどうなるかが気になる方はこの本をどうぞ。

まとめ

f:id:issi_0x0:20161220164820j:plain まとめです。自然言語の文はプログラムで、型と規則があれば文かどうかが証明できます。
めっちゃシンプルですよね!
そう、シンプルなんです。Misocaではシンプルを大切にしています。


採用

f:id:issi_0x0:20161220164830j:plain 同じようにシンプルを大切にしている方、世の中をシンプルにしたい方、型に興味がある方、Misocaではエンジニアを募集しています。ぜひ一度あって開発や好きなことについてお話ししましょう。 お互いに刺激を与えながら、学習し、いっしょに成長していけたら嬉しいです。

*1:なんと今回が初LTでした。めっちゃ緊張した