日々の流転

λ. 近代思想

今日は、「人間主義」について。行動の究極的目的を(神・善・正義でも、快楽・金銭・権力でもなく)人間に置くってのがやっぱりポイントだろう。

「天動説 → 地動説」と「神中心主義または宇宙中心主義 → 人間中心主義」を対置して「ルネッサンスの逆説」と呼ぶのは筋違いに感じられる。

λ. LK

「(A → B) → ((A → ¬B) → ¬A)」の証明なんかに苦戦。かなりダメげ。でも、シーケント計算とか推論規則とかって面白いなぁ。

[2005-05-30 追記] 一応書いておこう(exchangeは省略)。ちなみにLJで十分。それにしても、「→左」規則は直観的でないと思う。

                     B |- B
                   ------------ (¬左)
          A |- A     B, ¬B |-
         ---------------------- (→左)
A |- A      B, A→¬B, A |-
------------------------------------ (→左)
A→B, A→¬B, A, A |-
----------------------- (contraction左)
A→B, A→¬B, A |-
----------------------- (¬右)
A→B, A→¬B |- ¬A
------------------------ (→右)
A→B |- (A→¬B)→¬A
-------------------------- (→右)
|- (A→B)→(A→¬B)→¬A

ちなみに、Agdaだと簡単だし直観的。

--#include "Hedberg/SET.alfa"
open SET use Imply, Not
 
z (|A,B::Set) :: (A `Imply` B) `Imply` ((A `Imply` Not B) `Imply` Not A)
z = \(x::A `Imply` B)-> 
     \(y::A `Imply` Not B)-> 
      \(a::A)-> 
       case y a (x a) of { }

λ. 読んだ本

• 「BASTARD 第22巻」　萩原一至
• 「遊戯王 第24巻」　高橋和希
• 「ノルマンディーひみつクラブ　第4巻」　たかはしみきお

λ. noname

昨日の日記に何故かrefererが残っているnoname.tar.gzだけど、何やら面白そう。

λ. というか、樋口さんのmiscディレクトリの中身を見て凹む。とてもかなわない。

λ. スピード狂のための道標

この文書は、GNU CやFortranなどで書かれたプログラムを少しでも高速化したい、という時に役にたちそうな情報をまとめたものである。GCCのオプションやGNUの独自拡張について、高速化に関連する部分を様々な文書から抜粋してまとめてある。また、プログラム高速化のためにはアセンブリ言語を理解したり書いたりすることができると非常に役にたつため、i386のアセンブリ言語についても簡単に解説する。

[2005-03-12 追記] 非常に役に立つ文章だったのだけど、消えてしまったみたい。 手元には保存してあるけれど、残念なことだ。というわけで、Internet Archive を参照のこと。

λ. キノの旅検索エンジン - Kino Search

.

λ. 『吸血姫美夕　十』

『吸血姫美夕　十』

垣野内成美[画] 平野俊貴[原作]

λ. マイナスイオン

最近クーラーやトイレに使われているマイナスイオンとやらがあるけど、金になるものは金にしてやろうというメーカーの考えにはひっじょーに共感を感じる。それについていく一部の消費者の馬鹿さ加減には呆れるけど。

とか書いてみるテスト。

λ. 横山哲郎, 『効果的な融合変換のための変換戦略の記述法とその実現』

を読んだ。

λ. String#intern

1.8では空文字列のinternはエラーになったのね。Rinnではまった。

λ. 政策・メディア研究科 修士課程 入学試験

今日が一次試験の小論文だったわけだが、これが大失敗。時間配分に失敗して半分も写しきれなかったよ。欝。こりゃ、秋に再挑戦することになるか……

λ. 知恵の輪

現実逃避すべく、生協で知恵の輪など買ってみる。このGlassとかいうやつなのだが、なかなかむずい。

λ. 交渉人 真下正義

を観てきた。

λ. Haskell と OCaml

型システムに注目すると、HaskellになくてOCamlにあるのは、Object, Polymorphic Variant, Functor (parameterized module) かな。一方OCamlになくてHaskellにあるのは、Higher Order Polymorphism, Type Class (Ad-hoc Polymorphism), (Predicative) Rank-n Polymorphism, GADT(Generalized Algebraic Data Types) といったあたりだろうか。*1

Haskellで型関係の宣言に data, newtype, type の三つがあるのが分かりにくい というのは一理あるけど、これらはそれぞれ違った意味を持っているので、全部一緒にしてしまうのが良いかどうかは一概には言えないと思う。少なくとも私がOCamlを最初に触ったときには全部typeで済ませていることに少し混乱しました。

関連エントリ

• newtypeはHaskellの仕様に不要では?

λ. 知識発見法

Alephを使った実習。 バイアスの設定、正例のみからの学習、一貫性制約の発見。 Alephの挙動がなにやら不思議。

しかし、モード宣言で入力が「+」で出力が「-」というのは、ちょっと直観に反するような。……圏論での exponential functor の variance と、CPLでのvarianceの表記法から、入力が「-」で出力が「+」だとつい連想してしまうので。

λ. 古川研:Abduction勉強会

Hierarchical planning に関して。

• from first principles = 元々の原理から
• circumscription
  • <URL:http://en.wikipedia.org/wiki/Circumscription>
  • 極小限定?
  • どういう場合に predicate completion に落ちるのか?

λ. OrdのcompareでNaNを比較

OrdクラスのcompareメソッドでNaNを比較してみたら、何と比較しても常にGTが帰ってきた。

Prelude> let nan = 0/0
Prelude> nan
NaN
Prelude> compare nan nan
GT
Prelude> compare nan 0
GT
Prelude> compare 0 nan
GT

そこで、Ordのインスタンスが全順序集合であることを期待しているコードにNaNを放り込むと、変なことが起こる。例えばData.Map。

Prelude> :module +Data.Map
Prelude Data.Map> let m = insert nan 0 empty
Prelude Data.Map> m
{NaN:=0}
Prelude Data.Map> insert nan 1 m
{NaN:=0,NaN:=1}
Prelude Data.Map> lookup nan m
*** Exception: user error (Data.Map.lookup: Key not found)

λ. トマト鍋(?)

キムチじゃなくてトマト。美味しかった。 けど、ちょっとやらかしてしまって欝。