∃φ∀x[¬(x∈φ)]

ふと思ったことメモ書き。

（純粋な）関数型言語を使うってのは、

1 + 2 = 3

を

{φ} ∪ {φ, {φ} } ≡ {φ, {φ}, {φ, {φ} } }

と書くようなものよなぁ。（公理的集合論での自然数の定義。自然数は再帰で作る。）

確かに抽象的なんだけど、基礎に分解しすぎて人間の直感からは遠ざかってるというか。

この書き方ができること自体にはかなり大きな価値があるんだけど、これでしか書けないのは論外。

普通はこの基礎的な公理の上に、直観に近い概念を載せてから使う。

「関数型言語は並列化しやすい」って話も「マシン言語で書けば高速」ってのと同レベルな臭いを感じる。マシン語はコンピューターのアーキテクチャに束縛されるって意味で低レベルだけど、関数型言語は数学的に基礎に降りすぎって意味で低レベル。