【シプサ】7 時間の複雑さ (その3)

こつこつ。今回は7.3 クラスNPから。

• clique:小集団,派閥,仲間
  
• クラス NPの概念を理解した。
  
• 7.4にはいり、NP完全性のイメージはわかった。
  

この節はお話的な雰囲気もあり、困難もそんなになかった。またおもしろかった。
「このことは、まだわかっていない」というフレーズが徐々に増えてきて、先端に近づいている感じがした。
7.4 NP完全性のさわりだけ入った。次回は、多項式帰着可能性、から。

【シプサ】7 時間の複雑さ (その2)

シプサは、ちょっと離れると再開する敷居が高い。されど、こつこつ。

• まず、前回最後のあたりがぐだぐだになったので、そのあたりから。
  
  
• 「定理7.8 t(n)をt(n)>=nであるような関数とする。このとき、すべてのt(n)時間複数テープTuring機械に対して、それと等価なO((t^2)(n))時間単一テープTuring機械が存在する。」
  
  
  
  • まず、この定理がいっていることの理解を深める。
    
  • t:n->R+な関数tについて、TIME(t(n))という言語の集合をつくれる。TIME(t(n))に含まれる言語は、O(t(n))時間Turing機械で判定されるものに限る。これが基本情報。
    
  • ということは、t(n)時間複数テープTuring機械が判定する言語は、TIME((t^2)(n))に属している言語である、という感じなんだな。
    
  • (t^2)(n)が何をあらわしているのかわからない。(t(n))(t(n))ということか? これは説明を読んで理解することにする。
    
    
  • さて、説明の理解。これは文章ではなくて、紙に絵を書いて理解をこころみる。
    
  • ... お絵描き中 ...
    
  • 雰囲気はわかった。。。(t^n)(n)は、(t(n))(t(n))のことのようだ。先へ進む。
    
  
  
  
• 「定理7.11 t(n)をt(n)>=nであるような関数とする。このとき、すべてのt(n)時間非決定性Turing機械に対して、それと等価な2^(O(t(n)))時間決定性単一テープTuring機械が存在する。」
  
  
  
  • うーん。これもなんとなく雰囲気をつかんだ。
    
  • 先々、必要になったときに、理解を深めることにする。(今は興味がわかない)
    
  
  
  
• ここから「7.2 クラスP」。
  
  
• そうか、決定性単一テープTuring機械で多項式時間判定できる言語のクラスがクラスPなんだ。
  
• そして、クラスPである、ということと、現実の電子計算機で計算を実行できるということは経験上等価であると。少くとも第一近似または突破口としてはよし。
  
• クラスPという概念は、「妥当な」計算モデルの変更によって影響を受けない。さらばTuring機械、ということか!?
  
• クラスPの概念を理解した。
  
  
• 気になるところを確認。
  
• 「与えられた数の素因数を求める一つの方法は、すてのの可能な序数を調べてみることである。この探索空間のサイズは指数的なので、」
  
  
  
  • 素因数って何だっけ?
    
  • 素因数：整数の因数である約数のうち、素数であるもの。
    
  • 因数って何だ?
    
  • 因数：一つの数や整式が、いくつかの数や整式の積の形で表されるときの、その個々の数や整式のこと。
    
  • 探索空間のサイズは?
    
    
    
    • 10進数で入力を表現する。
      
    • n=1;数=1 -> 1
      
    • n=2;数=10 -> 10
      
    • n=3;数=100 -> 100
      
    • n=4;数=1000 -> 1000
      
    • なるほど。入力のサイズnに対して調べるべき対象の数は、10^nになっている。
      
    
    
  
  
  
• 「項目1は、Pが数学的に頑強なクラスであることを示している」
  
  
  
  • 頑強(robust)というのは、前にでてきたような、どこだっけ。
    
  • 索引を調べるが、なかった。先へ進む。。。
    
  
  
  
• その計算が多項式時間でいけるかどうかを検討する際のポイント
  
  
  
  • 問題の符号化に関連すること(表現から内部表現の構成、他の表現も使うならばそれへの変換、またはこれらの逆変換など)が多項式時間でできるかどうか。
    
  • アルゴリズムのステージ数は多項式時間か。
    
  • アルゴリズムの各ステージの実行ステップは多項式時間か。
    
  
  
  
• 気になること。数字の一進表現は指数的だが、二進表現は多項式的?
  
  
  
  • まず、一進表現。
    
  • n=1;16進数=1 -> 1
    
  • n=2;16進数=10 -> 16個
    
  • n=3;16進数=100 -> 256個
    
  • まあ、これは指数的。
    
  • 次に二進表現。
    
  • n=1;16進数=1 -> 1個
    
  • n=2;16進数=10 -> 5個 (1 0000)
    
  • n=3;16進数=100 -> 9個 (1 0000 0000)
    
  • おお、n^2程度だ。
    
  
  
  
• う、これから、例としてグラフ理論が多くなるのか。。。
  
  
• 「定理7.14 PATH∈P」
  
  
  
  • 気になるところを調べる。
    
  • 全数探索は本当に指数的か?
    
  • グラフ Gの節点数をmとする。
    
  • sからtへの経路が存在するならば、それは各節点をたかだか1回しかとおらない。なぜなら、2回とおるということはループ構造があるということであり、ループしなきゃいいんだから。
    
  • するとG内に存在する経路とは高々m個の節点の列である。
    
  • ではこのような節点の列が何個あるかというと、始点をsとしたものは、(m-1) + (m-1)(m-2) + (m-1)(m-2)(m-3) + ... + (m-1)(m-2)...(2)(1)かな?
    
  • これが指数的か多項式的か?
    
  • わからない。。。
    
  • いかん、グラフ理論または離散数学の勉強をせねば。
    
  • とりあえず今は先に進む。
    
  
  
  
• 「定理7.15 RELPRIME∈P」
  
  
  
  • これはアルゴリズムとデータ構造のときに検討したので、まあわかる。
    
  
  
  
• 「定理7.16 すべての文脈自由言語はPの要素である」
  
  
  
  • これ、ぼやぼやしている、日を置いて再度考える。
    
  
  

またまた最後ぐだぐだになったが、とりあえずクラスPがおわった。
次回はクラスNP。

【CLドリル】1 Basic Constructs

もともとは日本語の書籍だが、日本語版は古本屋でもみつからなかった。英訳版を偶然古本屋でみつけたので購入したもの。内容は、Common Lisp入門と対応している。Common Lisp入門の復習をしながら、取り組んでいくことにする。

• 1 Basic Constructs
  
  
  
  • 1-1 A Common Lisp System
    
  • 1-2 Functions
    
  • 1-3 Variables and Symbols
    
  • 1-4 Lists
    
  • 1-5 Evaluation and Forms
    
  
  

ちょっともやもや。
(setq x '((a b) (c d)))
として、例えば、
(cons (car x) nil)
がなぜ、
((a b))
となるのか?
評価をたどると、
(cons (a b) nil)
となってここで、(a b)を関数呼び出しとならないのか???
直接、
(cons (a b) nil)
を評価すれば、(a b)は関数呼び出しとなって、aは関数として未定義なので、エラーとなる。

まずansiによるとconsは関数である。そだったんだ。
そして、consの値は、"a cons"である。これは"a compound data object having two components called car and the cdr"という意味でのcons。
すなわち、(cons ...)を評価した値はそれがスペシャルフォームや関数呼出フォームの形であっても、あくまで、a consであるとして、次の関数に渡されるということか。

次にcarはaccessorである。まあsetfに使えるからね。
listを引数で受け取り、objectを値とする。objectは"any lisp datum"である。。。
う、ここらへん、実はもやもやしている。整理する。

• 記法として、evalされて返されたlist objectのみ、と表記することにする。
  
  
• (cons (car (quote ((a b) (c d)))) nil)の場合。
  まず、これをreaderが読み込んでlisp objectに解釈する。それは概念的には次のようなもの(object)になる。
  (<symbol cons> (<symbol car> (<symbol cons> (<symbol cons> <symbol a> (<symbol cons> <symbol b> <symbol nil>) (<symbol cons> <symbol c> (<symbol cons> <symbol d> <symbol nil)))) <symbol nil>)
  そして、evalにわたされる。
  evalは、まず、consがfunctionの名前なので、function formと判断する。
  function formはsubformを左から右へ先行評価するので中身の評価にはいる。
  ちょっとずるして先に二つ目をやっちゃう。二つ目はnilのsymbolなので、nilが返る。
  一つ目は、
  (<symbol car> ... )
  なので、これもfunction formで中身へ。
  (<symbol cons> ...)
  なので、consのfunction form。この中身へ。
  (<symbol cons> ...)
  なので、function form。subformをそれぞれ評価する。ひとつめは
  (<symbol cons> <symbol b> <nil>)
  function callすると、
  <list-obj {<symbol b>} >
  という感じのものがかえる。ひとつ上にもどると、
  (<symbol cons> <symbol a> <list-obj {}>)
  なので、function call。結果は、
  <list-obj {<symbol a> <symbol b>}>
  ひとつ上にもどって評価した結果は、
  <list-obj {<list-obj {<symbol a> <symbol b>}> <list-obj {<symbol c> <symbol d>}>}>
  となる。これが
  (<symbol car> ...)
  のsubformの結果なので、carの関数呼び出し。その結果、
  <list-obj {<symbol a> <symbol b>}>
  が返る。なので結局、はじめのfunction form consのsubformの評価結果は、
  <list-obj {<symbol a> <symbol b>}>
  <nil>
  の2つ。この評価結果たちにたいしてconsをfunction call。
  <list-obj { <list-obj {<symbol a> <symbol b>}> }>
  が結果として返る。これが((a b))のこと。
  
  
• (cons (a b) nil)の場合。
  まずこれをreaderが読みこむと次のようなlisp objectになる。
  (<symbol cons> (<symbol a> <symbol b>) <symbol nil>)
  これをevalが評価する。
  
  まず、頭のconsはfunction nameだからfunction formと解釈する。
  subformの評価に進む。
  (<symbol a> <symbol b>)
  を解釈しようとするが、この<symbol a>に該当する
  
  special operator
  macro name
  function name
  
  が存在しない。またこのcarがcompoud formでlambdaなら解釈のしようがあるが、そうでもない。
  よって、これは解釈不可能ということでエラーになる。
  
  
• 要約する。何がポイントかというと
  (cons (car '((a b) (c d))) nil)を評価する、とかいうとき
  
  (cons (car '((a b) (c d))) nil)
  =>(cons (a b) nil)
  =>((a b))
  
  とか書くとなんだか変である。
  
  (cons (car '((a b) (c d))) nil)
  =>(cons '(a b) nil)
  =>'((a b))
  
  の方がよさ気。
  しかし、根本的に言うと、この疑似的に評価プロセスを手書きするという手法は曖昧なものである。というのは、「readerに入力する構文表記のままで、evalしている」からだ。readerは頭の中にある、という解釈もあるが、evalした結果がreadされる前の構文表記に戻っているのがいただけない。
  
  まあわかっているものどうしの便法、野暮なことは言うなということ、なんでしょうね。
  

こつこつ。

目標の整理 (Ver.2.1.1)

状態をアップデート。

• GNU/linuxのptyアプリを書きたい。
  
  
  
  • 「詳解UNIX」を勉強する。
    
    
    
    • C言語を勉強する。
      
      
      
      • 「明解 C言語 入門編」【完了】
        
      • 「明解 C言語 実践編」【完了】
        
      • 「UNIXの道具箱」★途中
        
      
      
    • GNU/linuxのAPIの基礎を勉強する。
      
      
      
      • 「例解UNIXプログラミング教室」★途中
        
      
      
    
    
  
  
  
• NorvigのAIを読みたい。(Common Lispプログラミングの書きぶりを知りたい)
  
  
  
  • アルゴリズムとデータ構造について勉強する。
    
    
    
    • C言語の基礎を勉強する。【完了】
      
    • C言語でアルゴリズムとデータ構造をやる。
      
      
      
      • 「C言語によるアルゴリズムとデータ構造」【完了】
        
      • 「アルゴリズムC」
        
      
      
    
    
  • Common Lispについて基本を復習する。
    
    
    
    • 「初めての人のためのLISP」★途中
      
    • 「Common Lisp入門」【完了】
      
    • 「Common Lisp Drill」 ★途中
      
    
    
  
  
  
• Common Lispを理解したい。
  
  
  
  • コンパイルを理解する。
    
    
    
    • 「パタヘネ」を理解する。
      
      
      
      • 上巻【通読完了】
        
      • 下巻【通読完了】
        
      
      
    • 「シプサ」を理解する。
      
      
      
      • 「集合30講」【完了】
        
      • 「計算理論の基礎 1」【完了】
        
      • 「計算理論の基礎 2」【完了】
        
      • 「計算理論の基礎 3」★途中
        
      
      
    • コンパイラの基礎を学ぶ
      
      
      
      • 「新コンピュータサイエンス講座 コンパイラ」(シプサの後に実施)
        
      
      
    
    
  • 「Lisp In Small Peaces」を理解する。
    
  
  
  
• OSの基礎知識を得る
  
  
  
  • 「Operationg Systems Design and Implementation 3rd Ed.」
    
  
  
  
• 記述論理を理解する。
  
  
  
  • 数理論理学の基礎知識をえる。
    
    
    
    • 一階述語論理とホーア論理を理解する。
      
      
      
      • 「ソフトウエア科学のための論理学」
        
        
        
        • 「論理学をつくる」 ★途中 (シプサの後に復帰)
          
        
        
      
      
    • 圏論を理解する。
      
      
      
      • 群・環・体の基本を知る。
        
      • 代数幾何の基本を知る。
        
      • 圏論の入門書を読む。
        
      
      
    
    
  
  
  
• 考えるための基本的な訓練をする。
  
  
  
  • 微積分
    
  • 線形代数
    
  
  
  
• マネージメントを勉強する
  
  
  
  • 統計学の基本をおさえる。
    
    
    
    • 「統計学入門」 ★途中
      
    • 数学的に準備する。
      
      
      
      • 位相の基本を知る。
        
      • ルベーグ積分を知る。
        
      • 確率論を知る。
        
      
      
    
    
  
  
  
• 生活環境の改善
  
  
  
  • Emacs
    
    
    
    • 「入門GNU Emacs」【通読完了】
      
    
    
  • Shell
    
    
    
    • 「詳解シェルスクリプト」【通読完了】
      
    • 「新Linux/Unix入門」★途中
      
    • 「Linuxの教科書」
      
    
    
  
  
  
• 体で覚えるもの
  
  
  
  • 「解きながら覚えるC言語」
    
  • 「入門 GNU Emacs」
    
  • 「詳解シェルスクリプト」
    
  
  

【CL入門】付録2 Lispプログラムのデバッグ

こつこつ。

• aclでは、ブレイク・レベルにて、環境の参照を素朴には実施できない。:localをつかえば一覧表示はできる。
  
• aclでは、
  
  
  
  • バックトレースは:bt。
    
  • トップレベルにもどるのは:reset。
    
  
  
• そうか、print文を埋め込む方式を「デバッグ・ライト」と呼ぶのか。
  
• #+debug (print x)
  お、頭いいな。
  
• aclでbreakから実行再開するには:cont 0。
  

おお、湯浅先生のCommon Lisp入門を読了した。
CLtL1ではありますが、処理系実装者らしさを適度におりまぜたよい説明が随所にありました。読んでよかったです。
次のターゲットは、この本と双子であるCommon Lisp Drillです。

【CL入門】付録1 実際的なLispプログラムの例 (その2)

こつこつ。今日も写経。

• クロス・リファレンスってこういうことなんだ?
  
• とりあえず、loadは通るようになった。
  
• 将来、つくりこもう!
  

次回は付録2 Lispプログラムのデバッグ。

【シプサ】7 時間の複雑さ

気分一新、第三巻。

• asymptotic: asymptote 漸近線
  
• 漸近線: ある曲線が、原点から無限に遠ざかるにつれて、限りなく近づいてはいくが、決して交わらないし、接しもしない直線。
  
• おお。big-O記法というのは、大きい入力における近似の考え方だったんだ。
  
• うーん。logがわからない。wikipedia。。。
  
  
  
  • 任意の正の実数x について、x=a^p (a != 1) をみたす実数pが唯一存在する。このpを p = log[a] x と書く。
    
  • ここで、aを底と呼ぶ。底は、2, e(ネイピア数), 10などをとることが多い。それぞれのとき底を省略するために、Log, ln, lgなどと書くこともある。
    
  • xy = a^pのときp=log[a](xy)。x=a^q, y=a^rのときq=log[a]x,r=log[a]y。xy=(a^q)(a^r)=a^(q+r)だから、log[a](xy) = log[a]x +log[a]y。
    
  • nが自然数のとき、前項をつかって、log[a](x^n) = nlog[a]x。これはたぶん実数でもなりたって、log[a](x^p) = plog[a]x。
    
  • (log[a]x)(log[b]a) = log[b](a^(log[a]x)) = log[b]xより、log[a]x = (log[b]x)/(log[b]a)。なるほど定数倍だ。
    
  
  
• 5n^3+2n^2+22n+6 = O(n^3)。
  
  
  
  • nが十分大きければ、n^3 > 2n^2+22n+6。
    
  • よって、nが十分大きければ、6n^3 > 5n^3+2n^2+22n+6。
    
  
  
• 3nlog[2]n+5nlog[2]log[2]n+2 = O(nlogn)
  
  
  
  • loglognはlognよりもはるかに発散が遅い。ゆえにnが十分に大きければ、4nlog[2]n>3nlog[2]n+5nlog[2]log[2]n+2。
    
  
  
• O(n^2)+O(n) = O(n^2)。
  
  
  
  • nが十分に大きければ、定数倍の値に関わらず、O(n^2)+O(n^2) > O(n^2)+O(n)。
    
  
  
• f(n)=2^(O(n))の意味は?
  
  
  
  • nが十分に大きいとき、2^(Cn)がf(n)の上界になっているということ。
    
  • なんで、O(2^n)ってかかないんだろう??
    
  
  
• f(n)=2^(O(logn))の意味は?
  
  
  
  • nが十分に大きいとき、2^(Clogn)がf(n)の上界になっているということ。2^(Clogn) = 2^(log(n^C)) = Dn^Cだからn^Cが上界ということ。
    
  • なんで、O(n^C)と書かないんだろう?
    
  
  
• n^O(1)とは?
  
  
  
  • O(1)は、定数より大きくならない。よって、n^C。なので2^(O(logn))と同じ。
    
  
  
• n^5、n^3、nなどの上界を多項式境界という。
  
• 2^(n^6)、2^(n^2)、2^(n)などの上界を指数境界という。
  
  
• small-o 記法。
  
• f(n)=o(g(n)) <=> lim f/g = 0 。 なるほど。これはbig-Oよりも「ずいぶん大きい」境界だな。
  
  
• あ、big-Oとかsmall-OのOって、たぶんOrder(規模)のOなんだろうな。なっとく。
  
  
• う、言語0^k1^kの修正アルゴリズムで、走査回数がたかだか1+log[2]nになるのがわからない。考える。
  
  
  
  • n=2、01とのき。q01#Xq1#Xxq_#Xqx_#qXx_#qXx_。これは5回?
    
  • 1 + log[2]2 = 1 + 1 = 2。あり?
    
  • n=4、0011のとき。q0011#Xq011#X0q11#X0xq1_#X0x1q_#X0xq1_#X0qx1_#Xq0x1_#qX0x1_#Xq0x1_#Xxqx1_#Xxxq1_#Xxxxq_#Xxxxq_。これは13回?
    
  • 1 + log[2]4 = 1 + 2 = 3。あり?
    
    
  • なんかおかしい。1+lognになるのはここではないのかな?
    
  • まず、はしからはしまでの一回の動作のステップは、常にn。
    
  • じゃあ、何回、はしからはしまでをやりますか、というと、
    
  • n=2のとき、1回。log[2]2 = 1
    
  • n=4のとき、2回。log[2]4 = 2
    
  • n=6のとき、2回。log[2]6 = 2.58
    
  • n=8のとき、3回。log[2]8 = 3
    
  • n=10のとき、3回。log[2]10 = 3.32
    
  • n=16のとき。log[2]16 = 4
    
  • 1を足しているのがよくわからないが、対数的にはなっている。
    
  • なぜ、底を2とした対数的になっているのか?
    
  • 底を2とする対数ってなんだ?
    
  • a = log[2]b のとき、2^b = a。
    
  • そうか、今あるNがあるとき、「2の何乗がNですか」ということは、「Nに1/2を何回掛けると1になりますか」ということであり、これは「N個の作業対象があり、毎回作業対象が前回の半分になるときに、何回作業すると作業対象が0になりますか」ということと同義なんだ。
    
  • やっと、毎回半分になる作業が、log[2]n回の繰返しになるということが理解できた。
    
  
  

最後ぐだぐだになったが、とりあえず7.1がおわった。
次回は、7.2 クラスP。こつこつ。

【CL入門】付録1 実際的なLispプログラムの例

テキストエディタをつくるの巻。

• A1.1 テキスト・エディタをひたすら写経。
  
• そっか、テキストエディタのデータ構造って穴あきバッファなんだ。
  
• はたと気がついた。この本、CLtL1なんじゃないかと。
  
• 調べると、
  1984 - CLtL1
  1986 - この本の出版
  1986 - X3J13の開始
  1989 - CLtL2
  1994 - X3.226-1994
  やはりそうだ。KCLだしね。
  
• タイポを除去して、起動するようにはなったが、画面制御まわりの整備が必要(KCL->ACL)。
  
• これは興味深いが、将来の課題にとっておく。
  

うーん。500行の写経で長いと思っているようではいかん。
こつこつ。

【CL入門】12 プログラミング

こつこつ。

• (ed "foo.lsp")で、ソースがemacsのbufferにでた。ちょっとびっくり。
  
• compile、劇的だ。
  

  
  CL-USER(25): (time (fib 20))
  ; cpu time (non-gc) 110 msec user, 0 msec system
  ; cpu time (gc)     10 msec user, 0 msec system
  ; cpu time (total)  120 msec user, 0 msec system
  ; real time  125 msec
  ; space allocation:
  ;  527,965 cons cells, 54,642,624 other bytes, 0 static bytes
  10946
  CL-USER(26): (time (fib 25))
  ; cpu time (non-gc) 1,070 msec user, 10 msec system
  ; cpu time (gc)     290 msec user, 0 msec system
  ; cpu time (total)  1,360 msec user, 10 msec system
  ; real time  1,379 msec
  ; space allocation:
  ;  5,855,494 cons cells, 606,020,352 other bytes, 0 static bytes
  121393
  CL-USER(27): (time (fib 30))
  ; cpu time (non-gc) 10,990 msec user, 100 msec system
  ; cpu time (gc)     3,150 msec user, 20 msec system
  ; cpu time (total)  14,140 msec user, 120 msec system
  ; real time  14,273 msec
  ; space allocation:
  ;  64,938,696 cons cells, 6,720,894,720 other bytes, 0 static bytes
  1346269
  CL-USER(28): (compile 'fib)
  FIB
  NIL
  NIL
  CL-USER(29): (time (fib 20))
  ; cpu time (non-gc) 0 msec user, 0 msec system
  ; cpu time (gc)     0 msec user, 0 msec system
  ; cpu time (total)  0 msec user, 0 msec system
  ; real time  1 msec
  ; space allocation:
  ;  1 cons cell, 0 other bytes, 0 static bytes
  10946
  CL-USER(30): (time (fib 25))
  ; cpu time (non-gc) 10 msec user, 0 msec system
  ; cpu time (gc)     0 msec user, 0 msec system
  ; cpu time (total)  10 msec user, 0 msec system
  ; real time  2 msec
  ; space allocation:
  ;  1 cons cell, 0 other bytes, 0 static bytes
  121393
  CL-USER(31): (time (fib 30))
  ; cpu time (non-gc) 20 msec user, 0 msec system
  ; cpu time (gc)     0 msec user, 0 msec system
  ; cpu time (total)  20 msec user, 0 msec system
  ; real time  21 msec
  ; space allocation:
  ;  1 cons cell, 0 other bytes, 0 static bytes
  1346269
  CL-USER(32):
  

  
  
• この後、eval-whenやモジュール、そしてdescribe/inspect/apropos。
  

あり? さくっと終わってしまった。
付録1と2の完了をもって読了としよう。次は付録1「実際的なLispプログラムの例」。

【シプサ】6 計算可能性の理論における先進的な話題 (その7)

こつこつ。今日は演習。

• 6.1 再帰定理の考え方を利用して、自己複製プログラムをつくれということ。
  
  
  
  • 問題の解釈はいろいろあるが、とりあえず、CLということで、REPLにて評価の前後で形がかわらないS式をつくる、というお題とした。
    
  • また、TMへの入力を関数の引数とした。よってTMが各部にわかれている場合、各部の間の入力出力の組み合わせは、関数の連続適用によってなされているとした。
    
    
  • 一番簡単なのは、NILなんだが、それはおいといて。
    
  • こんな感じ。
    

    
    ((lambda (B)
       `(,B ((lambda () ',B))))
     ((lambda () '(lambda (B)
                    `(,B ((lambda () ',B)))))))
    

    
    
  • quoteをちゃんと書くと、こんな感じ。
    

    
    ((lambda (B)
       (list B (list (list (quote lambda) nil (list (quote quote) B)))))
     ((lambda () (quote (lambda (B)
                          (list B (list (list (quote lambda) nil (list (quote quote) B)))))))))
    

    
    
  • 後々、C言語でもやってみたい。今はやらない。
    
  
  
  
• 6.2 「MIN[TM]の任意の無限部分集合がTuring認識可能でないことを示せ」
  
  
  
  • えっとMIN[TM]って何だっけ。
    
    
    
    • TMの表現を集めた言語。
      
    • ただし、それはそれぞれのTMにおいて文字列長において最小のもののみ有資格。
      
    
    
  • で、これは認識不可能だったはずだがなぜか。
    
    
    
    • 再帰定理がきいてくる。
      
    • えっと、まずMIN[TM]を認識するTM Mが存在するとする。
      
    • するとMを変形してMIN[TM]の列挙装置もつくれる。これをM'とする。
      
    • 次のようなTM Sを構成する。
      
      
      
      • 入力をwとする。
        
      • まず、再帰定理で自分自身の表現<S>を得る。
        
      • 列挙装置M'を動かして、<S>より長いTM表現を得る。これを<T>と呼ぶ。
        ※証明はしていないが、TMの定義からいって、Tが常に存在することは問題なさそうだ。
        
      • <%>を入力wについてシミュレートする。
        
      
      
    • すると、TM SはTM Tと同じ動作をするTMである。
      
    • ここで、TM Sの中では、<S> < <T>が長いということになっている。
      
    • これは、列挙装置M'が出力するTMの表現が「同種のもので最小である」といことに反している。ゆえに仮定がおかしい。■
      
    
    
    
  • えっと、この証明をそのまま「MIN[TM]の任意の無限部分集合」に適用すればよいかと。■
    
  
  
  
• 6.3 「A <=T B かつ B <=T C のとき、A <=T C であることを示せ」
  
  
  
  • A <=T B の定義はなんだっけ?
    
    
    
    • たしか、Aのoracleが存在した場合に、Bが判定可能となるようなAのoracleをつかった手順が存在すること、だった。
      
    
    
  • えっと、記法をさだめる。
    
    
    
    • AのoracleをOR[A]とかく。
      
    • oracle OR[X]を使った判定手順をT[OR[X]]とかく。
      
    
    
  • すると、T[OR[A]]はBを判定し、T[OR[B]]はCを判定する、ということ。
    
  • このとき、T[OR[A]はBを判定するのだから、Bのoracleでもある。Cについてもしかり。
    
  • Cのoracle = T[OR[B]] = T[OR[T[OR[A]]]]]。
    
  • これはAのoracleが存在すれば、それを使った手順にてCのoracleが作れる、すなわちCを判定できることを示している。
    
  • この言明は、A <=T Cの定義そのもの。■
    
  
  
  
• 6.4
  
  
  
  • A[TM]ってなんだっけ?
    
  • A[TM] = {<M,w> | TM Mは入力wを受理する。}
    
  • では、A[TM]'って何だろう? 問題文からすると
    
  • A[TM]' = {<N,x> | Nはoracle TMである。A[TM]に対するoracleを内蔵したoracle TM M^(A[TM])はxを受理する}
    
  • ということ? ちょっとよくわからない。
    
  • しょうがないので、A[TM]'を自分なりに組み立てて探る。
    
    
  • まず、MというTMがある。これはTMの定義にしたがって仕様がきまる。
    
  • TM Mはいろいろな入力にたいして、受理したり拒否したりループしたりする。
    
  • 言語A[TM]というのは、そんなTMと入力の組み<M,w>について、受理するものだけの表現を集めたものということだった。
    
    
  • さて、言語A[TM]に対するoracleというのは、任意の文字列について、それがA[TM]の要素かどうかを判定してくれる超機械であった。
    
  • その超機械への問い合わせ機構をもった特殊なTMをoracle TMと呼び、oracleというのは言語に紐づいて設定される概念であるから、その名前をM^(A[TM])などと、言語とともに書くことにした。
    
  • M^(A[TM])は、A[TM]を判定するoracle TMである。よってその入力は、A[TM]の要素<M,w>である。
    
    
  • さて、A[TM]は、TMと入力の組だった。この考えをoracle TMに拡張できるか。
    
  • A[TM]'はoracle TMと入力の組。ただし、入力はまったく任意ではなくて、M^(A[TM])が受理するものに限るとする。
    
  • この組の数は膨大になるかもしれない。なぜなら、oracle TM が入力を受理する、などの制限をかけていないので、すべてのoracle TMの表現がこの言語に含まれるからだ。
    
    
  • さて、これがA[TM]'の理解として正しいのかどうか微妙だが、正しいとして解答をこころみる。
    
  • まず、A[TM]'がA[TM]に対して相対的に判定可能だと仮定する。
    
  • ということは、M^(A[TM])を使ってA[TM]'を判定する手順が存在する、ということ。
    
  • 。。。いきづまった?
    
    
  • 問題の解釈に間違いがあるか?
    
  • 「さて、A[TM]は、TMと入力の組だった。この考えをoracle TMに拡張できるか。」というところを、oracle TM M^(A[TM])としてみる。
    
  • するとA[TM]'はあくまで受理される組についての言語になり、すこしまっとうになった気がする。
    
    
  • さて、これがA[TM]'の理解として正しいのかどうかひきつづき微妙だが、正しいとして解答をこころみる。
    
  • まず、A[TM]'がA[TM]に対して相対的に判定可能だと仮定する。
    
  • ということは、M^(A[TM])を使ってA[TM]'を判定する手順が存在する、ということ。
    
  • あ、これは簡単に判定できる。wをM^(A[TM])にくわせるだけじゃん。
    
    
  • うむー。問題文を理解できないとつらい。これは未来の自分への課題として、先へ進む。
    
    
  
  
  
• 6.5
  
  
  
  • ∃x∀y [ x+y=y ]はTh(N,+)の要素である。
    
  • なぜかというと、x=0∈Nとするとき、関係0+y=yはyの値に関わらずtrueとなる。よって、この言明はtrueであり、Th(N,+)の要素となる。
    
    
  • ∃x∀y [ x+y=x ]はTh(N,+)の要素ではない。
    
  • なぜなら、例えば、y=1∈Nにたいしてxは存在しない。よってこの言明はfalseである。falseな言明は、Th(N,+)の要素ではない。
    
  
  
  
• 6.3と6.5の解答を確認。芯は外していないな。
  

6.4の問題文を理解できなかったのがくやしいが、一応シプサの第二巻を読了した！！

次回から第三巻 複雑さの理論。

まずは第7章 時間の複雑さ。ここはbig-Oだとかsmall-oだとか、NP完全だとか、これまたいろんなところでよくみるけれど、全然知らなくて、いつも理解を妨げていた概念たちだ。楽しみ。

【シプサ】6 計算可能性の理論における先進的な話題 (その6)

こつこつ。「6.4 情報の定義」
今日は邦書メイン。

• informationの定義はいくつかある。ここではcomputability theoryを使った定義を確認する。
  
  
• 言葉の定義
  
  
  
  • x: 二進文字列
    
  • d(x): xの最小記述
    
  • <M,w>:テープ上にxを設定して停止するTM Mとその入力wの記述。二進文字列。
    
  • K(x): <M,w>のうち最も長さが短いもの。(同じ長さの場合は辞書式で若い方)記述の複雑さ、またはKolmogorov複雑さと呼ぶ。K(x)=d(x)である。
    
  
  
  
• 定理を丁寧に理解する。
  
  
• 定理6.24
  ∃c∀x[K(x) <= |x| + c]
  
  
  
  • この定理は、アルゴリズムによる情報の記述を採用すると、場合によって、表現したい情報そのものよりも長くなってしまうのであるが、それは入力の文字列のあり様にかかわらず、せいぜい定数であるということ。
    
  • これは起動したら何もせず定義するTMをNとすると、
    d(x)の候補: <M,w> = <N,x> = <N>x
    K(x) = |d(x)| <= |<N>x| = |x| + |<N>|
    最後の項はxによらず定数。定理を確認できた。
    
  
  
  
• 定理6.25
  ∃c∀x [K(xx) <= K(x) + c]
  
  
  
  • この定理が意味するところは、入力文字列を二度繰り返すことによってどれくらい情報量が増えるかというとたいして増えなくて、単一の入力だったときとくらべると、入力文字列のあり様に関わらず、せいぜい定数だということ。
    
  • TM Dは、<N, w>を入力として受け取り、Nを入力wでシミュレートした後で、その出力文字列を二回出力するとする。
    
  • これのwをxに変えたものとしてd(x)を選ぶ。
    
  • d(x)を入力とするDはxxを出力するので、K(xx)候補ではある。
    d(xx) の候補: <:D,w> = <D>d(x)
    K(xx) <= |<D>d(x)| = |<D>| + |K(x)|
    
  • これで定理を確認できた。
    
  
  
  
• 定理6.26
  ∃c∀x,y [K(xy) <= 2K(x) + K(y) + c]
  
  
  
  • この定理が意味するところ。K(xy) <= K(x) + K(y) + c と予測されるが、そうではなくて連結はもう少し情報を含んでいる、またはコストがかかる、ということ。
    
  • 入力は0or1から成る。
    
  • xyを出力するTMを考えるときに情報として、xとyの区切りを認識する必要がある。
    
  • この2つのことを鑑みて、xの文字を全て2個ずつにして(010なら001100)、yとの区切りを01とする手法をとるとする。x,yからこの手法で構成した文字列をwと呼ぶ。xを2倍にしたものをx'と呼ぶ。
    
  • 今作成中のTMをMと呼ぼう。
    
  • Mは3つの部分からなるとする。
    
    
    
    • M1. 全体を統合管理するとともに、x'とyに分離して他の部分に渡す処理。
      
    • M2. x'を受け取りxを出力する部分
      
    • M3. yを受け取りyを出力する部分
      
    
    
  • 。。。いきづまった。
    
  • あれ、この定理、シプサ先生が書いているほど、自明じゃないんじゃないか???
    
  • 深掘りはやめて、先に進むことにする。
    
  
  
• xyのencodingとして、xの長さ(整数)を冒頭につけて、それを00,11方式で書くとすると、
  2log(K(x)) + K(x) + K(y) + c
  までは追い込める、とな。
  
  
  
• 定義の最適性
  
  
• 言葉の定義。
  
• 計算可能な関数 p: Σ* -> Σ* を、一般的な記述言語と呼ぶ。
  
• 情報化対象となる二進文字列をxと呼ぶ。
  
• p(y) = xとなるyのうち、最短かつ辞書式最若のものをsと呼ぶ。
  
• pに関するxの最小記述をdp(x)と呼び、それはsであるとする。
  
• Kp(x) = |dp(x)|と定義する。
  
  
• LISPだとしたときの例。
  
• dlisp(x)は、xを出力する最小のLISPプログラム。
  
• Klisp(x)は、そのプログラムの長さ。
  
  
• 定理6.27
  「任意の記述言語pに対して、pだけに依存する定数cが存在して、次が成り立つ。
  　∀x [K(x) <= Kp(x) + c]」
  
  
  
  • ある記述言語pについて、次のようなTM Mを考える。
    
    
    
    • 入力wに対して、p(w)を出力する。
      
    
    
  • xのpによる記述がwであるとする。
    
  • Mは言語Pのインタープリタといえる。
    
  • すると、情報としてのxの記述は、<M,w> となる。
    
  • 定義より、|<M,w>| = |<M>dp(x)| = |<M>| + |dp(x)| = |<M>| + Kp(x)。
    
  • これは、xのアルゴリズムによる最小記述候補だから、
    K(x) <= Kp(x) + |<M>|
    が確認できた。
    
  
  
  
• 圧縮不可能な文字列とランダム性
  
  
• 言葉の定義。
  
• c圧縮可能： K(x) <= |x| - c なるcが存在すること。
  
• xが1圧縮不可能なとき、xは圧縮不可能である、と言う。
  
  
• 定理6.29
  「あらゆる長さに対して、その長さの圧縮不可能な文字列が存在する」
  
  
  
  • おお！ この定理の証明、簡単かつ強力。すごい。
    
  
  
  
• 系6.30
  「長さnの文字列全体で少なくとも2^n-2^(n-c+1)+1個の文字列は、Cで圧縮不可能である。
  
  
• 定理6.31と定理6.32は感じだけ掴んでおく。
  

おお、第二巻の本文を読了した！！
長かった。。。
次回は章末演習。章末演習を越えれば、ついに最終巻だ！

【CL入門】11 入出力 (その2)

こつこつ。「11.8 シャープ・マクロ」。

• シャープ・マクロというディスパッチ機構が用意されているのは、歴史的な経緯なのか意味があるのか。
  

写経に専念。おお、ついに最終章だ。次回は「12 プログラミング」。

【CL入門】11 入出力

こつこつ。

• 「入出力を制するものはプログラミング言語を制する」そうだったのか。。。
  
• とりあえず、「11.7 入力マクロ」まで写経完了。
  
• CLのwrite/readはけっこう深くて、一番の要所なので、今の時点では深掘りはしない。
  

次回は、「11.8 シャープ・マクロ」から。

【シプサ】6 計算可能性の理論における先進的な話題 (その5)

もう一歩、進めるだろうか。

• 6.3 TURING REDUCIBILITY
  
  
• connote: ...を暗示する。...を伴う。...を内包する。
  
• この、oracleの超越機械的な考え方、めちゃくちゃおもしろい。
  
  
• EXAMPLE 6.19を丁寧に理解する。
  
  
  
  • A[TM]のoracleがあるとする。
    
  • それを内包したoracle Turing machineをM^(A[TM])と呼ぶ。
    
  • このM^(A[TM])は通常のTMとくらべると、はるかに強力な判定能力をもっている。
    
  • 例として、E[TM]を判定できることを示す。
    
  • M^(A[TM])を使って、E[TM]を判定する手順を構成する。
    
  • その手順。
    
    
    
    • 入力はTMの表現<M>とする。
      
    • 1. 次のようなTM Nを構築する。
      
      
      
      • 入力は無視する。
        
      • 1. TM M を 全てのw∈Σ* について並列動作させる。(いいのか、こんな設計???)
        
      • 2. 1がいずれかについて受理になるならば、受理する。
        
      
      
    • 2. M^(A[TM])に<N,0>を入力する。すなわち、<N,0>∈A[TM]かどうかを調べる。
      
    • 3. 2の結果が拒否なら、受理する。受理なら、拒否する。
      
    
    
  • さて、この手順にでてくるTM Mが認識する言語が空集合でないならば、Nは<M>を受理する。ゆえに、Nはどんな入力でも受理となるのでもちろん0も受理する。ゆえに、<N,0>∈A[TM]であるから、この手順自体の結果は拒否となる。空集合であるケースも同様の分析で受理となることがわかる。
    
  • よって、この手順は、E[TM]を判定する手順である。
    
  
  
  
• THEOREM 6.21
  A <=T B かつ Bが判定可能ならば、Aも判定可能である。
  
  
  
  • A <=T B ということは、「Aは、Bに相対的には判定可能」ということである。
    
  • すなわち、Bのoracleを用いてAのoracle TMが作れるということだ。
    
  • Bが判定可能ということは、BのoracleはたかだかTMで実現できるものであるということ。
    
  • Aのoracle TMが内包するoracleもたかだかTMであり、すなわちAを判定する通常のTMが存在することになる。■
    
  
  
  
• Turing帰着性は写像帰着性を一般化したものである。
  
  
  
  • 写像帰着性では、計算可能な関数によって、言語間の要素を写像した。
    
  • A <=m B のとき、写像帰着関数は、Aの要素をBの要素に写像し、Aの要素でないものをBの要素でないものに写像した。
    
  • これによって、Aの要素を判定するということが、Bの要素を判定するということの部分問題になるというのが本質であった。
    
  • これはBが判定可能であるならば、Turing帰着性におけるoracleをBが担っているということである。
    
  • 写像帰着関数は、Aからそのoracleを利用するための手順を示していることになる。
    
  
  

進めた。よかった。

【例解UNIX】低水準入出力 (その3)

一週間ぶりにちょっとだけできる。せめて一週間に二回はやらないとあかんな。
3.18 章末問題。

• 三つ星はやらない。
  
• プロセスの後にやるとした節に関係する問題はやらない。
  
• という方針にて。
  
  
• 1. 私家版catをつくる。(約30分)
  
  
  
  • シプサでTuring機械をああだこうだやるなかで、オブジェクトの表現とアルゴリズムとを分離して考えて、なおかつそれを抽象的に解決した上で、プログラミング言語での表現を組み立てる、というのが頭に染み付いてきたきがする。
    
  • 書いてて気がついたのだが、これがいわゆる、データ構造とアルゴリズムということだよね。。。そうか、そういうことだったのか。
    
  • だからアルゴリズムの本のなかには、特定のプログラミング言語ではなく自然言語に近い形で書くものがあるんだな。
    
  
  
  
• 2. 穴をもつファイルをいろいろつくる。(約30分)
  
  
  
  • あんま、おもしろくなかった。
    
  
  
  
• 6. ファイルの操作手順の必要性について。(約5分)
  
  
  
  • open/closeが存在しない場合、read/writeなどがそれらを内包することになる。それは毎回read/writeするたびにopenとcloseをするか、read/writeにそのopen/close処理の指示を与えるかのどちらになる。前者は効率がわるく、後者はopen/closeのロジック記述がread/writeの引数に場所を移しただけなので、得るものがないことにくわえて、OS作成者もアプリ作成者も手間が増える。てな感じではなかろうか。
    
  
  

次回は第四章 標準入出力ライブラリ。

数理論理学のわかりやすさ

シプサで、数理論理学との接続ポイントをやったところで感じたこと。

「論理学をつくる」はとてもよい本だと思うのです。

日頃慣れ親しんでいる日本語に潜む構造と、形式的な論理言語の構成を丁寧にマッチングして組み立てていきます。

しかし、しかしかもしれません。

日本語をその観点で分析するのが、なんだかそのこと自体が難しい気がするのです。シプサのように、数学的言明を対象に一階述語論理(のさわり)を理解するのは何故か比較的簡単でした。

自然言語を対象として論理学を考えるときは、「論理学をつくる」の理解は越えなければいけない最初の壁ですが、計算機を対象として論理学を考えるときは、別の入口があるかもしれない、と感じました。その後で、「論理学をつくる」をやった方がいいかもしれない、ということです。

雑感でした。

【シプサ】6 計算可能性の理論における先進的な話題 (その4)

休日にもう少しすすめたらうれしい。

• "AN UNDECIDABLE THEORY"
  
  
• この節は、詳細な証明(確認)をするのでなく、考え方をざくっとしめすもののようだ。それにそって進みたい。
  
  
• THEOREM 6.13
  Th(N,+,x) is undecidable.
  
• これがこの節のひとつめのお題。
  
• 確認の方針は、A[TM]をTh(N,+,x)に帰着させる、ということ。手法には計算履歴を使う。
  
  
  
  • LEMMA 6.14
    TM Mと入力wがあるとする。これらから、とある論理式をつくることができる。それをΦ[M,w]と呼ぶ。どんな論理式かというと、Mがwを受理するときに限り∃xΦ[M,w]がモデル(N,+,x)にてtrueとなる、すなわちthe language of Th(N,+,x)となるような論理式である。
    
  • これの証明というか、このような機構を構築することはかなり面倒。
    
  • ここでは、これが構築できる、ということにしておく。
    
  
  
• LENNMA 6.14は写像帰着であるから、A[TM] <=m Th(N,+,x) である。よって、A[TM]は判定不可能性により、Th(N,+,x)は判定不可能であるといえる。■
  
  
• 次のお題は、ゲーデルの不完全性定理。
  
• 完全な証明ではなく、そのスケッチをみてみる。
  
• ゲーデルの不完全性定理を簡単に言うと
  「数論において、証明形式や方式についていかなるものを採用したとしても、それをつかって証明不能な数学的言明が存在する」
  ということ。
  
• 証明(proof)の正確な定義を構成する余裕はこの本ではない。
  
• そこで簡単に言うと、
  
  
  
  • 言明Φに対する形式的証明πとは、言明の列である。
    
  • その列をS1, S2, ..., Slと表すとする。
    
  • SlはΦである。
    
  • Siは、Siより前の言明と数に関する基本的な公理とをもとにして、形式化された含意ルール(implication)によって導かれる。
    
  
  
• さて、話しを進めるために次の2つが成り立つと仮定しちゃおう。
  
  
  
  • 1. {<Φ,π> | π is a proof of Φ } は 判定可能。
    
  • 2. ここで採用する証明システムは健全である。すなわち、ある言明の証明が存在するならば、その言明はtrueである。
    
  
  
  
• THEOREM 6.15
  Th(N,+,x)をもとにして証明可能な言明を集めた部分集合をつくると、それはTuring認識可能である。
  
• これの証明は簡単。上記1を使えばよい。
  
  
• THEOREM 6.16 (不完全性定理 Th(N,+,x)版)
  Th(N,+,x)の一部の言明は、証明不可能である。
  
  
  
  • 背理法で確認していく。
    
  • 「Th(N,+,x)の全ての言明(すなわちtrueとなる言明)は証明可能である」とする。
    
  • この仮定を利用してアルゴリズムDを構成する。
    
  • さて、THEOREM6.15の認識可能ということを実現するアルゴリズムをPとする。
    
  • 言明入力Φから、Φと¬Φをつくり、双方についてアルゴリズムPを適用させる。
    
  • Φと¬Φのどちらかはtrueだから、仮定によると、そのtrueな方は証明可能である。
    
  • これはまさにTHEOREM6.15によって認識可能ということだから、先のアルゴリズムPの適用はどちらかが受理し停止する。
    
  • さて、どちらで受理したとしても、受理した方がtrueである。これは上の2によって保証されている。すなわち、Φで受理すれば、Φはtrue。¬Φで受理すれば、Φはfalse。
    
  • このアルゴリズムDは、Th(N,+,x)を判定している。これはTHEOREM6.13に反している。よって仮定は間違いである。■
    
  
  
  
• うわ、次、再帰定理を使うのか。。。
  
  
• 再帰定理を使って、(N,+,x)に関する言明で証明不可能なものを作ってみる、ということ。
  
  
• 次のようにTM Sを構成する。
  
  
  
  • あらゆる入力に対して次のように動作する。
    
  • 1. 再帰定理を使って、自分自身の記述<S>を得る。
    
  • 2. LEMMA 6.14をつかって、言明ψ = ¬∃c [Φ[S,0]] を構成する。
    
  • 3. THEOREM6.15のアルゴリズムPを、入力ψにて動作させる。
    
  • 4. 3で受理すれば受理、拒否すれば拒否。
    
  
  
• 実はこのψが、trueだがunprovableな言明である。それを確かめる。
  
  
• 入力を(どうせ無視するが)0としておこう。
  
• TM Sは受理するか拒否するか、である。
  
  
• TM Sが受理するのは、3.でPが受理したとき。
  
• Pが受理するということは、言明ψが証明可能ということ。
  
• 一方、TM Sは受理するんだから、∃c [Φ[S,0]] はtrue。
  
• ということは、¬∃c [Φ[S,0]] = ψ がfalse。
  
• あり、このケースは、falseなものが証明可能となっている、というケースであることがわかった。
  
• これは証明システムの事実2.に反している。
  
• よってこのケースは発生しえない。
  
  
• というわけで、次のケースが発生することがわかった。
  
  
• TM Sが拒否するのは、3.でPが拒否したとき。
  
• Pが受理するということは、言明ψが証明不可能ということ。
  
• 一方、TM Sは拒否するんだから、∃c [Φ[S,0]] はfalse。
  
• ということは、¬∃c [Φ[S,0]] = ψ がtrue。
  
  
• ψは、証明不可能かつtrueである。■
  

こつこつ。次回は「Turing帰着性」。

【CL入門】10 さまざまなデータ

写経。

• 文字のtype-specifierについて、この本では、'string-charとあるが、ansiでは、'character。
  
• aclではエラーにならない。
  

  
  CL-USER(99): (concatenate 'string '(a b))
  "?髓"
  CL-USER(100):
  

  
  

基本的なリテラルとデータ構造に関してなので、すんなり。

【シプサ】6 計算可能性の理論における先進的な話題 (その3)

休日なので、シプサができる！

• 前回のTh(M)の定義の訳が誤訳な予感。"the" collection of true sentences なので、trueとなるsentenceを全て集めたものがTh(M)。
  
• 脚注によると、modelは、interpretationとかstructureとかとも言うそうな。
  
  
• さて、"A DECIDABLE THEORY"。
  
  
• Theorem 6.12 Th(N, +) is decidable.
  
  
• これをやるまえに、問題1.31と1.32をやっておいた方がよさそうだ。第一章正規言語の問題だが。
  
  
• 問題1.31
  
  
  
  • A^R = {w^R | w ∈ A}について、AがregularならA^Rもreguralを確認せよ、ということ。
    
  • これは正規表現の帰納的な定義において、各ルールについてA^R版を考えられるので、まあ当然。
    
  
  
  
• 問題1.32
  
  
  
  • Σ3 = {000, 001, 010, 011, 100, 101, 110, 111}
    
  • B = {w ∈ Σ3* | 3n+1番目の文字をならべて数値と解釈した数と、3n+2番目を並べて数値と解釈した数との和が、3n+3番目を並べて数値と解釈した数に等しい。n={0,1,2,3,...}}
    
  • 例：
    001100110 ∈ B
    001101 !∈ B
    
  • このBがregularであることを示せ。
    
  • B^Rがregularであることを示す。そのregular expressionを具体的に構成する。
    
    
    
    • まず、しらべてみる。
      
    • 単一で要素たりえるもの。
      000, 011, 101
      
    • 二つで要素たりえるもの。(単二)
      単一○単一
      110001
      
    • 三つで要素たりえるもの。(単三)
      単二○単一
      単一○単二
      110 111 001
      110 010 001
      110 100 001
      
    • 四つで要素たりえるもの。(単四)
      単三○単一
      単一○単三
      単二○単二
      110 111 111 001
      110 010 111 001
      110 100 111 001
      
      110 111 010 001
      110 010 010 001
      110 100 010 001
      
      110 111 100 001
      110 010 100 001
      110 100 100 001
      
    • 規則性が見えてきた。
      (000∪011∪101∪(110○hoge○001))*
      で、hogeが、
      (010∪100∪111)*
      である。まとめると
      (000∪011∪101∪(110○((010∪100∪111)*)○001))*
      となる。(εをみとめないなら末尾を+に)
      
    
    
  • しかし、足し算というのが正規言語に過ぎない、というのは結構すごいことだな。。。
    
  
  
  
• さて、本題。Theorem 6.12。
  
  
• 頭の中で考えてみたが、どうも集中できない、というかわからない。そこでメモをやる。
  
  
• 証明の方針検討。
  
  
  
  • まず、言明Φを判定するアルゴリズムを考える、という目標設定。
    
  • Φの表現を次のものにする。
    Φ=Q1x1Q2x2...Qlxl[ψ]
    ここでQ1...Qlはコンティフィア。ψはコンティフィアを含まず、変数x1...xlをもつ。
    
  • さて、for (i = 0; i <= l; i++)的に、
    Φ[i]=Q[i+1]x[i+1]Q[i+2]x[i+2]...Q[l]x[l] [ψ]
    をつくる。するとi=0のとき、上のΦに等しいことがわかる。
    Φ[0] = Φ
    続けると、
    Φ[1] = ΦからQ[1]x[1]をとったもの、
    ...
    Φ[l-1] = Q[l]x[l] [ψ]
    Φ[l] = ψ
    となる。
    
  • するとΦ[i]はi個の自由変数をもつ。
    
  • で、a1,...,ai∈N、として、その自由変数に当てはめたものを、Φ[i](a1,...,ai)と表記する。
    
  • で、for (i = 0; i <= l; i++)のそれぞれのiにおいて、
    
    
    
    • このΦ[i](a1,...,ai)があるわけだが、
      
    • これをtrueとする、a1,...,aiを認識するFA A[i]を構築する。
      
    • 構築のプランは、
      
      
      
      • まずA[l]を構築する。
        
      • A[i]からA[i-1]が構築できることを示す。
        
      
      
    • というもの。
      
    • 構築の結果、A[0]が得られれば、それはΦをtrueにする自由変数の入力を判定するものである。
      
    • ところで、Φに自由変数はない。
      
    • よって、Φが真ならば、A[0]はεを受理するはずである。偽ならば、拒否するはずである。
      
    
    
  
  
  
• 方針決定。
  
• ミソはAの構築であろう。そこを重点的に読む。
  
  
• Aの構築。
  
  
  
  • A[i]のアルファベットは、問題1.32の拡張で、
    Σ[i] = {[0...00], [0...01], [0...010], ... , [1...11]}.
    で、それぞれの要素はi個の0or1を含むものとする。
    また、
    Σ[0] = {[]}.
    とする。
    
    
  • まず、A[l]を構成できるかどうか。
    
  • さて、モデル(N,+)の話をしているのだから、ψというのは{∧, ∨, ¬, (,), R, x}からなり、RはPLUSであるものにすぎない。
    
  • 一方で、問題1.32でみたように、PLUS(a,b,c)の入力たるa,b,cを認識するFAは構築可能である。
    
  • ψを構成するには、PLUSをもとにして、前掲の論理演算で帰納的に組み立てていくしかない。
    
  • ここで、PLUS(a,b,c)をみたすabcの組はtuple alphabetにおいて正規言語をなし、正規言語は、前掲の論理演算に関して閉じているので、結果得られる言語(ψに関する言語)も正規言語である。
    
  • というわけでA[l]は構成できる。
    
    
  • 次にA[i+1]からA[i]を構成できるかどうか。
    
  • A[i+1]が存在すると仮定する。
    
    
    
    • ところで、A[i+1]とは何か?
      
    • Φ[i+1](a1,...,a[i+1])をtrueとする、a1,...,a[i+1]の表現たる言語を認識するFA。ここで、a1,...,a[i+1]の表現は、Σ[i+1] = {[0...0],[0...1],...,[1...1]}としたときのΣ[i+1]*をなし、Σ[i+1]*の要素の解釈はi+1-tupleのk番目の0or1を集めて連結したものがakであるというもの。
      
    • 違う言葉でいうと、Φ[i+1]は自由変数をi+1個もつが、それぞれにa1,...,a[i+1]をいろいろあてはめていき、Φ[i+1]がtrueになるものだけを集めた言語。
      
    • A[i+1]は、Σ[i+1]*を入力として、前項をみたすものだけ受理する。
      
    
    
  • A[i]を構成する。
    
  • まず、Φ[i]とΦ[i+1]の関係は、これらの定義から、Φ[i] = ∃x[i+1]Φ[i+1]であるか、Φ[i] = ∀x[i+1]Φ[i+1]であるかのいずれかである。
    
  • ∀xP(x) <=> ¬∃x¬P(x)だから、後者は、前者に帰着できる。よって、前者さえ構成できればよい。そこで前者の構成。
    
    
    
    • まず、A[i]は状態として、A[i+1]のものと、新しい開始状態をもつ。
      
    • そして、A[i]に入力[b1 ... b[i-1] b[i]]が与えられるたびに、A[i+1]の入力足りえる[b1 ... b[i-1] b[i] z]を想定する。
      
    • ここで「想定する」とは、zが0or1であるとして非決定的に状態遷移する、ということ。
      
    • で、すべての入力を処理し、非決定的な状態遷移を終えたときに、A[i+1]の受理状態にいるならば、それはその受理状態に辿りつくためのzの部分を連結して作ったa[i+1]にて、Φ[i]がtrueである、ということなので、そのときのa1,...,aiをA[i]は受理する。それ以外は拒否する。
      
    • これでA[i]を構成できた。
      
    
    
  
  

たかが、こつこつ。されど、こつこつ。

【CL入門】9 宣言 (その2)

こつこつ。

• 9.1 動的なバインディングを自分なりに確認。
  
  
• ;; 追記 ここでは「環境」という概念というか言葉をつかわずにバインディングやスコープについて整理してみる、という方針。一般的には、環境をつかった方が理解ははるかに簡単。
  
  
• まず、動的ってどういうことなんだろ?
  
• 変数の値の決まり方の一種、かな。
  
• 実行時には、変数の値が存在するか、しないかのどちらかだ。
  
• 存在しない場合は実行エラーとなる。なので、ここでは無視する。
  
• すると実行時には、変数の値は必ず存在する。
  
• 次に外部からの入力が無いとすると、あるプログラムが実行する計算は決まっている。(逆にその計算を実行するためにつくったのがプログラムなのだが)
  
• すると、動的/静的といったって、それは何かプログラムの書きぶりのたぐいの話であり、できあがったプログラム(実行)という観点でみれば、決まっているものでしかないということ。
  
  
• 曖昧な表現になってしまうのだが、top-level(REPL)で定義した変数は、大域変数となる。
  
• ここで、大域、というのは、その変数は、同じREPLが存続している間、どこでもアクセス可能なことを指す(転じて、いつでもアクセス可能)。
  

  
  CL-USER(2): (setq x 0)
  0
  CL-USER(3): x
  0
  ;xという変数は、このREPLが終了するまで存在する。
  

  
  
• 大域変数へのアクセスは、top-level以外でも可能である。
  
• 大域変数へアクセスするには、
  
  
  
  • symbol-value/setを使う。
    
  • 大域変数しか参照の結果として得られないようなスコープ状態にする。
    
  
  などの方法がある。
  

  
  CL-USER(6): (let ()
                (+ x 1))
  1
  CL-USER(7): (let ((x 100))
                (+ x 1))
  101
  CL-USER(10): (let ((x 100))
                (+ (symbol-value 'x) 1))
  1
  

  
  
• 大域変数というのは局所変数の自然な延長ではない。というのは、局所変数どうしのスコープも階層的になることがあり、
  

  
  CL-USER(11): (let ((x 10))
                 (let ((x 100))
                   (+ x 1)))
  101
  

  
  これは大域変数と局所変数における、
  

  
  CL-USER(13): (setq x 10)
  10
  CL-USER(14): (let ((x 100))
                 (+ x 1))
  101
  

  
  というものと同じような関係性ではないか、と思えるが、差異が存在する、ということ。
  (おそらく、これが同じ関係性になっているのがMLのREPLなはず。)
  
• 違う点は何か?
  
• それは、まず第一に、
  

  
  CL-USER(11): (let ((x 10))
                 (let ((x 100))
                   (+ x 1)))
  101
  

  
  では、(let ((x 10)) ...で定義したxに、(let ((x 100)) ...)の...の中からアクセスする方法が存在しないが、
  

  
  CL-USER(13): (setq x 10)
  10
  CL-USER(14): (let ((x 100))
                 (+ x 1))
  101
  

  
  において、(let ((x 100)) ...)の中で、その「外側」の(setq x 10)にアクセスする方法があるということ。
  

  
  CL-USER(15): (let ((x 100))
                 (+ (symbol-value 'x) 1))
  11
  

  
  
  
• これを基礎として、setqの振舞をみる。setqは大域変数を特別視しない。
  

  
  CL-USER(57): (setq x 1)
  1
  CL-USER(58): (setq x (1+ x))
  2
  CL-USER(59): x
  2
  CL-USER(60): (setq x 1)
  1
  CL-USER(61): (let ((x 10))
                 (setq x (1+ x)))
  11
  CL-USER(62): x
  1
  CL-USER(63): (setq x 1)
  1
  CL-USER(64): (let ((x 10))
                 (let ((x 100))
                   (setq x (1+ x)))
                 x)
  10
  CL-USER(65): x
  1
  

  
  
  
• setは特別視する。それによって指されるのは、局所変数を突きぬけて、大域変数である。
  

  
  CL-USER(66): (set 'x 1)
  1
  CL-USER(67): x
  1
  CL-USER(68): (set 'x (1+ x))
  2
  CL-USER(69): x
  2
  CL-USER(70): (set 'x 1)
  1
  CL-USER(71): (let ((x 10))
                 (set 'x (1+ x)))
  11
  CL-USER(72): x
  11
  CL-USER(73): (set 'x 1)
  1
  CL-USER(74): (let ((x 10))
                 (let ((x 100))
                   (set 'x (1+ x)))
                 x)
  10
  CL-USER(75): x
  101
  

  
  おまけ。
  

  
  CL-USER(78): (boundp 'y)
  NIL
  CL-USER(79): (let ((y 2))
                 (set 'y y))
  2
  CL-USER(80): (boundp 'y)
  T
  

  
  
  
• これらを基礎として関数はどうなるか。
  
• まず、top-levelにてdefunで作る関数はクロージャをつくらない。
  

  
  CL-USER(23): (setq x 1)
  1
  CL-USER(24): (defun f () 
                 (+ x 1))
  F
  CL-USER(25): x
  1
  CL-USER(26): (f)
  2
  CL-USER(27): (setq x 100)
  100
  CL-USER(28): x
  100
  CL-USER(29): (f)
  101
  CL-USER(30): x
  100
  

  
  ※これ、先のことと同じだが、MLではレキシカルなので(setq x 1)がずっと効いたはず。
  
• lambdaも同じ。top-levelではクロージャをつくらない。
  

  
  CL-USER(35): (setq x 1)
  1
  CL-USER(36): (setq g #'(lambda () (+ x 1)))
  #
  CL-USER(37): x
  1
  CL-USER(38): (funcall g)
  2
  CL-USER(39): x
  1
  CL-USER(40): (setq x 100)
  100
  CL-USER(41): (funcall g)
  101
  CL-USER(42): x
  100
  

  
  
• 比較として、クロージャをなすのはどういうときか? 局所変数どうしの重なりにおいてはクロージャをなす。
  

  
  CL-USER(45): (let* ((x 1)
                      (h #'(lambda () (+ x 1))))
                 (let ((x 100))
                   (funcall h)))
  2
  

  
  
  
• ここまでのことを整理しよう。大域変数だ局所変数だ、というのは、プログラムの実行の流れにおいて、値の参照のルールがどうなっているかという話題である。
  
• それはプログラマの関心からすると次のように整理できる。
  
• まずは、ジャンプしない流れでの関心。
  
  
  
  • ある記号の値を参照するとき、それが何か。例： (+ x 1)のxは何?
    
  • ある記号の値を設定するとき、どの記号を設定するか。例。(let ((x 1)) (let ((x 2)) (setq x (+ x 1)))の(setq x のxは何か。
    
  
  
• 次にジャンプする流れでの関心。
  関数によって実行の流れがジャンプする。そのとき、ジャンプした先のコード(関数定義の中のコード)が、ジャンブする前との兼ね合いがありつつ、前項の話題がどうなるのか、ということ。
  
  
  
  • ある記号の値を参照するとき、それが何か。例： 関数定義の中の、(+ x 1)のxは何?
    
  • ある記号の値を設定するとき、どの記号を設定するか。例。関数定義の中の、(let ((x 1)) (let ((x 2)) (setq x (+ x 1)))の(setq x のxは何か。
    
  
  
  
• では関数でジャンプした先での「値の設定」がどうなっているかということを調べてみよう。
  
• まず、setは大域LOVEなので、とにかく大域を指す。
  

  
  CL-USER(81): (setq x 1)
  1
  CL-USER(82): (defun f ()
                 (set 'x 2))
  F
  CL-USER(83): x
  1
  CL-USER(84): (f)
  2
  CL-USER(85): x
  2
  CL-USER(86): (setq x 1)
  1
  CL-USER(87): (let ((x 10))
                 (f))
  2
  CL-USER(90): x
  2
  

  
  
• そして、setqもdefunの中では大域を指す。
  

  
  CL-USER(91): (setq x 1)
  1
  CL-USER(92): (defun f ()
                 (setq x 2))
  F
  CL-USER(93): x
  1
  CL-USER(94): (f)
  2
  CL-USER(95): x
  2
  CL-USER(96): (setq x 1)
  1
  CL-USER(97): x
  1
  CL-USER(98): (let ((x 10))
                 (f)
                 x)
  10
  CL-USER(99): x
  2
  

  
  
• 局所変数のかさなりでは、クロージャをなし、setqは定義時の変数を指す。
  

  
  CL-USER(103): (let* ((x 10)
                       (g #'(lambda () (setq x 2))))
                  (print x)
                  (let ((x 100))
                    (print x)
                    (funcall g)
                    (print x))
                  (print x))
  10
  100
  100
  2
  2
  CL-USER(104): 
  

  
  
  
• これから、やはりsetqは大域変数を特別視しないことがわかる。
  
  
• また、大域(top-level)にしても、局所(let内)にしても、「同じ階層にいるとき」、setqについては、あまりレキシカルという感じはしない。つまりレキシカルというのは、スコープが階層構造をなす状況において、どの階層での実行が何を指すかについて言っているものだ、ということ。
  

  
  CL-USER(158): (setq x 1)
  1
  CL-USER(159): (setq g #'(lambda () (setq x (1+ x))))
  #
  CL-USER(160): (setq x 10)
  10
  CL-USER(161): (funcall g)
  11
  CL-USER(162): (let ((x) (g))
                  (setq x 5)
                  (setq g #'(lambda () (setq x (1- x))))
                  (setq x 50)
                  (funcall g))
  49
  CL-USER(163): (funcall g)
  12
  

  
  
  
• さて、top-levelを根っことしてletなどを使って局所変数にて階層をつくってきたのが、ここまでの作業。letなどを使うことによって、大域-局所-局所-...という階層ができたのだ(これを造語だがlet階層と呼ぶ)。そこでは、「大域-局所」なるかさなりの関係と、「局所-局所」なるかさなりの関係の調査がメインであった。
  
• ここで、progvを導入する。progvは、letなどとは別のかたちで、階層を成すことができる。(これを造語だが、progv階層と呼ぶ)
  

  
  CL-USER(164): (setq x 0)
  0
  CL-USER(165): (defun f () (setq x (1+ x)))
  F
  CL-USER(166): (f)
  1
  CL-USER(167): (progv '(x) '(100) (f) x)
  101
  CL-USER(168): x
  1
  CL-USER(169): (setq x 0)
  0
  CL-USER(170): (defun f () (setq x (1+ x)))
  F
  CL-USER(171): (f)
  1
  CL-USER(172): (progv '(x) '(100)
                  (progv '(x) '(1000)
                    (f) x))
  1001
  CL-USER(173): x
  1
  CL-USER(175): (progv '(x) '(100)
                  (progv '(x) '(1000)
                    (f) x)
                  (f) x)
  101
  CL-USER(176): x
  1
  

  
  
  
• CLの仕様としては、let階層を基本として、その根であるtop-level(大域)について、直交としてprogv階層があるという感じか。
  
• progv階層の影響をうけるのは、まず、set/symbol-value。
  
• これはprogv階層に準拠してスコープされる。
  
• 次に、top-levelでの関数定義内のsetq。
  
• これはlet階層では、その階層で呼出したとしても、常に定義時たる大域の記号を指していたが、progv階層では、それが呼び出された階層の記号を指す。(★これが動的ということ★)
  
• let階層を基本として直交というのは、let階層とprogv階層が混在しているとき、set/symbol-valueなどの大域にアクセスするものでなければ、記号参照はletのルールに従うということ。
  
• これらを確認する例。
  

  
  CL-USER(179): (setq x 'top-setqed)
  TOP-SETQED
  CL-USER(180): (defun f () (setq x 'fun-setqed))
  F
  CL-USER(181): (let ((x 'letted))
                  (progv '(x) '('progved)
                    (list x (symbol-value 'x) (f))))
  (LETTED 'PROGVED FUN-SETQED)
  CL-USER(182): x
  TOP-SETQED
  

  
  
  
• これらの状況をひとことであらわすと、
  「局所変数は静的(staticまたはlexical)なバインディングであり、大域変数は動的(dynamic)なバインディングである」
  ということ。
  
  
• エクステントは、「いつ(まで)」その変数を利用できるかということ。
  
• 静的バインディングは(クロージャをつくるので)不定である。動的バインディングは(クロージャをつくらないので)フォームの実行時のみである。
  

  
  CL-USER(183): (setq hoge #'(lambda ()
                               (let ((x 100))
                                 #'(lambda () (setq x (1+ x))))))
  #<Interpreted Function (unnamed) @ #x1000bdf1f2>
  CL-USER(184): (funcall hoge)
  #<Interpreted Closure (unnamed) @ #x1000bfcf92>
  CL-USER(185): (setq hoge1 (funcall hoge))
  #<Interpreted Closure (unnamed) @ #x1000c34fa2>
  CL-USER(186): (funcall hoge1)
  101
  CL-USER(189): (funcall hoge1)
  102
  CL-USER(190): (setq hoge2 (funcall hoge))
  #<Interpreted Closure (unnamed) @ #x1000cb92f2>
  CL-USER(191): (funcall hoge2)
  101
  CL-USER(192): (funcall hoge1)
  103
  CL-USER(193): (setq piyo #'(lambda ()
                               (progv '(x) '(100)
                                 #'(lambda () (setq x (1+ x))))))
  #<Interpreted Function (unnamed) @ #x1000d98392>
  CL-USER(194): (setq x 0)
  0
  CL-USER(195): (setq piyo1 (funcall piyo))
  #<Interpreted Function (unnamed) @ #x1000e01c42>
  CL-USER(196): (funcall piyo1)
  1
  CL-USER(197): (funcall piyo1)
  2
  CL-USER(198): (setq piyo2 (funcall piyo))
  #<Interpreted Function (unnamed) @ #x1000e3f892>
  CL-USER(199): (funcall piyo2)
  3
  CL-USER(200): (funcall piyo1)
  4
  

  
  
  
• さて、スペシャル変数。
  
• proclaim: ...を公表する, 宣言する, 公布する。
  
• let階層のお話。
  
• proclaimした変数(記号)は、大域(top-level)所属になり、かつ、動的バインディングになる。
  
• ちょっとずつ確認。
  
• letはprogvがごとし、かな。ま、このかぎりにおいて、letもprogvも振舞いはそもそもかわらんのだが。
  

  
  CL-USER(201): (setq x 0)
  0
  CL-USER(202): (let ((x 1)))
  NIL
  CL-USER(203): x
  0
  CL-USER(207): (proclaim '(special x))
  T
  CL-USER(208): (let ((x 1)))
  NIL
  CL-USER(209): x
  0
  CL-USER(210):
  

  
  
• setqはsetがごとし、かな。
  

  
  CL-USER(210): (let ((x 1))
                  (setq x x))
  1
  CL-USER(211): x
  0
  

  
  
• う、違った。setqはあくまで自分がいる階層をみているし、大域変数としてのprogv的スコープが発生している。
  
• そうするとやはり★のところが動的たるところで、これがlet階層でも発生する、ということか。
  

  
  CL-USER(211): x
  0
  CL-USER(212): (defun f ()
                  (setq x (1+ x)))
  F
  CL-USER(213): (f)
  1
  CL-USER(214): x
  1
  CL-USER(215): (let ((x 10))
                  (f)
                  x)
  11
  CL-USER(216): x
  1
  CL-USER(217): (setq y 0)
  0
  CL-USER(218): (defun g ()
                  (setq y (1+ y)))
  G
  CL-USER(219): (let ((y 10))
                  (g)
                  y)
  10
  CL-USER(220): y
  1
  

  
  
• やはり、そうだ。
  
  
• ではクロージャはどうなる。
  

  
  CL-USER(2): (setq hoge #'(lambda ()
                             (let ((x 100))
                               #'(lambda () (setq x (1+ x))))))
  #<Interpreted Function (unnamed) @ #x1000ae19a2>
  CL-USER(3): (setq hoge1 (funcall hoge))
  #<Interpreted Closure (unnamed) @ #x1000b336a2>
  CL-USER(4): (funcall hoge1)
  101
  CL-USER(7): (funcall hoge1)
  102
  CL-USER(8): (setq hoge2 (funcall hoge))
  #<Interpreted Closure (unnamed) @ #x1000ba3a22>
  CL-USER(9): (funcall hoge2)
  101
  CL-USER(10): (proclaim '(special x))
  T
  CL-USER(11): (funcall hoge2)
  102
  CL-USER(12): (funcall hoge1)
  103
  CL-USER(13): (funcall hoge1)
  104
  CL-USER(14): (funcall hoge1)
  105
  CL-USER(15): (funcall hoge1)
  106
  CL-USER(17): (funcall hoge1)
  107
  CL-USER(18): (funcall hoge2)
  103
  CL-USER(19): (setq hoge3 (funcall hoge))
  #<Interpreted Closure (unnamed) @ #x1000c66b72>
  CL-USER(20): (funcall hoge3)
  Error: Attempt to take the value of the unbound variable `X'.
    [condition type: UNBOUND-VARIABLE]
  
  Restart actions (select using :continue):
   0: Try evaluating X again.
   1: Use :X instead.
   2: Set the symbol-value of X and use its value.
   3: Use a value without setting X.
   4: Return to Top Level (an "abort" restart).
   5: Abort entirely from this (lisp) process.
  [1] CL-USER(21): :reset
  CL-USER(22): (setq x 0)
  0
  CL-USER(23): (funcall hoge3)
  1
  CL-USER(24): (funcall hoge3)
  2
  CL-USER(25): (funcall hoge1)
  108
  CL-USER(26): (funcall hoge2)
  104
  CL-USER(27):
  

  
  
• おお、specialにした後から、クロージャをつくらなくなる!
  
  
  
• で、declare
  
• まず基本的なスコープ動作確認。
  

  
  CL-USER(2): (setq x 'top)
  TOP
  CL-USER(3): (let ((x 'local))
                (let ((x 'special))
                  (declare (special x))
                  (let ((x 'local2))
                    )))
  NIL
  CL-USER(4): x
  TOP
  

  
  
• 通常の、大域変数の関数内利用における振舞い。let階層では動的バインディングしない。
  

  
  CL-USER(5): (defun f ()
                (setq x (cons 'called x)))
  F
  CL-USER(6): (f)
  (CALLED . TOP)
  CL-USER(7): x
  (CALLED . TOP)
  CL-USER(8): (setq x 'top)
  TOP
  CL-USER(9): x
  TOP
  CL-USER(10): (let ((x 'local))
                 (f))
  (CALLED . TOP)
  CL-USER(11): x
  (CALLED . TOP)
  

  
  
  
• declare specialによって、let階層でも動的バインディング。
  

  
  CL-USER(12): (let ((x 'special))
                 (declare (special x))
                 (f))
  (CALLED . SPECIAL)
  CL-USER(13): x
  (CALLED . TOP)
  

  
  
  
• おまけ。proclaim specialによるlet階層での動的バインディング。
  

  
  CL-USER(16): (setq x 'top)
  TOP
  CL-USER(19): (proclaim '(special x))
  T
  CL-USER(20): x
  TOP
  CL-USER(21): (let ((x 'let))
                 (f)
                 x)
  (CALLED . LET)
  CL-USER(22): x
  TOP
  

  
  
  
• aclのdefvarとdefconstant。
  

  
  CL-USER(25): (macroexpand '(defvar *x*))
  (PROGN (DECLAIM (SPECIAL *X*)) (RECORD-SOURCE-FILE '*X* :TYPE :SPECIAL-DECLARATION) '*X*)
  T
  CL-USER(26): (macroexpand '(defconstant one 1))
  (PROGN (DECLAIM (SPECIAL ONE)) (EVAL-WHEN (COMPILE) (EXCL::DEFCONSTANT1 'ONE 1)) (RECORD-SOURCE-FILE 'ONE :TYPE :VARIABLE) (EXCL::DEFCONSTANT2 'ONE 1))
  T
  

  
  

うーん、少々掘ってしまった。しかし、宣言に関するモヤモヤがすこし整理できた。
次回は「さまざまなデータ」。

【CL入門】9 宣言

業務繁忙にて、まとまった時間がとれない。休み時間とかにちょこちょこCL入門だけでも進めるしかない。

• バインドって何だっけ、、、そうか、(環境に)新しい記号とそれが指す値を登録することだ。
  
• おお、progvをつかうと、大域変数のスコープを動的にできるんだ。ん? 違うか、大域変数はそもそも動的であり、それの制御にprogvが使えるってことか。
  
• このあたりがREPL(=大域の一形態)の特質につながっているのだな。
  

  
  CL-USER(152): (defun cnt ()
                  (setq x (1+ x)))
  CNT
  CL-USER(153): (setq x 0)
  0
  CL-USER(154): (cnt)
  1
  CL-USER(155): x
  1
  CL-USER(156): (progv '(x) '(2) (cnt) x)
  3
  CL-USER(157): x
  1
  CL-USER(158): (let ((x 2))
                  (cnt)
                  x)
  2
  CL-USER(159): x
  2
  

  
  
• バインドの認識は冒頭のものでは不十分かもしれない。スコープの概念がないからだ。
  
• 宣言がらみは、スコープ、エクステント、環境というののどれを主軸に理解するか、がちょっと複雑。
  
• 今は写経なので、深掘りしない。
  

とりあえず、スペシャル変数の前まで写経。
一章すら進まないが、こつこつ。

【CL入門】8 リスト処理

こつこつ。

• えっと、リストってなんだっけ。。。そっか、第一階層のコンスセルの連鎖がnil終端されているもの、だ。リストじゃないものは、atom、cons cell (cdr がnilじゃないもの)、dotted listなどなど。ただ、nilは両生類か。'()なら空リストだし。試す。
  

  
  CL-USER(3): (listp (list 'a 'b))
  T
  CL-USER(4): (listp 'a)
  NIL
  CL-USER(5): (listp (cons 'a 'b))
  T
  CL-USER(6): (listp nil)
  T
  CL-USER(7): (atom nil)
  T
  

  
  おお、cons cellはlistなのか?
  

  
  CL-USER(8): (cons 'a 'b)
  (A . B)
  CL-USER(9): (consp (cons 'a 'b))
  T
  CL-USER(10): (consp (list 'a 'b))
  T
  CL-USER(11): (consp nil)
  NIL
  CL-USER(12): (listp nil)
  T
  

  
  ふむ、listpとconspは違いがあるにはあるが、listpはほぼconspだ。
  あ、P106に説明があった。。。「listpという述語がある。その名前のために、リストかどうかを判定する述語だと誤解しやすいので注意しておこう。」そりゃ、誤解するってば、、、
  listなんぞや、は私の冒頭の理解でよさげ。
  
• この本、関数の引数で関数をわたすとき、ほぼfunctionでまれにquoteだったりするんだけど意図あるのかな。また意味あるのかな? クロージャが必要になるケースが例になってないので、その限りにおいてはどっちでもよいと思うのだが。
  

  
  CL-USER(78): (mapcar 'cons '(a b c) '(1 2 3 4 5 6))
  ((A . 1) (B . 2) (C . 3))
  CL-USER(82): (mapcar #'cons '(a b c) '(1 2 3 4 5 6))
  ((A . 1) (B . 2) (C . 3))
  CL-USER(79): (mapcar #'(lambda (x) (* x x))
                       '(7 2 3 8))
                       (mapcar #'(lambda (x) (* x x))
                       '(7 2 3 8))
  (49 4 9 64)
  CL-USER(80): (mapcar '(lambda (x) (* x x))
                       '(7 2 3 8))
  (49 4 9 64)
  

  
  
• pリストについて、細かいところがこの本とaclではちょこちょこ違う。aclにあわせて理解しておく。
  

次回は宣言。結構大事なところなのだが、この本ではどんな書きぶりなんだろー。

【CL入門】7 マクロ

虚心坦懐、写経に集中、、、深掘りしない、深掘りしない。

• aclでは、
  

  
  CL-USER(130): (macroexpand '(incf x))
  (SETQ X (+ X 1))
  

  
  
• aclでは、special-form-pは存在しなくて、special-operator-p。
  
• マクロは関数である、ということにフォーカスした説明だな。マクロ理解における5W1HのなかのWhatと、Howの半分を集中して説明する感じ。これはこれでわかりやすい。が、マクロのWho、When、Where、Whyをまったく知らない人には、すわりがわるいかも。
  
• 最近「マクロ」をみると「マグロ」にみえる。上の文では、「マグロは関数である、ということにフォーカスした説明だな。マグロ理解における...」と頭の中で自動変換される。なので、常に鮪が頭に浮かぶ。そしてそれがマグロとした場合にどういう意味をもつのかというマグロ意味論を自動的に考えてしまう。鮪、邪魔だ！　アホらしい。頭がおかしくなってるのかな。。。いや、おかしくなってるよね。
  
• そうか、自分が書くかぎりでは、macroと書けばいいんだ。
  
  
• う、aclでは、'`(if ,condition (progn ,@body))は展開されない。
  

  
  CL-USER(193): '`(if ,condition (progn ,@body))
  `(IF ,CONDITION (PROGN ,@BODY))
  

  
  macroexpandしてみる。
  

  
  CL-USER(195): (macroexpand '`(if ,condition (progn ,@body)))
  (EXCL::BQ-LIST `IF CONDITION (EXCL::BQ-CONS `PROGN BODY))
  

  
  ふむ。
  

次回はリスト処理。こつこつ。

【シプサ】6 計算可能性の理論における先進的な話題 (その2)

上半期末に向けて、業務が膨大に、、、
されど、こつこつ。
「6.2 Decidability of logical theories」から。

• ある数学的言明(statement)が真かどうかを判定するアルゴリズムがあるかどうか、ということは、もちろんその言明が属している数学のドメインによる。判定するアルゴリズムがあるドメインもあるし、それが存在しないドメインもある。
  
• このことをTMで扱うために、言語をつくる。
  
• その言語に含まれる要素は、真である(ある特定された対象ドメインに属する)数学的言明の表現である。
  
• 数学的言明というオブジェクトの表現方法を決める。文字列で表現するルールをきっちり定める、ということ。
  
• ここで定めているのは、一階述語論理っぽい。
  
  
• R(x1, ..., xj)のかたちのもの = atomic formula
  
• 構成ルールにしたがって、atomic formulaからつくったもの = well-formed formula (単にformulaと言うときはこれ)
  
• formulaで、コンティフィアが冒頭にしかないもの = prenex normal form
  
• formulaで、no free variableなもの = sentence or statement
  
  
• さて、これでformulaを整備できた。違う言葉でいうと、数学的言明を表現する方式を確立した。
  
  
• あと、やらねばならぬことが2つ。
  
  
• ひとつは、variableってなんじゃないな、ということ。
  
• それはvariableの値になりうるのはこれこれですよということを明確にする集合があるとする。
  
• その集合をUniverseと呼ぶ。
  
• これを具体的に割当てる必要がある。(これが意味論?)
  
• つぎに、Relationsというのは第一章で確認済みな真偽値を値とする写像なんだが、
  
• この言語におけるRelationsシンボルが、どういう具体的Relationを表現しているのよということの特定。(これが意味論?)
  
  
• で、この具体的に特定された(universe, relation assignments)の組のことを、modelと呼ぶ。
  
• 逆に、あるmodelに対応したstatementの集りのことを、language of a modelと呼ぶ。
  
• ここで「対応した」とは、そのmodelに適合した形(relationシンボルとrelationのarityがポイント)であるということ。
  
• で、ここ、ややこしいというか用語が混乱しているように思うのだが、
  
  
  
  • model Mがあるとする。
    
  • statement Φ が 、Mに対するlanguage of a modelに属しているとする。
    
  • すると、Φは、Mによって、trueとなったりfalseとなったりするでしょう。(ここまではよい。)
    
  • あるMでΦがtrueになったとする。
    
  • そのとき、MはΦの a modelであるという。(ここ、ちょっと混乱している)
    
  
  
• まあ、これが定義なのだからしかたなし。
  
  
• EXAMPLE 6.10 そうか、「∀x∀y(R1(x,y)∨R1(y,x)をモデル(N,<=)で考える」というのが言語とモデルの正式な関係で、これを「∀x∀y(x<=y)∨(y<=x)を考える」といってしまうのはこのモデルを念頭においた略記にすぎないのだな。
  
  
• で、Th(M): theory of M の定義
  
  
  
  • a model たる Mがあるとする。
    
  • すると、Mに対する複数のlanguage of a modelがあるだろう。
    
  • そのなかで、すべてのsentenceがtrueとなるものがあったとする。
    
  • それをtheory of Mと呼ぶ。
    
  
  

TMもずいぶん長くやっているし、「論理学をつくる」で一階述語論理まではかじっているので、すんなり。
とりあえず、ここまで。
次回は、これらについて判定可能性を調べていく。

意味論をぼやぼやと

プログラミング言語関係で、わかりにくい言葉に「意味論」がある。私はさっぱりわからない。Semanticsを意味論と訳していることも、誤訳じゃないかと疑っているくらいだ。(意味という言葉にひっぱられて、理解しずらくなっているんじゃないか、という責任転嫁)

Semantic Webとかもさっぱりわからない。単にメタデータがつくことがSemanticなの? とか。OWLでオントロジ書けばSemanticなの?とか。

先々、プログラミング言語のSemanticsもかじるとして、ぼやぼやと準備を初めようと思う。

まずは、計算機科学にくる前の「意味論」ってどんなものなんだろ、という興味にて、

「ルイス・キャロルの意味論」

を読もうと思う。

なんとか、深掘りせずに、お気楽にいきたい。。。

【シプサ】6 計算可能性の理論における先進的な話題

まずは 6.1 再帰定理。このあたり、λ算法との関連性が高いような感じがする。関数という単語がたくさんでてくるし。シプサが終わったらλ算法も少し勉強したい。CLを勉強していて、lambdaとか出てくるんだけど、λ算法をさっぱり知らない、というのはどうもいけない気がする。

将来λ算法をやるときの接続ポイントになるかも、と意識しつつも、あくまでTuring機械の観点で理解すればよしとする。深掘りすると抜けられなくなりそうで。

※予告：この回、文章がかなりぐだぐだです。

• 「自分自身を再生産する機械を作ることは可能である。」
  
  
  
  • これ、大事なので、原著もあたっておく。
    
  • 「Making machines that reproduce themselves is possible.」
    
  
  
• まず、入力には関知しないで、とにかく自分自身の記述(のコピー)を出力するTMを作ることを目標にする。それをSELFと呼ぶ。
  
• その準備として次の補題を確認する。
  
• 「補題6.1
  wを任意の文字列とすると、q(w)がwを出力して停止するTuring機械Pwの記述であるような計算可能な関数q:Σ*->Σ*が存在する。」
  
  
  
  • この章に入ってから、ほにゃららなTMが存在する、ということを、ほにゃららな計算可能な関数が存在する、とかの言い回しをすることが多い。
    
  • さて、まず計算可能な関数qがある、という。
    
  • ということは、その計算を実行できるTM Qがある、ということ。
    
  • qはΣ* -> Σ*。
    
  • 入力文字列は任意。wとする。
    
  • 出力文字列はとあるTMの表現。どんなTMかというと、入力文字列に関わらず、とにかくwをテープに書いちゃうようなTM。これをPwと呼ぶ。
    
  • そうするとQは2つの部分にわけるとよさそうだ。
    
    
    
    • Pwを構成する。
      
    • 前項で構成したPwから表現をつくる。その表現を<Pw>と表記する。
      
    
    
  • これは、できるのか??
    
    
    
    • 考える便宜のためにマルチテープTMとする。
      
    • まず、TM Qが動き出したとき、テープにはwが書かれている。それを読んでTM Qはwを知ることができる。
      
    • 一般にTMの仕様は{Q,Σ,Γ,δ,q0,qaccept,qreject}で特定できる。これを文字列で表現するのは決めの問題だけ。TMはとにかく表現可能。
      
    • Pwの仕様概要は、「入力文字列を消去して、wをテープに書いて受理」というだけ。
      
    • 入力文字列の消去は、TMでできる。
      
    • wを書くのはどうか?
      
    • wが"01"だとして、計算状態でいうと、q__ -> 0r_ -> 01s というように状態と遷移関数を組めばいいだろう。
      
    • よって、PwなるTMは存在する。
      
    • なので、できる。
      
    
    
    
  • 関数qってどんなものだろ、とイメージする。wが"01"だとしたとき、上のようにwを出力するTMの表現(<Pw>)がでてくるから、かなりけったいな文字列に写像する関数なのだろう。
    
  • TM Qってどんなものだろ、とイメージする。これはテープに例えば"01"と書かれて動作開始すると、それを消去して前項のかなりけったいな文字列をテープに書き出して受理状態として終了するようなものだろう。
    
  
  
  
• さて、TM SELFを構成する。
  
  
  
  • SELFは二つの部分から成るとする。それぞれをA,Bと呼ぶ。
    
  • 最初にAが動作して、終了すると制御をBにうつし、Bが動作することにする。
    
  • Aの仕事は、Bの記述を出力することとする。出力される表現を<B>と書く。
    
  • Bの仕事は、Aの記述を出力することとする。出力される表現を<A>と書く。
    
  • すると<A><B>と結合した文字列は、SELFを記述しきっているから、<SELF>と認定できる。
    
  • なので、こういうAとBを構成できれば、SELFは構成できたことになる。
    
    
  • AはPwをベースにする。
    
  • Aは<B>という文字列をとにかく出力するものなのだから、AはPwのwを<B>にしたP<B>であるとしてしまう。(それなら間違いなく<B>を出力する)
    
  • さて、上の関数qのイメージのところで"01"としたところを、<B>に読み替えてみる。
    
  • qによって、入力<B>に対して、<B>を出力するTMの表現がでてくる。
    
  • いいかえると、<A> = q(<B>) ということ。
    
  • ただし、P<B>を構成するには、上でみたように、<B>を(Aを構築する際にすでに)知らなければいけない。
    
    
  • では、Bはどうする。Bは具体的にTM的に構成して明示してあげなければいけない。
    
  • まず具体的に構成できたとして、その構成の表現を<B>とする。
    
  • そうするとそれはAの構成にビルドインされており、Aが動作すると<B>を出力する。
    
  • ところでq(<B>) = <A>なのだから、BはAのこの出力を受け取って、Q的に動けばよいことがわかる。
    
  • TM Bは次のとおり。
    B = 「入力<M>に対して、(MはTMの一部の表現)
    1. q(<M>)を計算する。
    2. その結果を<M>と結合してTMの完全な記述をつくる。
    3. その記述を印刷して停止する。」
    
  
  
• ミソは、やはりAとBの関係q(<B>) = <A>。
  
  
• さて、SELFが構成できた、ということはどういうことか。
  
• あるTM Mを表現するTM Sがあったとすると、TM SはTM Mのことをあらかじめしっていて、かつその構成の一部にTM Mを含んでいるので、TM SのほうがTM Mよりも複雑にならざるをえない、と思われる。
  
• たいていの場合はそうなのだが、SELFのように、「自分自身の構成のあり様」と「自分自身を表現する動作」ということが単体で充足している不思議な構造をもったTMも存在する、ということが言えたのだ。
  
  
• さて、ちょっと違う観点でみると、<SELF>をTMをシミュレートする万能TMのようなものに入力すると、<SELF>を出力する。
  
• これは、ここまで見てきたとおり、アプリオリではない。(print "I'm SELF")とかを考えてみれば、実感できる。
  
• では、万能TMにではなくて、人間に、同じような機能をもったプログラムというか指示というかその表現を与えるとしたらどんなものがあるだろう。
  
• それが、
  
  この文を書き写せ。
  
  であると。
  
• 「この」という自己参照を排除したバージョンは、
  
  次の文を二つ書き写して、二つめの文を鉤括弧で囲め。
  「次の文を二つ書き写して、二つめの文を鉤括弧で囲め。」
  
  ということ。
  
• SELFがわかったところで、再帰定理。
  
• 「再帰定理(Recursion Theorem)
  Tを、関数t:Σ*xΣ*->Σ*を計算するTMとする。このとき、すべてのwに対して、
  r(w) = t(<R>, w)
  となる関数r:Σ*->Σ*を計算するTM R が存在する。」
  
  
• 再帰定理の説明がわからない。ちょっとわからなさすぎる。日本語としてもわかりにくい。
  
• 原著を読む。
  
• う、この部分は翻訳より原著の方がはるかにわかりやすい。
  
• 自分なりにわかりやすく訳す。(再帰定理の説明のところ。P262)
  
• 「この定理は多少ややこしくみえるかもしれないが、実はとても簡単なことを言っているにすぎない。どういうことかというと、自分自身の表現をテープに書き出せたりそれを計算に利用できたりするようなTuring機械を構成するには、この定理にあるようなTuring機械 T を構成すればよい、ということだ。T は 入力文字列wに加えて、Turing機械の表現も入力として受け取るようにしておく。そんなTに対応して、入力文字列wに対する動作がTと同じであるTuring機械 R が存在しますよ、そしてそのときR自身の表現が(Tへの入力の一方として)内包されていますよ、というのが再帰定理が述べるところである。」
  
• このまま訳書で進めていくべきかどうか迷った。ここの説明、誤訳ではないが、私には理解できない日本語だ。。。
  
• せっかくここまで来たから訳書を完全にすてるのではなく、原書と両用していくことで対処することにする。
  
• 再帰定理の証明は簡単。
  
• 気になるのは、再帰定理が、T -> R という流れということ。一般的に利用したいのは、R -> T という事実なような気がする。
  
• t:Σ*xΣ* -> Σ*、 r:Σ* -> Σ*なので、再帰定理がなりたつなら、Rに対して、Tも存在しそう(構成できそう)なので、ここはスルーする。
  
  
• 再帰定理を認めてしまえば、残りの話は簡単だった。
  
  
  
  • 再帰定理を用いた、A[TM]の判定不可能性の証明。
    
  • 再帰定理を用いた、MIN[TM]の認識不可能性の証明。
    
  • 再帰定理を用いた、TMを変換するような計算可能な関数に対する不動点TMの存在証明
    
  
  
• こうしてみると、TMというのは、その仕様によって、
  
  
  
  • TMの表現を受け取ってそれをシミュレートできること。
    
  • 自身の表現を得ることができること。
    
  
  の2つが成立していて、これらがTMの特質として支配的であり、他の定理を導きやすいような気がする。
  

ああ、こつこつじゃなくて、ぐだぐだ。
次回は、「6.2 数理論理における判定可能性」。ここは「論理学をつくる」との接続ポイントになるかも、なので楽しみ。

【CL入門】6 関数

こつこつ。写経。

• 「ラムダ式はそれ自体はフォームではなく、したがって評価できない。」
  あれ、aclのREPLだと評価できる。。。
  

  
  CL-USER(14): (lambda (x) (* x x))
  #<Interpreted Function (unnamed) @ #x1000f1e752>
  

  
  
• defunは、ラムダ式を使って関数を定義する。その際にいくつか仕事をする。
  
  
  
  • 自動的にラムダ式のまわりにブロックを用意する。(スコープの管理がこれでつきているのか別の仕事なのかは、ちょっとわからない。)
    
  • そのブロックのタグは関数名として与えられたものである。
    
  • その関数名をシンボル管理テーブル(のようなもの)に加える。
    
  
  
• 写経なので深掘りしない。深掘りしない。。。
  
• といいつつ、なんとなくわかった。上のスコープ管理のこと。defunで定義された関数名は大域であり、かつ、レキスカルスコープなので、当該関数の呼び出し時にそのときのスコープではなく、記述時のスコープになるという、スコープの途絶えが発生するということだ。(※これは間違った理解であることが、下のクロージャのところでわかることになる)
  
• ここのfletやlabelsの説明は、「defunだとレキシカルスコープによってスコープの流れが変則的になること」に対して、fletやlabelsが自然なスコープの流れを維持するのに有効であるという論調。(※これも間違った理解であることが、下のクロージャのところでわかることになる)
  
• おお、(funcall 'cons ...)と(funcall #'cons ...)の違いは、それが参照する環境(のシンボル管理テーブル)の違いなのか。前者は常に大域をみて、後者は常にその時点での環境階層に従う、と。(※これも中途半端な理解というか、schemer的な解釈であることが、下のクロージャのところであきらかになる。)
  
• 次の例によって、#'fooが関数実体をあらわし、'fooが関数実体への参照であることがよくわかる。これはスコープの話とは基本的には別。
  

  
  CL-USER(83): (setq fdef #'foo fname 'foo)
  FOO
  CL-USER(84): (funcall fdef 10)
  11
  CL-USER(85): (funcall fname 10)
  11
  CL-USER(86): (defun foo (x) (1- x))
  FOO
  CL-USER(87): (funcall fdef 10)
  11
  CL-USER(88): (funcall fname 10)
  9
  

  
  
• なお、昔から疑問があって、MLはREPL上というかtop-levelもまごうことなきレキシカルスコープなんだけど、それとくらべると、Common Lispのレキスカルスコープは中途半端な気がするのです。これはいつかちゃんと調べないといけないと思っています。
  
  
• クロージャ。
  
• 以下、あたりまえだが、CLの話。
  
• evalはリスト・フォームをうけとるだけ。というのは、今自分がどこにいて(どういう状況にて)呼出されているのかという環境については何もしらない。その範囲でそのリスト・フォームを評価する、と。(例 (eval '(a b c)); evalはaを大域関数と解釈し、bとcを大域変数と解釈する。)
  
• funcallについても似たようなことがある。(funcall 'a)はaというシンボルを受け取るだけで、環境についてはしらず、funcallはそのaを大域関数と解釈して実行する。
  
• (funcall '(lambda (x) (* x x)) 3)についてはどうか。
  
• この場合まずシステムは'(lambda (x) (* x x))を単なるリスト・フォームと解釈する。そしてそのリストをfuncallに渡す。funcallは、「リスト・フォームを受け取った場合、リストの第一要素がlamdaだった場合、それがラムダ式であるとしてxを3にバインドした上で本体を評価するという機構」を持っているのだ。(ここSchemeと違うんじゃないか、というところ。)
  
• で、重要なのはこの場合もリスト・フォームしか渡してなくて、環境(情報)は渡していない、ということ。
  
• なので、
  

  
  (setq y 2)
  (let ((y 4))
    (funcall '(lambda (x) (* x y)) 3))
  ; -> 6
  

  
  などとすると、funcallは自分が呼出されているところでの環境(情報)を渡されていないので、答が6になる。
  
• では、
  

  
  (setq y 2)
  (let ((y 4))
    ((lambda (x) (* x y)) 3))
  ; -> 12
  

  
  はどうなのか、ということ。funcallのときは、システムはあくまでfuncallという関数呼び出しの面倒をみているだけであり、だからその関数に渡す引数を普通に(lambda式とかを特別扱いせずに)評価してあげた上で、funcallを呼出すだけだった。これは今までの説明のとおり。それとは違って、この例は、このリスト・フォームをシステムが評価するときにどういう動作をするのか?ということ。
  
• で、この場合は、 ((lambda (x) (* x y)) 3)はラムダ式ではじまるリスト・フォームなので、ラムダ式が定義する関数を生成して呼出す。この生成の際に、システムは局所変数yのスコープにいることを尊重して(知っている)ということがCLの仕様として決っている、ということ。
  
• ここでちょっと考える。CLではやはりlambda式はクロージャをつくらないのか、ということ。よりイメージを正確にいうと、lambda式の評価結果がクロージャではないのか、ということかな。(追記：いや、正確に言うとCLではラムダ・フォームというのは存在せず、そういう意味においての評価はされない(できない)ので、これは阿呆な言明である。)
  
• 上の議論は、クロージャをつくらない、ということだと思う。
  
• なので、ラムダ式というのは、頭がlambdaのリスト・フォームにすぎなくて、それを扱う側が特別視しないかぎり、単なるリストということかな。特別視されるのは、リスト・フォームの頭がラムダ式のときやfuncallの第一引数に与えられたときなど。
  
  
• で、クロージャをつくるのはfunctionだと。略記は"#'"。
  
• なので、先の例は、quoteじゃなくてfunctionにすれば、環境情報までfuncallにわたる
  

  
  (setq y 2)
  (let ((y 4))
    (funcall #'(lambda (x) (* x y)) 3))
  ; -> 12
  

  
  
• すなわち、スペシャル・オペレータたるfunctionは、それが呼出された場所の環境情報を集めて、それらをラムダ式に付加したデータを生成する(このデータ(やその型)をクロージャと呼ぶ)。(Functionにすぎないfuncallやapplyは環境をいじれないが、Special operatorであるfunctionは環境をいじれる。ややこしい。。。)
  
• funcallやapplyは、引数がクロージャであるなら、それが持つラムダ式と環境情報とを利用して処理を進める。
  
• クロージャは数値などと同じ意味でのデータなので、名前をつけて参照したり、いろいろ受け渡したりできる。(う、説明が面倒になってしまい。。。ファーストクラスということかと)
  
  
• この本、CLのクロージャの説明で、今までで一番わかりやすかったような。
  
• でも、他のものをいろいろ見た後で見ているからこの本のものが初見でわかりやすいかどうかはわからない。
  
  
• 思うところ。正確には表現できないのだが、たぶん、Schemeでは処理系の内部の環境モデルとクロージャというものと、言語の外部仕様というか形式としてのlambdaがもつ意味とが、よりダイレクトに対応しているのではないか。CLでは、言語の内部ではfunctionが無いフォームの処理においても環境モデルやクロージャを使っている(処理系依存というか処理系の作者の判断だが)としても、言語を使う側としてのクロージャというもの(処理系内部のクロージャと同一仕様というか同じものとは限らない)を利用する場合は明示的にfunctionというスペシャル・オペレータを使わなければいけない、ということじゃないかなぁ。(長い。。。)
  
• なお、ここらへんは、処理系内部に関する知識がない現状の私では、間違えている可能性もある。私はよく間違えるし。
  
• 早くコンパイラの勉強をして、自分でこれが正しいのか違うのか判断できるようになりたいなぁ。
  
• お、これやってみたらおもしろい。
  

  
  CL-USER(108): (lambda (x) (* x y))
  #<Interpreted Function (unnamed) @ #x1000b40dd2>
  
  CL-USER(109): '(lambda (x) (* x y))
  (LAMBDA (X) (* X Y))
  
  CL-USER(110): #'(lambda (x) (* x y))
  #<Interpreted Function (unnamed) @ #x1000b4d732>
  
  CL-USER(111): (let ((y 4))
                  #'(lambda (x) (* x y)))
  #<Interpreted Closure (unnamed) @ #x1000bb8aa2>
  

  
  上で説明したことや、top-levelの特殊性についてよくわかる。
  

写経だけのつもりが、、、
でも楽しめたので、いいや。

# ここに書いた説明は、Common Lisp 入門の内容そのまんまではなくて、私の理解で書いたところがそこそこあります。なので、間違いがあったとしてもそれはおそらく私が原因です。

【シプサ】5 帰着可能性 (その12)

こつこつ。演習5.8。

• ちょっと手を動かして考えたら、なんもかんもわかった。
  
• そもそもPCPのお題を理解していなかったのだ。
  
• PCPのお題は、ドミノのある意味クラスがあたえられて、それから任意個のオブジェクトとしてのドミノを使ってマッチがつくれますか、ということだったのだ。クラスは全部使わなくてもよいし、ひとつのクラスからたくさんオブジェクトを作ってもよい。どう誤解していたかというと、与えらているのがクラスではなく複製不能なオブジェクトであると思っていたのだ。
  
  
• まず、これでPCPの判定不可能性を理解しようとしたときにもやもやしてたことが解消した。
  
• 次に、演習5.3 のマッチを探す問題の意図がわかった。私のような阿呆がこのように誤解することに対するセーフティネットだったのだ。見事に突き破ってしまったが。。。
  
  
• で、演習5.8。PCPがわかってしまえば造作もない。
  
• Part 2.で追加するドミノに、それが左端だった場合のものを足せばいいのだ。
  
• すなわち、Part 2.の条件化において、ドミノ[qa/rb]を足せばよい。もしそれが本当に左端だった場合は、マッチにこのドミノを使えばよい。
  
  
• 演習5.6〜5.8の解答を見てみる。証明の記述において違いはあるが、まあ正解だった。
  
• ただ、5.8の解答に「右」という単語があるが、どう考えてもこれは全部「左」の誤植/誤訳だろう。
  
• 念のため原著を確認した。"leftmost"、"move left"だった。
  
  
• 演習5.3 再度
  
• マッチあり。{[aa/a], [aa/a], [b/a],[ab/abab]}でいける。
  

おお、これにて帰着可能性が終わった。
えらい時間がかかった。次の6章は、

• 先進的な話題への入口
  
• 第三巻を読むのに必須ではない。
  

とのことなので、内容次第で、楽しめるところは深掘りして、現在興味がないところは軽く流そうと思う。
ああ、シプサが進むと嬉しい。

【例解UNIX】低水準入出力 (その2)

こつこつ。今回は「3.10 位置決め：lseek」から。

• whence: どこから(from where, from what place)
  
• システムコール、便利だなぁ。ファイルが自動的に長くなっていってくれたり。やはりOSというのはfacilityであることを実感。やばい、OSの勉強をそろそろ初めないと。
  
  
• 電話帳プログラムで、いちいちmemset(rec, 0, sizeof(rec))というように領域の0初期化を実施しているんだけど、これ、宣言時に、char rec[RECLEN+1] = { 0 }とするだけでいいんじゃないかなぁ。
  
  
• 3.12まで完了。
  
• 電話帳プログラム2を演習ですんなり書けたのが嬉しかった。
  
• 3.13以降は5章でプロセスをやってからやるとよいということなので、素直に従う。
  

次回は、3章の章末問題。

【シプサ】5 帰着可能性 (その11)

昨日は漢字変換がおかしくなって難儀した。例えば、「癒着」とかも変換してくれなくて、だけど全部が全部変換してくれないわけではなくて、おかしな状態だった。AquaSKKが原因なのかなと、OSXを再起動したら、ましになった。でも、なんだかまだ変な感じ。辞書が壊れているのかな?
さて、こつこつ。

• 「5.6 <=m がすいい関係をみたすことを示せ」
  
  
  
  • ああ、すいいが変換できなくなっている。。。とりあえず、しゅうりは後まわしにして進む。ああ、しゅうり、が変換できない。なんだかアルジャーノンのように、使える漢字がじょじょに動的にげんしょうしているような気がする。
    
    
    
    • だめだ。SKKがまともにうごかないと、書きながら思考、というのができない。。。
      
    • 調べる。。。。
      
    • 判った。なんと主辞書ファイルが途中でぶったぎれてた。こんなこともあるんだな。
      
    • SKK-JISYO.Lをダウンロードしなおして、skkを再起動。直った。
      
    • これでキリアン先生に愛してもらえる。
      
    
    
  
  
  
  
  • 推移関係とは、「あらゆるx,y,zについて、xRyかつyRzならばxRz」ということであった。
    
  • 写像帰着の正式な定義は、
    「計算可能な関数f:Σ*->Σ*が、任意のwに対して、
    w∈A <=> f(w)∈B
    をみたす」
    であった。
    
  • いま、言語A,B,Cがあり、A <=m BかつB <= Cであるとする。
    
  • ここで計算可能な関数f,gがあり、任意のwに対して、
    w∈A <=> f(w)∈B かつ w∈B <=> g(w)∈C
    である。
    
  • すると
    w∈A <=> g(f(w))∈C
    である。
    
  • ここでg・fは計算可能である。なぜならgのTMとfのTMを連結すれば構成できるから。■
    
  
  
  
• 「5.7 AがTuring認識可能であり A <=m 「Aの補集合」ならば、Aが判定可能であることを示せ」
  
  
  
  • ある言語が、自分の補集合に写像帰着可能ってどういう感じなんだろ?
    
  • 写像帰着関係(の定義)は補集合演算に関して透過的だから、これは同時に、「Aの補集合」 <=m A でもある。
    
  • そうか、その写像によって、Aのものは必ずAの補集合に写されるし、逆もなりたつのだ。総入れ替え、みたいな状況なんだな。
    
    
  • さて、証明自体は簡単で、「Aの補集合」 <=m A から「Aの補集合」もTuring認識可能ということがわかる。自身と補集合が認識可能だから、Aは判定可能である。■
    
  
  
  
• 「5.8 定理 5.15の証明で、Turing機械を変形してヘッドが左端からはみ出さないようにした。この変形をMに対して行わなかったとする。このケースを扱うために、PCPの構成を変更せよ」
  
  
  
  • う、PCPのところ、ぐだぐだになっていたので、問題文が何を言っているのかすらわからない。
    
  • 気分転換に例解UNIXをやってからにしよう。
    
  
  

【CL入門】5 リスト構造

こつこつ。写経は楽し。

• そっか、(rplacd x x)で、循環リストがつくれる。
  
• 循環させるには名前が必要ということに何かありそうな。
  
• aclではリストが長い場合、REPLが表示というかリストの探索をきりあげてくれる。
  

  
  (WE WE WE WE WE WE WE WE WE WE ...)
  

  
  などと表示される。
  

C言語はハードウエアにべったり?

感じたことを書いておこうと思う。

• C言語はハードウエアべったり(ノイマン型べったり)だから速い、とか言われていた。
  
• 自分もそれを鵜呑みにして、そう信じていた。
  
  
• でも、パタヘネでコンピュータアーキテクチャを自分自身で確認しなおして、さらにC言語も自分自身で確認しなおすと、どうもべったりとは思えない。
  
• パイプラインだとか、記憶階層だとか、そういうような速度に影響を与える重要要素がアーキテクチャにはたくさんあるのだが、それはC言語の言語仕様には見えていない。
  
• というか、ものによっては、命令セット(機械語)にも見えていない。逆に、隠蔽した上で、うまく最適化するのがアーキテクチャの善し悪しになっている。IA32はマイクロアーキテクチャなのでそれが顕著だが、MIPSだってそうだ。
  
• なので、C言語はあくまでC言語たるモデルに基づいた高級言語にすぎないと思う。
  
• それが速い、というのは、おそらく、それが速いようにアーキテクチャが調整されて、コンパイラが作り込まれて、というある意味優遇されている環境によるのではないか。その意味での、癒着構造としてのべったりならわかる。C言語がアーキテクチャにべったりなんじゃなくて、アーキテクチャがC言語にべったり、ということ。同じようだが、違う。
  
• マルチコアとかの新しい状況は、本当にこのままC言語を偏重してアーキテクチャを進化させていくので大丈夫なのか、という時期に来ていると感じさせる。
  
  
• C言語を入門する際に、実はこの誤解が学習障害になっているのではないか、と思った。
  
• ハードウエアべったりというようにイメージしても、実際のハードウエアは違うからそこがずれている。
  
• 一番大きなずれは、変数名などをどのように管理しているかというシンボル管理の側面を、ハードウエアべったりということを意識して、メモリと箱モデルですましてしまい、シンボル管理を言語モデルというか仕様としてどのようにしているかを説明しないところではないか。自分は、C言語の前にCommon Lispをかじっていたので、そのあたりを適宜補って理解することができた。今でもC言語をたいして理解したとはいえないが、それがなかったら、もっとぐだぐだになってしまったと思う。
  
  
• C言語が速いというのは、上のような長年の優遇措置を除けば、静的型付けであることと、OSがC言語でかかれているのでシステムコールを他言語にくらべてもっともダイレクトにcallできること、というのが理由ではないか。
  
  
• というわけで、昔はハードウエアべったりだったのかもしれませんが、今は違うと思う。
  
  
• あ、小さな組み込み系とかで、アーキテクチャがシンプルなものは、今でもべったりというのはありそうですね。
  
  
• C言語が速い、というのは、ある意味事実だが、それが「言語仕様がノイマン型にべったり」だからというのは理由としても違うし、このべったりというのは単体の言明としても違うと思った。
  

【シプサ】5 帰着可能性 (その10)

そのn、のnが二桁になったのはこれがはじめてかも。
体調が再度悪化しているけど、なんとか、こつこつ。

• 「5.5 A[TM]はE[TM]に写像帰着可能でないことを示せ。すなわち、A[TM]をE[TM]に帰着する計算可能な関数が存在しないことを示せ。」
  
  
  
  
  • まずA[TM]とE[TM]について、わかっていることを整理。
    
    
    
    
    • A[TM]は、判定不可能、認識可能。
      
    • E[TM]は、判定不可能。認識可能性は不明。
      
    • E[TM]が判定不可能であることは、帰着を用いて、A[TM]の判定不可能性から導いた。
      
    
    
    
  • とりあえず、この3つめが関係ありそう。これを考えてみる。
    
    
    
    
    • 導くにあたって、E[TM]が判定可能であるとすると、A[TM]が判定可能であるTMを構成できてしまうということで、背理法を使った。
      
    • ということは、帰着としては、A[TM]をE[TM]に帰着させている、ということ。
      
    • するとこの演習がフォーカスしているのは、やはり「写像」帰着が不可能ということ。帰着はできる、と。
      
    • その帰着の様を確認してみる。
      
      
      
      
      • A[TM]を判定するTM Sを構成する。
        
      • E[TM]を判定するTM Rが存在すると仮定する。
        
      • TM Sの入力は、<M,w>である。
        
      • まず、TM M1を、TM Mとwをつかって構成する。
        
      • M1 = 「入力xに対して、x != wなら拒否。x = wならば、wに対してMを動作させ、Mが受理するなら、受理する。」
        
      • つぎに、TM Sを、RとM1を使って構成する。
        
      • S = 「入力<M,w>に対して、1. TM M1を構成して、2. Rを入力<M1>にて動作させ、3. Rが受理するなら拒否し、拒否するなら受理する」
        
      
      
      
    • これは確かに、A[TM]という問題をE[TM]という問題に帰着させている。
      
    • さて、まず、この帰着をA[TM]からE[TM]への写像帰着にできるかどうか。
      
    • ああ、それが、違いますよ、っていうのがP.248の説明だ。
      
    • A[TM]からE[TM]への写像帰着ではなく、A[TM]から「E[TM]への補集合」への写像帰着になっている、と。
      
    • なんで、補集合への写像帰着でいいんだっけ？
      
    • ああ、そうか、集合と補集合の境界を判定できるか、というのが言語の判定可能性であり、それは境界に関することだからだ。それを集合と補集合のどちらの観点から言及しているか、というだけだから。
      
      
    • ああ、だいぶ彼らのことがわかってきた。
      
      
    • すると、A[TM]から「E[TM]の補集合」へは写像帰着可能ということが事実としてわかった。
      
    • とすると、「E[TM]の補集合」が認識不可能だとすると、A[TM]も認識不可能となってしまう。
      
    • A[TM]は認識可能なので、これは矛盾。よって、「E[TM]の補集合」は認識可能である。
      
    • すると、E[TM]は判定不可能だから、E[TM]は認識不可能であることがわかる。
      
      
    • A[TM]からE[TM]への帰着写像が存在するとする。
      
    • すると、E[TM]が認識不可能であるから、A[TM]も認識不可能ということになる。
      
    • これはA[TM]が認識可能という事実に反する。ゆえに仮定が間違っている。■
      
      
    • 正解かな？ と答を見てみる。
      
    • 解答は、はるかに簡単かつスマートに証明しているが、捉えているポイントは同じだ。よかった。
      
    
    
    
  
  
  

早く体調を戻さねば。

【例解UNIX】低水準入出力

虚心坦懐、こつこつ。

• とりあえず、「3.9 標準入力、標準出力、標準エラー出力」まで終わった。
  
• 病みあがりなので、無理しない。
  

次回は、「3.10 位置決め：lseek」から。

【CL入門】4 記号とパッケージ

昨日よりもだいぶ調子がよい。昨日までは、正直、椅子に座っているだけでつらかった。今日は椅子に普通に座っていられる。

• in-packageがちょっと違うような。
  
• まず、引数はunquotedであるべき?
  
• それから該当packageが存在しないときに自動生成されるとあるが、defpackageが必要かと。
  
• とりあえず、(defpackage "TOKYO")などと補いながら写経をつづける。
  
• ACLのREPLでは、top-levelの":'頭はREPLコマンドになっている。そのため、REPLでキーワードシンボルを":"頭で入力できない。いいのか?
  

写経は終了。こつこつ。

【シプサ】5 帰着可能性 (その9)

うむ。吐き気がするがちょっとだけ考えてみる。正規言語と写像帰着の関係について。

• この関係を考えるときに、「正規言語の任意の部分集合は正規言語といえるのだろうか」ということが気になっている。
  
• これがいえるからといって、演習問題が解けるとは限らないのだが、なんだか気になる。
  
• で、ちょっと考えてみる。
  
• まず、有限集合である言語は、全て正規言語ではないか、ということ。
  
• これはその有限の文字列を全て分岐して試すようなNFAを構成できるので真。
  
• そうすると、部分集合が無限集合のときだけ考えればよいことになる。
  
• 無限集合である正規言語を考えるとき、その無限を生み出しているのは正規表現でいうとスター演算のみであることに気付く。
  
• Σ={0}, L = Σ* = {ε, 0, 00, 000, ...}として、0の個数が2^n個のものだけを取り出して言語をなしたとすると、それはどうも正規表現で書けそうにないので偽なのだろう。
  
  
• ちょっと演習問題まで考えてみる。
  
• たしか、「A <=m BでBが正規言語のときに、Aが正規言語といえるかどうか」ということだったはず。(問題を見返す元気もない。。。)
  
• ここで、w∈A <=> f(w)∈B だったはず。
  
• 上で見た例を適用するとどうなるか。
  
• L(B) = Σ*とする。
  
• L(A) = {w | wは0以外の文字を含まない文字列。ただし0の個数が2^nである。ここでnは自然数}とする。
  
• fは、「文字列に0以外を含むなら、入力文字に写像。文字列が0以外を含まず長さが2^nならBの該当要素に写像。これら以外なら、1に写像」とするとする。
  
• そうするとfは帰着写像になっている。
  
• これはBが正規言語だが、それへの帰着写像が存在するAは正規言語ではない。
  
• これで反例をしめせた。
  
  
• 本当か?
  
• 精査する余力がない。。。
  
• 次回、精査することにする。
  

こつこつ。

【CL入門】3 制御構造

久しぶりに体調をえらいくずした。先週末に体調が悪くなってきたところ、今週に入ってから職場の飲み会が続いたからだと思う。なんとか復活してきた。朦朧としながら写経を完了。次回は、「記号とパッケージ」。。。

【シプサ】5 帰着可能性 (その8)

こつこつ。

• 「5.2 EQ[CFG]が補Turing認識可能であることを示せ。」
  
  
  
  • いろいろ考えてみた。こういう風にいろいろ考えてみるのはとても訓練になると思う。
    
  • で、EQ[CFG]の補集合が認識可能であることは、認識可能なTMを構成することによってできると思えてきた。
    
  • 大筋を書く。
    
    
    
    • 入力は、<G,H>。
      
    • 入力が不適切なら受理。
      
    • 入力が適切ならば、それらと等価なPDAを構成。両PDAのアルファベットの和集合をΣとする。
      
    • Σ*を生成する装置を構成。
      
    • それをGとHで動作させる。文脈自由文法は判定可能だから、かならずそれぞれ受理か拒否になる。
      
    • GとHとで、受理or拒否が食い違ったなら、受理とする。
      
    • 同じなら、次の文字を試す。
      
    
    
  • これによって、EQ[CFG]の補集合について、判定は不可能だが、認識は可能である。■
    
  
  
  
• 5.3 Post対応問題の具体的な例
  
  
  
  • 上段と下段の文字列長の和が違うのでマッチは存在しない。
    
  • これ、何を意図した問題なのかな???
    
  
  
  
• 「5.4 A <=m BかつBが正規言語ならば、Aは正規言語となるか? その理由を述べよ。」
  
  
  
  • これ、結構考えたが、地味に難しい。。。
    
  
  

次回は、5.4の続きから。

【シプサ】5 帰着可能性 (その7)

今日から演習開始。

• 「5.1 EQ[CFG]が判定不可能であることを示せ」
  
  
  
  • 調査：A[CFG]とE[CFG]は判定可能。ALL[CFG]は判定不可能。計算履歴を用いた帰着で確認している。
    
  • 方針：EQ[CFG]とALL[CFG]との帰着にて示す。EQ[CFG]を判定可能であると仮定して、ALL[CFG]が判定可能になってしまうことを示す。
    
  • 証明：
    
    
    
    • ALL[CFG] = {<G> | GはCFGであり、L(G)=Σ*}
      
    • EQ[CFG] = {<G1,G2> | G1とC2はCFGであり、L(G1) = L(G2)}
      
    • そっか、Gを与えられたときそのPDAのΣに対して、Σ*を受理するCFG(or PDA)を構成できればいいんだ。
      
    • Σ自体は有限集合であり、正規言語。正規言語のクラスはスター演算に関して閉じているからΣ*も正規言語。
      
    • Σを生成するCFGは、一定の手順で構成できる。そのCFGからΣ*を認識するCFGも一定の手順で構成できる(演習2.16)。
      
      
    • さて、TMを記述してみる。
      
      
      
      • EQ[CFG]を判定するTM Mがあると仮定する。
        
      • TM Sを構成する。
        
      • Sの入力は<G>とする。
        
      • 動作を構成する。
        
        
        
        • <G>から等価なPDAを計算してΣを明確にする。(終端記号のピックアップで事足りるかも?)
          
        • Σを生成するCFGを構成し、それをもとにΣ*を構成するCFG G'を構成する。
          
        • Mに<G', G>を入力する。
          
        • Mが受理すれば受理し、拒否すれば拒否する。
          
        
        
      
      
    • これはALL[CFG]を判定するTMである。
      
    • ALL[CFG]は判定不可能だから矛盾が生じている。ゆえに仮定が間違っており、EQ[CFG]は判定不可能である。■
      
    
    
  
  
  
• 「5.2 EQ[CFG]が補Turing認識可能であることを示せ」
  
  
  
  • 調査：
    
    
    
    • 補Turing認識可能って何だっけ? 調べる。「Turing認識可能な言語の補集合」だ。
      
    • うお。そうすると、EQ[CFG]の補集合はTuring認識可能、ということか。ちなみにそうすると、EQ[CFG]はTuring認識可能ですらないんだ。。。
      
    • 系5.29によると「A <=m Bのとき、AがTuring認識不可能ならBもTuring認識不可能」である。写像帰着の定義によると「A <=m B ならば、Aの補集合 <=m Bの補集合」なので、「Aの補集合 <=m Bの補集合のとき、Aの補集合がTuring認識不可能ならBの補集合もTuring認識不可能」となる。ここで、AをA[TM]、BをEQ[CFG]とすると、「A[TM]の補集合 <=m EQ[CFG]の補集合のとき、A[TM]の補集合がTuring認識不可能ならEQ[CFG]の補集合もTuring認識不可能」となる。あれ? これじゃだめじゃん。
      
    • 単純に、 EQ[CFG]の補集合 <=m A[TM] を示せばいいんだ。EQ[CFG] <=m A[TM]の補集合 という手もある。どちらにするか。 前者の方が簡単そうだ。
      
    
    
  • 方針：EQ[CFG]の補集合 <=m A[TM] を示す。
    
  • 証明：
    
    
    
    • EQ[CFG]の補集合の受理入力：<G1,G2> G1とG2は受理する言語が違う。
      
    • A[TM]の受理入力：<M,w>で、TM M は 入力wを受理する。
      
    • む、wの扱いが難しい。
      
    • あと、CFGとTM、というように言語クラスが違うところをどうするか。。。
      
      
    • EQ[CFG]が認識不可能であることは示せそうなんだけど。これだと逆にできる。やってみる。
      
    • すなわち、A[TM]の補集合 <=m EQ[CFG] を示せばよい。
      
      
    • A[TM]の補集合の受理入力：<M,w&tで、TM M は 入力wを受理しない。
      
    • EQ[CFG]の受理入力：<G1,G2> G1とG2は受理する言語が同じ。
      
    • M,wからG1,G2を構成できるか?
      
    • 二つのPDA D1とD2を構成する。
      
    • D1は全ての入力を拒否する。
      
    • D2は全ての入力に対して、wでMを動作させる。拒否したら拒否、受理したら受理する。
      
    • <D1,D2>を出力。
      
    • 帰着関数ができた。
      
      
    • よって、EQ[CFG]は認識不可能。帰着関係は、A[TM]の補集合 <=m EQ[CFG]。
      
    • あ、この帰着関係は使える? 補集合は、A[TM] <=m EQ[CFG]の補集合。だめだやはり使えない。
      
    • 。。。
      
    
    
  
  

ダメダメ。一旦頭を冷やす。

【例解UNIX】Cの復習(2)：ポインタ、バイトオーダ、複雑な型 (その4)

こつこつ。2.8 章末問題

• 1 (5分くらい)
  
  
  
  • 特になし。
    
  
  
• 2 (20分くらい)
  
  
  
  • 問題文を理解していなくて、単にm * nの領域をとって2次元配列的に使う実装をしてしまった。そこから修正。
    
  
  
• 3 (180分くらい)
  
  
  
  • うお。OSXにもUbuntuにも、デフォルトではlibmudflapが入ってない。
    
    
  • Ubuntuにはパッケージがあるようだ。Ubuntuにする。いれる。 sudo aptitude install libmudflap0。
    
    
  • ぬお。Ubuntu上でleak.cをコンパイルしようとするとstdlib.hが無いと言われる。locateしてみるとたしかに無い? stdlib.hってそういうものなんだ。man mallocでヘッダを確認。あり? stdlib.hじゃん。なんで無いの? man stdlib.h しても有益な情報はなし。
    
  • find / -name "*.h" してみると、Ubuntuにはデフォルトで開発用ヘッダが入っていないような、という感じ。
    

    
    /usr/lib/gcc/i486-linux-gnu/4.2/include/decfloat.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/unwind.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/limits.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/linux/a.out.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/pmmintrin.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/emmintrin.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/mm3dnow.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/asm/posix_types.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/varargs.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/iso646.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/mmintrin.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/stdbool.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/float.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/omp.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/mm_malloc.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/xmmintrin.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/stdarg.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/syslimits.h
    /usr/lib/gcc/i486-linux-gnu/4.2/include/stddef.h
    

    
    
    
  • aptitude search gcc。この結果から、gcc-multilibとかにいるのかなと思って、パッケージ落として中身をみてみた(dpkg-deb --contents )が、いない。
    
    
  • Ubuntuのサイトでパッケージの中身検索をしようと思ったが、どこでできるのかわからない。
    
  • しょうがないのでdebian.orgで検索。
    
  • 検索結果から、そもそもlibc関係のファイルが足りてないのか、と推察。
    
  • apptitude search libc6。libc6-devのステイタスが"pi"だ。なんじゃこりゃ? man apptitude。「存在していないけど、インストール予定」とな。誰が予定したか、わけわからん。しかしこれだろう。
    
  • sudo apptitude install libc6-dev。libc6-devとlinux-libc-devが入った。
    
  • を、/usr/includeにわんさかできた。
    
  • stdlib.hが無いとは言われなくなった。
    
    
  • "cc1: error: mf-runtime.h: No such file or directory"とおっしゃる。(gcc)
    
  • たしかにfindしてもいない。
    
  • ああ、Ubuntu(debian)では、開発者はdevをいれねばならんのか。
    
  • sudo aptitude -s install libmudflap0-dev。おお、これはgcc-4.1用なのね。
    
  • sudo aptitude -s install libmudflap0-4.2-dev。ok。
    
  • sudo aptitude install libmudflap0-4.2-dev。ok。findすると、いるいる。
    
    
  • ヘッダが無い、とはいわれなくなったが、__mf*的なメッセージがごちゃごちゃでてコンパイルが失敗する。
    
  • これは、leak.cでもそうだし、他のソース(メモリ操作を含まない)でもそうだった。単純にライブラリの場所をしらんのかな。
    
  • gcc -Wall -g leaks -fmudflap -lmudflap。ok。
    
  • MUDFLAP_OPTIONS="-help" ./a.out。ok。次のヘルプがでる。
    

    
    This is a single-threaded thread-unaware GCC "mudflap" memory-checked binary.
    Mudflap is Copyright (C) 2002-2004 Free Software Foundation, Inc.
    
    The mudflap code can be controlled by an environment variable:
    
    $ export MUDFLAP_OPTIONS=''
    $ 
    
    where  is a space-separated list of 
    any of the following options.  Use `-no-OPTION' to disable options.
    
    -mode-nop                mudflaps do nothing
    -mode-populate           mudflaps populate object tree
    -mode-check              mudflaps check for memory violations [active]
    -mode-violate            mudflaps always cause violations (diagnostic)
    -viol-nop                violations do not change program execution [active]
    -viol-abort              violations cause a call to abort()
    -viol-segv               violations are promoted to SIGSEGV signals
    -viol-gdb                violations fork a gdb process attached to current program
    -trace-calls             trace calls to mudflap runtime library
    -verbose-trace           trace internal events within mudflap runtime library
    -collect-stats           collect statistics on mudflap's operation
    -sigusr1-report          print report upon SIGUSR1
    -internal-checking       perform more expensive internal checking
    -print-leaks             print any memory leaks at program shutdown
    -check-initialization    detect uninitialized object reads
    -verbose-violations      print verbose messages when memory violations occur [active]
    -abbreviate              abbreviate repetitive listings [active]
    -timestamps              track object lifetime timestamps [active]
    -ignore-reads            ignore read accesses - assume okay
    -wipe-stack              wipe stack objects at unwind
    -wipe-heap               wipe heap objects at free
    -heur-proc-map           support /proc/self/map heuristics
    -heur-stack-bound        enable a simple upper stack bound heuristic
    -heur-start-end          support _start.._end heuristics
    -heur-stdlib             register standard library data (argv, errno, stdin, ...) [active]
    -free-queue-length=N     queue N deferred free() calls before performing them [4]
    -persistent-count=N      keep a history of N unregistered regions [100]
    -crumple-zone=N          surround allocations with crumple zones of N bytes [32]
    -lc-adapt=N              adapt mask/shift parameters after N cache misses [1000003]
    -backtrace=N             keep an N-level stack trace of each call context [4]
    

    
    
  • しかし、leak.cは何もいってくれない。
    
  • dangling.cはいってくれる。
    

    
    *******
    mudflap violation 1 (check/write): time=1220683685.027955 ptr=0x80cac98 size=4
    pc=0xb7efb7bd location=`dangling.c:9 (main)'
          /usr/lib/libmudflap.so.0(__mf_check+0x3d) [0xb7efb7bd]
          ./a.out(main+0x9a) [0x80487be]
          /usr/lib/libmudflap.so.0(__wrap_main+0x49) [0xb7efb259]
    Nearby object 1: checked region begins 4729B after and ends 4732B after
    mudflap object 0x80ca028: name=`__mf_lookup_cache'
    bounds=[0x8049a20,0x80c9a1f] size=524288 area=no-access check=0r/0w liveness=0
    alloc time=1220683685.024966 pc=0xb7efb1fd
    Nearby object 2: checked region begins 0B into and ends 3B into
    mudflap dead object 0x80cace0: name=`malloc region'
    bounds=[0x80cac98,0x80cac9b] size=4 area=heap check=0r/0w liveness=0
    alloc time=1220683685.025568 pc=0xb7efb1fd
          /usr/lib/libmudflap.so.0(__mf_register+0x3d) [0xb7efb1fd]
          /usr/lib/libmudflap.so.0(__wrap_malloc+0xde) [0xb7efc72e]
          ./a.out(main+0x2c) [0x8048750]
          /usr/lib/libmudflap.so.0(__wrap_main+0x49) [0xb7efb259]
    dealloc time=1220683685.027660 pc=0xb7efb1a6
          /usr/lib/libmudflap.so.0(__mf_unregister+0x36) [0xb7efb1a6]
          /usr/lib/libmudflap.so.0(__real_free+0x88) [0xb7efbff8]
          ./a.out(main+0x3a) [0x804875e]
          /usr/lib/libmudflap.so.0(__wrap_main+0x49) [0xb7efb259]
    number of nearby objects: 2
    

    
    
  • overrun.cもいってくれるな。
    
  • うむ。3時間もつかってしまった。でも勉強になった。
    
  
  
• 4
  
  
  
  • これは三つ星なので、パス！
    
  
  

Cの復習はこれでおわり。
次回は、ついに本論開始。「低水準入出力」

【CL入門】2 基本構造

Lispは楽し。

• (set '...)と(setq ...)の違いをしらなかった。setは常に大域のシンボル対象で、setqはスコープのシンボル対象なのね。
  
• とにかく写経。
  

次回は制御構造。

【シプサ】5 帰着可能性 (その6)

こつこつ。今回は写像帰着可能性。

• 帰着させるという概念の細かな定義は、いくつかの流儀がある。
  
• ここでは写像帰着可能性というのをやる。
  
• おおざっぱにいうと、
  「写像帰着可能性を用いて問題Aを問題Bに帰着できるとは、問題Aへの入力例を問題Bへの入力例に変換する計算可能な関数が存在するということである」
  
  
  
  • なんとなく、わかるけど、ちょっと考えてみる。
    
  • 計算可能な関数が存在する、というのはTMで実施可能、ということ。
    
  • なので、問題Aへの入力例を問題Bへの入力例に変換できるTM hogeを構成できる、ということ。
    
  • 問題Aというのは、言語Aを判定できるかどうかということだとする。Bもしかり。
    
  • それは言語Aを判定するTM piyoを構成できるか、ということ。Bについては、そんなTM poyoを構成できるか、ということ。
    
  • TM hogeとTM poyoが存在するなら、この言明が成立するときは、TM piyoをTM hogeとTM poyoで構成できる。
    
  • よって、問題Bが解けるなら、問題Aも解けることになる。逆に問題Aが解けたって、問題Bが解けるとはいえない。
    
  • すなわち、問題Aより問題Bの方が難しいといえる。
    
  • 理解した。
    
  
  
  
• ついに「計算可能な関数」が出てきた。
  
• ここらへんがラムダ算法との接点なのかな?? ラムダ算法も学習したいなぁ。
  
• 余談だが、この章、ちょこちょこ誤植(誤訳?)があるな。
  
  
• こっから、結構タフな作業。この章のここまでの帰着に関する具体的な議論を、写像帰着性を用いて捉えなおす。こういう作業はタフ。だからこそ力になると考えて、進む。
  
• 定理5.1 HALT[TM]が判定不可能であること。
  
  
  
  • もともとの証明は?
    
    
    
    • TM R がHALT[TM]を判定すると仮定する。そして、A[TM]を判定する TM S を構成してみせた。ところで、A[TM]が判定不可能なのは直接確認済みなので、矛盾が生じている。ゆえにTM Rに関する仮定が間違っている。
      
    • さて、ここで「構成する」ところの詳細は?
      
    • TM Rの入力は、<M,w>であり、wに対してMが停止するなら受理し、しないなら拒否する。
      
    • TM Sの入力は、<M',w'>であり、wに対してM'が受理するなら樹脂し、しないなら拒否する。
      
    • Sの動作：Sは、<M', w'> を受け取る。それをRに入力する(SはRをシミュレートできる)。Rが拒否するなら拒否する。受理するなら、w'をM'に入力する(SはM'をシミュレートできる)。これは必ず停止するので、結果は受理または拒否である。それぞれ受理または拒否する。
      
    
    
  • これはわかる。これのどこが写像帰着なのか?
    
  • もしかしてこれは写像帰着ではないのか?
    
  • ああ、単純には写像帰着ではないようだ。入力の変換について明示していないから。
    
    
  • A[TM]からHALT[TM]への写像帰着を与える帰着(関数)f
    
    
    
    • 入力：<M,w>。
      
    • 出力：<M',w>。ただし「<M',w>∈HALT[TM]のとき、かつそのときに限り、<M,w>属するA[TM]」である。
      
    
    
  • fによって、A[TM] <=m HALT[TM]となる。
    
  • 判定可能な文字列を判定可能な文字列に変換する作業なことを、あらためて認識。
    
  • その変換する作業というか、そのための機構のなかに2つの言語の関係性が表われている。
    
  
  
  
• 定理 5.15 Postの対応問題
  
  
  
  • これはまさに写像帰着にて解いている
    
  
  
  
• 定理 5.4 E[TM]からEQ[TM]への帰着
  
  
  
  • う、この証明がどんなんだったかおもいだせない。
    
  • 見直してみる。
    
    
    
    • TM R はEQ[TM]を判定すると仮定する。E[TM]を判定するTM S を構成する。
      
    • TM S の構成。
      
      
      
      • TM S の入力を<M>とする。
        
      • M1をすべての入力を拒否するTMとする。
        
      • Rに、<M, M1>を入力する。
        
      • ああ、簡単じゃないか。
        
      
      
    • 私は、「E[TM]からEQ[TM]への帰着」が何をいっているかの方がわかっていないのだ。それがわかった上で、それの解法がわからないのではなくて。
      
    • 考える。
      
      
      
      • E[TM]からEQ[TM]への帰着。
        
        
      • まず問題の帰着として考える。
        
      • 問題E[TM]から問題EQ[TM]への帰着。
        
      • これは、ざっくり言って、問題E[TM]を解くことを、問題EQ[TM]を解くことにすりかえられるということ。
        
      • ということは、E[TM]はEQ[TM]より(ざっくりいうと)簡単である。
        
      • よって、EQ[TM]が判定可能なら、E[TM]も判定可能。
        
      • よって、E[TM]が判定不可能なら、EQ[TM]も判定不可能。
        
      • とするとE[TM]が判定不可能なことはここではアプリオリなので、EQ[TM]に帰着できれば、EQ[TM]も判定不可能である。
        
      • E[TM]を解くことを、EQ[TM]を解くことにすりかえられるか?
        
      • ああ、カリー化みたいな感じだ。E[TM](M) = EQ[TM](M1,M) (ただしM1はE[TM]なTM)
        
        
      • 次に言語の帰着として考える。
        
      • 言語E[TM]から言語EQ[TM]への帰着。
        
      • f : <M> -> <M1, M>
        
        
      • 多少、わかった気になれた。
        
      
      
    
    
  
  
• 定理 5.2 E[TM]は判定不可能である。
  
• これの証明もぼやっとしか覚えてない。
  
• 考える。
  
  
  
  • 判定不可能をしめしたいのだから、判定不可能だとわかっているものからE[TM]に帰着させる。
    
  • そこで、問題A[TM]から問題E[TM]に帰着させる。
    
  • これは、問題A[TM]を解くことを問題E[TM]を解くことにすりかえるということ。
    
  • そのためには、A[TM]を解くTM S を E[TM]を使って構成できればよい。
    
  • A[TM]への入力を<M,w>とする。
    
  • A[TM]の受理or拒否が、E[TM]の受理or拒否と一対一対応されていればよい。
    
  • で、E[TM]は空性検査、であると。
    
  • <M,w>にしたがって、<M'>をつくってそれを空性検査にかけるんだろうな。
    
  • で、M'が認識可能な言語は空か非空なのだが、それがA[TM]の受理or拒否に対応している、と。
    
  • なんとなく、受理->非空 (L(M') = {w})、 拒否->空、と算段する。
    
  • M'をつくる。材料は、とあるTM Mと、とある入力 w。そしてE[TM]なTM Rをどうつかうか。
    
    
    
    • M'の入力をw'とする。
      
    • w' != w なら拒否する。
      
    • w' = wならMをwで動作させる。Mが受理するなら、受理する。(ループと拒否は考えない)
      
    
    
  • <M'>でRを動作させればOK。
    
  • 少し、わかった気になった。
    
  
  
• えっとこの証明では、<M,w>から<M'>に写像した。
  
• ここで、
  (Rが<M'>を拒否 = M'の認識する言語が非空) -> (<M,w>を受理)
  (Rが<M'>を受理 = M'の認識する言語が空) -> (<M,w>を拒否)
  である。
  
• なので先の写像は、E[TM]への写像ではなく、E[TM]の補集合への写像である。
  

最後はぐだぐだになったが、帰着可能性をなんとか読んだ。次は演習。
今日はシプサでいっぱいいっぱい。
こつこつ。

【CL入門】1 基本構造

えっと、学習のスタックが深くて、Common Lispから離れている期間が長くなってきた。そろそろ本格的にまずい。慣れだけでもやっておこうと思う。そこで、

Common Lisp 入門

をちょっとずつ読みはじめる。

1章から。

• まずは、M-x fi:common-lisp
  
• ああ、やっぱりLispは楽しい。
  
• REPLをいじるとき、学習開始前とはまた違う感覚がある。
  
• 20分くらいで一章終了。
  

次回は「2 関数の定義」。

【シプサ】5 帰着可能性 (その5)

こつこつ。今日はPCP Post corespondence problem。これも字面をおっているだけではさっぱりわからない。メモをとりながら。

• PCPを定義する。
  
• PCP = {<P> | PはマッチをもつPost対応問題の入力例}
  
  
• 証明したいこと。
  
• PCPは判定不可能である。
  
  
• 証明の方針。
  
• 受理計算履歴を介したA[TM]からの帰着。
  
• 任意のTM Mと入力 w を用いて、マッチがMのwに対する受理計算履歴となるように、入力例Pを構成する。
  
• マッチがMとwに対する受理計算履歴となるようなP、というのが何を言っているのかわからないが、先に進む。
  
  
• 技術的な事前手当を3つ。これは今は理解できなくてもよいとのこと。
  
  
  
  • Mの変更。Mにはヘッドをテープの左端からはみ出させる動作はないようにする。
    
  • w = ε の場合、wの場所を空白文字にする。
    
  • マッチが最初のドミノ[t1/b1]から開始するように、PCPの定義を変更する。これをMPCPと呼ぶ。
    MPCP = {<P> | P は最初のドミノから始まる PCP ドミノの集り }
    
  
  
  
• 証明。
  
  
  
  • TM R がPCPを判定するとして、A[TM]を判定するSを、Rを使って構成する。構成できてしまったら、帰着により、Rは判定不可能と言える。
    
  • Sが入力対象とするMを定義する。
    M = (Q,Σ,Γ,δ,q[0],q[accept], q[reject])
    
  • Mがwを受理するとき、かつそのときに限り、SはマッチをもつようなPCPのドミノの集合Pを構成する。
    
  • 集合 Pの構成。
    
  • まず、MPCPの入力例 P' を構成する。
    
    
    
    
    • Part 1. 構成の開始方法。
      [#/#q0w1w2...wn#]
      を最初のドミノ[t1/b1]としてP'に加える。
      
    • ここで、q0w1w2...wnは受理計算状態履歴の開始状態C1である。
      
    • これはマッチしていない。上段をなんとかしないといけない。
      
    • そのために、ドミノを追加する。
      
      
    • Part 2.
      
    • 任意のa,b∈Γと任意のq,r∈Q、ただしq != qrejectにたいして、
      δ(q, a) = (r, b, R) ならば、[qa/br]をP'に加える。
      
      
    • Part 3.
      
    • 任意のa,b,c∈Γと任意のq,r∈Q、ただしq != qrejectにたいして、
      δ(q, a) = (r, b, L) ならば、[cqa/rbr]をP'に加える。
      
      
    • Part 4.
      
    • 任意のa∈Γに対して、
      [a/a] をP'に加える。
      
      
    • Part 5.
      [#/#]と[#/_#]をP'に追加する。( _ は空白文字)
      
      
      
    • Part 6.
      [a qaccept/qaccept] と [qaccept a/qaccept]をP'に追加する。
      
      
    • Part 7.
      [qaccept##/#]を追加して、マッチを完成させる。
      
      
    
    
  • ちょっとやってみる。
    

    
    step 1: part 1
    [ # / # q0 0 1 0 0 # ] 
    
    step 2: part 2
    δ(q0, 0) = (q7, 2, R)とする。
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    
    結合して上下比較
    # q0 0
    # q0 0 1 0 0 #  2 q7
    
    step 3: part 4
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    
    結合して上下比較
    # q0 0 1 0 0
    # q0 0 1 0 0 # 2 q7 1 0 0
    
    step 4: part 5
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    [ # / # ], [ # / _ # ]
    
    結合して上下比較
    # q0 0 1 0 0 # #
    # q0 0 1 0 0 # 2 q7 1 0 0 # _ #
    
    step 5: part 2
    δ(q7, 1) = (q5, 0, R)とする。
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    [ # / # ], [ # / _ # ]
    [ q7 1 / 0 q5]
    
    結合して上下比較
    # q0 0 1 0 0 # q7 1 #
    # q0 0 1 0 0 # 2 q7 1 0 0 # 0 q5 _ #
    
    step 6: part 4
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    [ # / # ], [ # / _ # ]
    [ q7 1 / 0 q5]
    [ 2 / 2 ], [ 0 / 0 ], [ 0 / 0]
    
    結合して上下比較
    # q0 0 1 0 0 # 2 q7 1 0 0 #
    # q0 0 1 0 0 # 2 q7 1 0 0 # 2 0 q5 0 0 _ #
    
    step 7: part 5
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    [ # / # ], [ # / _ # ]
    [ q7 1 / 0 q5]
    [ 2 / 2 ], [ 0 / 0 ], [ 0 / 0]
    [ # / # ], [ # / _ # ]
    
    結合して上下比較
    # q0 0 1 0 0 # 2 q7 1 0 0 # # #
    # q0 0 1 0 0 # 2 q7 1 0 0 # 2 0 q5 0 0 _ # # _ #
    
    
    step 8: part 3
    δ(q5, 0) = (q9, 2, L)とする。
    [ # / # q0 0 1 0 0 # ] 
    [ q0 0 / 2 q7]
    [ 1 / 1 ], [ 0 / 0 ], [ 0 / 0 ]
    [ # / # ], [ # / _ # ]
    [ q7 1 / 0 q5]
    [ 2 / 2 ], [ 0 / 0 ], [ 0 / 0]
    [ # / # ], [ # / _ # ]
    [ 0 q5 0 / q9 0 2 ], [ 1 q5 0 / q9 1 2 ], [ 2 q5 0 / q9 2 2 ], [ _ q5 0 / q9 _ 2 ]
    
    
    結合して上下比較
    # q0 0 1 0 0 # 2 q7 1 0 0 # 0 q5 0# #
    # q0 0 1 0 0 # 2 q7 1 0 0 # 2 0 q5 0 0 # q9 0 2 _ # _ #
    
    保留：[ 1 q5 0 / q9 1 2 ], [ 2 q5 0 / q9 2 2 ], [ _ q5 0 / q9 _ 2 ]
    

    
    感じはつかめた。
    
  
  

こちらも最後ぐだぐだになったが、なんとなくわかった。
後日振りかえるとして先に進もう。次回は写像帰着性。

【例解UNIX】Cの復習(2)：ポインタ、バイトオーダ、複雑な型 (その3)

こつこつ。可変長引数

• tiny_printfが自分でさくさく書けたのが嬉しい。
  

さあ、次回は二章の章末問題。

【例解UNIX】Cの復習(2)：ポインタ、バイトオーダ、複雑な型 (その2)

こつこつ。バイトオーダから。

• リトルエンディアン：x86, MIPS
  
• ビッグエンディアン：SPARC, MIPS
  
• 「改行と文字コードの問題を除けば、テキストデータはとても移植性の高いデータ表現です」
  
  
• 続いてtypedef。
  
• Cには4つのタグ名がある。
  
  
  
  • goto文のラベル名
    
  • タグ名 (構造体、共用体、enum)
    
  • メンバ名
    
  • その他(変数名、関数名、型定義名)
    
  • 列挙定数名
    
  
  
• う、5つに見えるのだが。
  
• typedefの例。
  
  
  
  • typedef struct list list
    
  • listがstruct list。これは違和感なし。
    
  • typedef int Array[10]
    
  • Arrayがint [10]。違和感あり。
    
  • typedef int (*Func)(int)
    
  • Funcがint (*) (int)。違和感おおきい。
    
  
  
• Array hogeがint hoge[10]ということだから、関数型マクロみたいなものと思っておくか。
  
• 
  
  
• そうか、システムデータ型の確認にはgdbが便利だ。
  
  
• うぉー、Cの型宣言、難しすぎ。
  
• int (*(*foo[])())[];
  
• int の配列へのポインタを返す関数へのポインタの配列。(笑った)
  
  
  
  • 
    

    
    int (*(*foo[])())[];
    
    分解しながら。
    
    int hoge; hogeはint。
    int hoge[]; hogeはintの配列。
    int (hoge)[];
    int (*hoge)[]; hogeはintの配列のポインタ。
    int (*hoge())[]; hogeはintの配列のポインタを返す関数。
    int (*(*hoge)())[]; hogeはintの配列のポインタを返す関数のポインタ。
    int (*(*hoge[])())[]; hogeはintの配列のポインタを返す関数のポインタの配列。
    

    
    
  • おお。一応読めた。
    
  • signalのプロトタイプを読む。
    

    
    void (*signal (int sig, void (*handler)(int)))(int);
    
    最左の識別子のみが重要。ここから考える。
    void ( *signal (int sig, void (*handler) (int) ) ) (int);
    
    *signal()を間違えないように *(signal())とする。
    void ( *(signal (int sig, void (*handler) (int) ) ) ) (int);
    
    読む。
    void hoge; hogeはvoid。
    void hoge (int); hogeはvoidを返す関数(引数はint)。
    void (*hoge) (int); hogeはvoidを返す関数(引数はint)へのポインタ。
    void (*(hoge (piyo)) (int); hogeはvoidを返す関数(引数はint)へのポインタを返す関数(引数piyo)。
    void (*(hoge (int sig, void (*handler)(int))) (int); hogeはvoidを返す関数(引数はint)へのポインタを返す関数(引数は、intと、voidを返す関数(引数int)へのポインタ)。
    こんな感じじゃろう。
    

    
    
  
  
• 演習問題2.13
  
  
  
  • int *x1(); intへのポインタを返す関数。
    
  • int (*x2)(); intを返す関数へのポインタ。
    
  • int *(x3()); intへのポインタを返す関数。
    
  • int (*x4()); intへのポインタを返す関数。
    
  
  
• お、読めた。
  
• 関数の型もgdbのptypeでわかるのね。それぞれ、
  
  
  
  • int *()
    
  • Int (*)()
    
  
  
• 演習問題2.14
  
  
  
  • int *x5[]; intへのポインタの配列
    
  • int (*x6)[]; intの配列へのポインタ
    
  • int *(x7[]); intへのポインタの配列
    
  • int (*x8[]); intへのポインタの配列
    
  
  
• gdb.
  
  
  
  • int *[1]
    
  • int (*)[0]
    
  
  
• う、1とか0がなぜいるのかわからない。
  

最後、ぐだぐだになったが、ビット演算まで終わった。
次回は可変長引数から。

【シプサ】5 帰着可能性 (その4)

こつこつ。

• ALL[CFG] = {<G> | GはCFGであり、L(G) = Σ*}
  
• 「ALL[CFG]は判定不可能である」
  
  
  
  • 方針：ALL[CFG]が判定可能と仮定し、その仮定を用いてA[TM]が判定可能であることを示す。
    
  • 方針：証明は計算履歴を介したA[TM]からの帰着である。
    
  
  
• 自分なりに組み立ててみる。
  
  
  
  • TM M と入力 w について、CFG G を構成する。
    
  • GはMがwを受理しないとき、全ての文字列を生成する。
    
  • GはMがwを受理するとき、Gはひとつの文字列を生成しない。それは、Mのwに対する受理計算履歴である。
    
    
  • さて、CFG GのかわりにPDA Dを構成することにする。
    
  • Dは非決定的な分岐をもつ。分岐は次のとおり。
    
    
    
    • 計算状態の列として所定の形式をみたしているか? 満足しないなら受理。
      
    • 先頭の計算状態が開始状態であるか? 開始状態でないなら受理。
      
    • 末端の計算状態が受理状態であるか? 受理状態でないなら受理。
      
    • CiからCi+1が遷移関数による関係になっているか? なっていないなら受理。
      
    
    
  • こうすると、Dは受理計算履歴以外のすべての文字列を受理する。
    
  • よって、
    
  • Mがwを受理するならば、Dは受理しない文字列がひとつだけ存在する言語である。
    
  • Mがwを受理しないならば、Dはあらゆる文字列を受理する。
    
  • あとは自明。
    
  
  

このあたり、あまり面白みがないような気がする。「写像帰着可能性」は面白そうなので、期待する。
次回は「単純な判定不可能問題」。こつこつ。

【例解UNIX】Cの復習(2)：ポインタ、バイトオーダ、複雑な型

こつこつ。

• 「よくあるポインタの間違い」 はい。こういう風によく間違えてました。。。
  

次回は、「2.2 バイトオーダ」から

【シプサ】5 帰着可能性 (その3)

こつこつ。E[LBA]の判定可能性から。丁寧に追ってみる。

• 「E[LBA]は判定不可能である」
  
  
  
  • A[TM]からの帰着で確認する。E[LBA]が判定可能 -> A[TM]が判定可能。どう帰着できるか。
    
  • 「TM Mと入力 w に対してあるLBA B を構成する。LBA Bの空性検査をすると、Mがwを受理できるかどうか判定できる」ということを実現できればよさげ。しかしBはどんなものか?
    
    
    
    • Bは、「wに対するMの計算履歴の表現」を入力として受け取る。
      
    • そして、それが受理計算履歴なときにそれを受理する。ちょっとメタ。
      
    • するとL(B)は、たったひとつの文字列を含むか、空集合かである。
      
    • こんな方針。
      
    
    
  • 整理して書いてみる。
    
    
    
    • E[LBA]を判定するTM R が存在するとする。
      
    • TM Mとwがある。
      
    • TM Sがあり、それはMとwに応じて動作(自己構成?)する次のような機構をもっている。
      
      
      
      • TM S は、Mとwから上で述べたLBA Bを構成する。
        
        
        
        • LBA Bの概要。
          
        • LBA Bの入力は計算状態を"#"で区切って連結したものとする。
          
        • C1が開始状態であり、Clが受理状態であり、CiからCi+1がMの遷移関数によって導出されることを確認する。
          
        
        
      • LBA Bから表現<B>を作る。
        
      • それをRに入力する。
        
      • Rがそれを受理するならば、Sは拒否する。Rがそれを拒否するならば、Sは受理する。
        
      
      
      
    • このTM Sは、A[TM]を判定する。
      
    • A[TM]は判定不可能だから矛盾が発生しており、仮定したTM Rは存在しない。
      
    • ゆえにE[LBA]は判定不可能である。■
      
    
    
  
  

これ結構複雑だよなぁ。

【例解UNIX】Cの復習(1)：マニュアルの読み方、エラー処理、構造体、共用体 (その2)

こつこつ。章末問題開始。

• 問題 1 (10分くらい)
  
  
  
  • うーん。大きな違いはない。SUSv3の方が長いといえば長い。
    
  
  
  
• 問題 2 (10分くらい)
  
  
  
  • うわ、あっさり出きたけど。ポインタについて理解があやふやでgccに注意されまくりなのを直してなんとかなっている現状。まずい。
    
  • とりあえず、この本を読み進める中で経験値が増して解決されることを期待する。
    
  • それで駄目ならポインタの復習を柴田さんの本でやることにする。
    
  
  
  
• 問題 3 (3分くらい)
  
  
  
  • バイトアライメント自体は固定であり、同じコンパイラ設定でコンパイルされたバイナリだけで動くなら問題ないと思うのですが。
    
  
  
  
• 問題4 (40分くらい)
  
  
  
  • 探索を考えなくてよいようなので、結構シンプルだった。
    
  
  

双方向循環リストが課題に出てきたので、今までやってきた道筋というか準備してきたことがそんなに的外れではないように感じた。少しうれしかった。

次回は「Cの復習(2):ポインタ、バイトオーダ、複雑な型」。難易度二つ星なので、ちょっと緊張。

【シプサ】5 帰着可能性 (その2)

こつこつ。

• 計算履歴を用いた帰着可能性
  
  
  
  • 「A[TM]をある特定の言語に帰着可能であることを証明するための重要な手法」
    
  • 「判定不可能性を示そうとする問題が何かの存在を調べることを含むとき、この手法はしばしば役に立つ」
    
  • 計算履歴とは、開始状況と「なんらかの状況」をつなぐような計算状況の列のこと。なんらかの状況が受理状況であるならば受理計算履歴と呼ぶ。拒否状況ならば拒否計算履歴と呼ぶ。計算履歴は有限の列であり、停止しない動作については存在しない。
    
  
  
  
• 線形境界付きオートマトン (linear bounded automaton)
  
  
  
  • テープが有限というのはわかるのだけれど、
    
  • 「テープ・アルファベットを入力アルファベットに比べて大きくとることによって、使用できるメモリを定数倍まで増加できる」
    
  • というのがわからない。。。
    
  • 定義がこれほど理解できないのは由々しきこと。掟破りだがWikipediaへ。
    
    
    
    • 「チューリングマシンと異なるのはLBAのテープ長が有限であることで、その長さはテープ上の初期入力文字列の長さに比例する」
      
    • ぬ、テープの長さは動的なのか?
      
    • Linear Bounded Automata によると「Definition. A linear bounded automaton (lba) is a multi-track Turing machine which has only one tape, and this tape is exactly the same length as the input.」とな。シプサの定義ともWikipediaの定義とも違う。
      
    • これらを繋ぐ説明 Linear-Bounded Automata 。これでわかった。
      
    • すなわち、入力文字列長さnはもちろん可変。そのk倍のテープ長であることになる。ここでkはオートマトン毎に固定。なので、実際のテープ長であるknは入力につれて動的。
      
    • これを実現する方法として、いまのところ、三つの方法をみた。
      
      
      
      • k=1として、テープアルファベットの数をます。あたかもknのテープ長があるようになるようにテープアルファベットを増すということ。
        
      • ひとつのテープとしてはk=1として、複数テープ(k本)用意する方法。
        
      • ひとつのテープの長さをknとする方法。
        
      
      
    
    
  • ここではあたりまえだがシプサの定義で進める。
    
  
  
  
• LBA Mが、q個の状態とg個のテープアルファベットをもつとき、長さnの入力文字列において、q*n*(g^n)個の異なる計算状態が存在しうる。ユニークな計算状態はこれで尽きている。
  
• このとりうる状態の数が有限で、ループに関する考察をするというのが、ポンピング補題との関連を感じる。
  
  
• A[LBA] = {<M, w> | Mは文字列wを受理するLBA}
  
• 「A[LBA]は判定可能である」
  
  
  
  • これは簡単。存在しうる計算状態の数が有限なので、そのステップを超えたときそれはループということだから拒否してよい。
    
  
  
  
• E[LBA] = {<M> | LBA M は L(M) = 空集合}
  
• あるLBAがあたえられたとき、それがまったく何も受理しないLBAかどうかを判定するアルゴリズムがあるかどうか、ということ。
  
• 「E[LBA]は判定不可能である」
  
• それは無い、ということ。
  
  
  
  • 結構むずかしい。
    
  • もやもや考えると徐々にわかってきた。
    
  • しかしもう業務なので、次回、整理することにする。
    
  
  

こつこつ。