トップ «前の日(06-04) 最新 次の日(06-06)» 追記

日々の流転


2001-06-05 梅雨だね〜。ジメジメ、蒸し暑〜い。

λ. 近代思想

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

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

λ. 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 { }

λ. 読んだ本

Tags:

2002-06-05

λ. noname

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

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

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

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

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

Tags: URL

λ. 『吸血姫美夕 十』

『吸血姫美夕 十』
垣野内成美[画] 平野俊貴[原作]
Tags:

λ. マイナスイオン

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

とか書いてみるテスト。


2003-06-05

λ. String#intern

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

Tags: ruby

2004-06-05

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

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

λ. 知恵の輪

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

本日のツッコミ(全2件) [ツッコミを入れる]

ψ takot [クリアしますた.]

ψ さかい [さすがtakotセソセイ!]


2005-06-05

λ. 交渉人 真下正義

を観てきた。

交渉人 真下正義 スタンダード・エディション [DVD](君塚良一/甲本雅裕/十川誠志)

Tags: 映画

λ. 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で済ませていることに少し混乱しました。

関連エントリ
Tags: haskell ocaml

*1 多分


2006-06-05

λ. 知識発見法

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

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

λ. 古川研:Abduction勉強会

Hierarchical planning に関して。

λ. 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)
Tags: haskell
本日のツッコミ(全2件) [ツッコミを入れる]

ψ kinjo [古川研の金城です。そういえば、東工大での勉強会の日程7月5日に決まりました。圧縮だとかベイジアンネットの計算法とかで..]

ψ さかい [情報ありがとう。 今回は多分参加できると思います。]


2008-06-05

λ. トマト鍋(?)

[トマト鍋(?)]

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

Tags: