2024.04.08
https://gyazo.com/5f8c65176930440148342f9127e13199
アロンゾ・チャーチは1932年にラムダ計算を定義した。ラムダ計算がプログラミング言語の基礎として使えることをジョン・マッカーシーが1958年末に提案し、1959年にスティーブ・ラッセルが最初のLispインタプリタをIBM 704のアセンブラで書いた。1975年にジェラルド・ジェイ・サスマンとガイ・スティールがLispの方言であるSchemeを作った。 手続き/関数を導入するときにlambdaを使うのは変に思うかもしれない。この記法はアロンゾ・チャーチにまで遡る。1930年に彼は「ハット」記号を使い始め、2乗関数を$ ŷ . y × yのように書いた。しかし植字工が面倒なのでハットを引数の左に移して大文字のラムダに変え、$ Λy . y × yのようにした。その後大文字のラムダは小文字に変わり、数学書では$ λy . y × y、Lispでは(lambda (y) (* y y))と書かれるようになった。私だったらfun か^を使っていたと思う。
Church-Turingのテーゼを超える計算模型、流石に何かしらはあるとは思うのだが自分が完全に忘れているのか調べてないのかともかく何も思い出せない 具体的に何があるのだろうか? そもそもパッと思いついただけでこれがどういう問いかけなのかはあまりちゃんと考えていない
・circuitによる計算量
・無限時間TM, CTC(よく知らない)
例えばReal Computerなんかは誤差なしに無限精度で実数の計算が可能とした模型で、通常のTMより真に強い?ようです
Leanであらゆる計算模型を実装してそれらの計算能力が実際に等価であることを証明する:どうか? メモ