この節は検証可能な参考文献や出典が全く示されていないか、不十分です。 出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方） 出典検索?: "再帰的頭字語" – ニュース · 書籍 · スカラー · CiNii · J-STAGE · NDL · dlib.jp · ジャパンサーチ · TWL (2019年8月) GNU - GNU is Not Unix[1] TikZ - TikZ ist kein Zeichenprogramm[2] Wine - Wine Is Not an Emulator[3] GNU Hurdの"Hurd"は更に凝っていて、"Hurd"は"Hird of Unix-Replacing Daemons,"の略、その"Hird"は"Hurd of Interfaces Representing Depth."の略、というように相互再帰になっ

「証明」という言葉と「計算」という言葉 「計算」という言葉の説明 「証明」という言葉の説明 ここまでのまとめ 補足:「完全」という言葉について 対角化定理と再帰定理 対角化定理 再帰定理 ラムダ計算との関係 第1不完全性定理、停止問題、その他 第1不完全性定理の証明 停止問題、真を表す述語の定義不可能性 自然数論の決定不能性 補足: 「決定可能」「決定不能」という言葉について 第2不完全性定理 第2不完全性定理の証明 第2不完全性定理の内容 補足: ヒルベルトの形式主義(ヒルベルト・プログラム) まとめ 文献 「証明」という言葉と「計算」という言葉 論理学についての話や説明をする場合、 「証明」とか「証明できる」という言葉がふたつの意味で使われる。 ひとつは数学とか日常で普通に使うのと同じ普通の意味での 「証明できる」(何かの正しさを筋道立てて示すことができる)で、 もうひとつは形式的な論

自分自身を出力するプログラムを書いてみる事にする。 あたりまえだけど、プログラム全体を文字列とかリストにして、 プログラム中に埋め込むわけにはいかない。 でも全体は無理でも、 プログラム内の一部分だけなら文字列やリストにして利用することはできる。 そこで、プログラムを、 Aパート ... プログラムの一部分を、単に文字列とかリストにしたもの。 Bパート ... プログラム全体を出力する部分。 の2つに分けて考える。 Aパートは、Bパート(または、その一部分)をリテラルとして保持して、 Bパートがそれを利用して全体を出力するという役割分担になる。 Schemeの場合 簡単のために Schemeで考える(Lispでも動く)。 プログラムの構成は、大まかには、 (<Bパート> <Aパート>) みたいになる。 とりあえず、AパートはBパートそのものをリストにしていると考える。 するとAパート

不動点オペレータY 階乗関数は、 (define fact (lambda (n) (if (= n 0) 1 (* n (fact (- n 1)))))) のように、再帰的に定義できる。 再帰的定義を行なう場合はdefineやletrecを使うけど、 代わりにletを使うと再帰的定義はできない。 defineやletrecをどうしても使いたくないなら、多少工夫がいる。 例えば、factの引数を増やすという方法がある。 (let ((fact (lambda (self n) (if (= n 0) 1 (* n (self self (- n 1))))))) (fact fact 10)) ⇒ 3628800 (中略) 不動点オペレータYを使うと次のように書ける。 (let* ((Y (lambda (g) ((lambda (s) (g (lambda (x) ((s s) x))

Schemeとか関数型言語を使う人は、ラムダ計算が好きだったりする。 実際にラムダ計算をするのは別に好きではないと思うけど。 日本にも、 ラムダ算法騎士団の 総本山 があったりする。 Schemeのlambdaでも実際のlambda計算みたいな事ができる。 ; *** car、cdr、cons *** ; car、cdr、consが、lambdaだけで書ける事は、わりと有名。 ; (car、cdr、consが書けるというのは、 ; (eq? x (car (cons x y))) ; (eq? y (cdr (cons x y))) ; が成立するという事。) ; 次のようになる。 (define _cons (lambda (x y) (lambda (z) (z x y)))) (define _car (lambda (z) (z (lambda (x y) x)))) (defin

全ての物理現象はコンピュータ内でシミュレート可能ですか？可能ならその理由を、可能でないならその理由を教えてください。

Jul 25, 2005 Lisp は大変優れた言語だと思いますが、いまいち人気がありません。なぜでしょうか？ 理由としては、 使う機会が無い。つまり、どうしても学ばなければならないというものではない。 敷居が高い。 の2点があると思います。 最初の点についてはまさにその通りだと思いますが、敷居が高いというのは誤解だと思います。 前置記法は Lisp を学ぶときに全然問題にならないと思います。中置記法より便利で、一貫性があります。 括弧の多さも問題にならないと思います。Emacs や xyzzy を使えば、括弧の対応づけ、 インデントは自動でやってくれるので、読み書きにはそれほど苦労しないと思います。 しかし、問題になるのは、 Lisp の記法があまりにもシンプルで、データとしてのリストも、 プログラムもまったく同じ記法を取る点であると思います。 この単純化しすぎた記法のため、quote

May 2001 (I wrote this article to help myself understand exactly what McCarthy discovered. You don't need to know this stuff to program in Lisp, but it should be helpful to anyone who wants to understand the essence of Lisp � both in the sense of its origins and its semantic core. The fact that it has such a core is one of Lisp's distinguishing features, and the reason why, unlike other languages,

Hofstadter『メタマジック・ゲーム』 ミンスキー「ゲーデルはLispを思いついておくべきだった。もし彼がLispを思いついていたならば彼の不完全性定理の証明はもっと簡単なものになっていただろう」 ゲーデルの証明の一番難しいところは、数学的体系に自分自身を語らせるところにある。天才のひらめきが何段階か必要になる。しかし、Lispは、少なくともゲーデルが必要としていた意味で、まさに自分自身を直接語ることができる ゲーデルはLispを発明した！ 不完全性定理のLisp, Mathematicaによる記述 和田英一「Lispへのこだわり」(PDF) Eric S. Raymond「ハッカーになろう」LISP は、それをモノにしたときのすばらしい悟り体験のために勉強しましょう。この体験は、その後の人生でよりよいプログラマーとなる手助けとなるはずです。たとえ、実際には LI

Lisp code / Mathematica notebook プログラミング言語なんてどれも同じと思っている人は下の3つをJavaやC++で書いてみてほしい 不完全性定理についてのゲーデルの証明 停止問題の解決不可能性についてのチューリングの証明 LISP式がエレガントであることを証明できないというチャイティンの証明 ライプニッツ「役に立たないパラドックスは無い」（チャイティン「知の限界」） ミンスキー「ゲーデルはLispを思いついておくべきだった。もし彼がLispを思いついていたならば彼の不完全性定理の証明はもっと簡単なものになっただろう」（ホフスタッター「メタマジック・ゲーム」） 次の2冊の本はLispといってもSchemeのようなオリジナル言語が使われている。ここではCommon LispとEmacs Lisp、Mathematicaで書き直した（The Unkn

In this file we derive the Y combinator, one of the fundamental results of recursive procedure theory. You already know that in some cases it is not necessary to give a procedure a name. For example, ((lambda (x) (+ x 1)) 6) adds 1 to 6 without naming the procedure that does it. But, what about a recursive procedure? For example, (define fact (lambda (n) (if (zero? n) 1 (* n (fact (- n 1)))))) whi

Table of contents What is a quine? What is this page? Introduction A first attempt and example Principles for writing a quine A second example: added clarity The fixed-point theorem Multi-quines: making use of introns Bootstrapping: recovering the code from the data Recapitulation Self-interpretation: using data as code Conclusion Links related to quines What is a quine? What is this page? A “quin