2006-01-18
λ. ライブドアショック
たまたまキャッシュポジションを増やしていたのでラッキーだった。 下落で損もしたけど、以前から購入したかった銘柄が比較的手頃な価格で買えたし、今のところトータルではそう悪くない感じ。 明日以降どうなるか知らないけどさ……
ネタ色々
マネックス証券批判について (2005-01-20 追記)
いきなり掛目をゼロにしたのは性急過ぎたというのはあるとは思いますが、掛目を引き下げたこと自体は当然だと思うし、ちょっと批判されすぎという気がします。
ヤバイことになった企業の株なり何なりの担保としての評価を下げ、契約に基づいて担保の追加なりを求めるのは当然であり、普通の金融機関ではどこでもやっていることです。お金を貸す以上そういったことは当然でしょう。 ましてや、代用有価証券は「代用」というくらいで、所詮は委託保証金の代用に過ぎないんですよね？ マネックス証券の言い分の「特定の株式の担保評価が困難になった場合、担保価値を下げることは経営の選択肢の1つ」というのは全くもってその通りだと思う。
今回の掛目の引き下げで追証に追われマネックス証券を批判している人は、自分が借金をして株を買っているということにあまりに無自覚だったのではないでしょうか。レバレッジのかかったハイリスクな取引を行い、これまで利益を追求してきながら、いざ失敗したら他者に責任を転嫁しようとする。自業自得でしょう。
λ. インターネット構成法 最終試験
予想していたより難しかった。問題は以下の通り。
- 問題1
- MACアドレスの特徴とその役割を100字以内で説明しなさい。
- 問題2
- Spannning Tree Protocol (STP) を100字以内で説明しなさい。
- 問題3
- Port VLAN を100字以内で説明しなさい。
- 問題4
- Autonomous System (AS) を100字以内で説明しなさい。
- 問題5
- Interior Gateway Protocol (IGP) と Exterior Gateway Protocol (EGP) に おける経路制御プロトコルを1つづつ挙げなさい。
- 問題6
- マルチキャストの経路制御プロトコルを1つ挙げなさい。
- 問題7
- IPアドレスのマスクについて、経路制御の観点から100字以内で説明しなさい。
- 問題8
- 経路表の構成要素を2つ挙げなさい。
- 問題9
- デフォルトルートを100字以内で説明しなさい。
- 問題10
- 光ファイバを用いたネットワークにおける帯域を示す単位として、OC(Optical Carrier level)が用いられる。OC12は622Mbpsを示し、OC48は2.5Gbpsを示す。このとき、OC768が示す帯域を答えなさい。
- 問題11
- 建物内の同一フロアなど、限られた空間に複数の無線LAN基地局を設置する場合、どのような点に注意すべきかを説明しなさい。(字数制限なし)
- 問題12
- 静的経路制御と動的経路制御の違いを、それぞれの特徴を具体的に説明しながら説明しなさい。(字数制限なし)
- 問題13
- 二つの隣接するサブネットA(192.168.1.0/24)とサブネットB(192.168.2.0/24)の2本の回線によって接続性を冗長化し、現用系の接続性が失われた際に予備系に切り替わるよう工夫したい。このとき、二つのサブネットを接続する機器(ルータやスイッチ)や回線をどのように接続するか図示しなさい。また、そのネットワーク構成をとるのに必要な通信技術またはプロトコルが図中のどの機器で動作すべきか、必要であればその設定を含めて説明しなさい。(字数制限なし)
2008-01-18
λ. 米田の補題とCPS変換
檜山さんのところで米田の補題とCPS変換の関係の話が紹介されていた。まだ読んでいないのだけど、多分こういう話だろうと思うので、読む前にちょっとメモ。
「locally-small な圏 C、関手 F : C→Set、対象 A∈|C| について自然同型 Nat(hom(A,-), F) ≅ FA が成り立つ」というのが米田の補題。 ところで、自然変換と多相関数は似たようなものなので、これを多相ラムダ計算の型で書くと、大体 ∀X. (A→X)→FX ≅ FA となる。 ここで、Fとして恒等関手を用いると ∀X. (A→X)→X ≅ A となり、同型は以下のΦとΨによって表現される。
id : ∀X. X → X id = ΛX. λx:X. x Φ : (∀X. (A→X) → X) → A Φ = λα:(∀X. (A→X) → X). α A (id A) Ψ : A → (∀X. (A→X) → X) Ψ = λa:A. ΛX. λk:A→X. k a
これはまさにある種のCPS変換になっている。
これが同型であることを多相ラムダ計算で示すには、通常の簡約規則と関数の外延性だけでは不十分で、パラメトリシティが必要になる(証明は Theorems for free! (20050218#p03) を参照)。 また、元の ∀X. (A→X)→FX ≅ FA も同様にパラメトリシティを用いて証明可能。→ 米田の補題と多相ラムダ計算
【2009-07-15 追記】 CPS A = (∀X. (A→X) → X) とおくことにする。 型 A と型 CPS A が同型なわけだけど、そうすると A→B と CPS A → CPS B も同型対応するようになる。
Φ' : (CPS A → CPS B) → (A→B)
Φ' = λg : CPS A → CPS B. λa : A. Φ (g (Ψ a))
= λg : CPS A → CPS B. λa : A. (g (ΛX. λk:A→X. k a)) B (id B)
Ψ' : (A→B) → (CPS A → CPS B)
Ψ' = Ψ (f (Φ α))
= λf : A → B. λα : CPS A. ΛX. λk : B→X. α (λa : A. k (f a))
ついでにHaskellで書いておく。
{-# LANGUAGE RankNTypes #-}
type CPS a = forall x. (a -> x) -> x
-- 値のCPS変換
psi :: a -> CPS a
psi a = \k -> k a
phi :: CPS a -> a
phi x = x id
-- 関数のCPS変換
psi' :: (a -> b) -> (CPS a -> CPS b)
psi' f = \x k -> x (k . f)
phi' :: (CPS a -> CPS b) -> (a -> b)
phi' g = \a -> g (\k -> k a) id
2017-01-18
λ. 2016年振り返り
全般的に体調的にも精神的にも低調で、倦怠感にずっと悩まされ、精神的には悩んでも仕方がないことに悩み、理不尽に対して無駄に怒りと鬱憤をため、あまり生産的な方向にエネルギーを使えなかった一年だった気がする。 自分にコントロールできないことには囚われず、コントロールできることに集中すべきなのだけど、そういう割り切りそれ自体を維持するにもエネルギーがいるよね。
年初の目標を振り返ってみると、達成できなかったことも多いけど、かといって全く何もやっていなかったわけでもないことが分かって、ちょっとポジティブな気持ちになった。
- SMT-COMP 参加
- → 自作のSMTソルバtoysmtに、有理数線形算術の理論と、非解釈関数(uninterpreted functions)の理論を実装して、SMT-COMPに参加。 出場した全てのカテゴリ(QF_LRA, QF_UF, QF_UFLRA, QF_RDL)で最下位という予想通りの結果だけれど、とりあえずちゃんと動いたようで良かったよかった。 その後、ビットベクタの理論については実装したし、後は整数線形算術の理論に対応したうえで、性能をもう少しなんとかしたいところ。 やりたいことに対して歩みは遅いけれど地味には進められているかな。
- MOOCの受講 x3
- → Courseraのガロア理論のコースを受講してみてたけど、途中でついていけなくなって、次の回にスイッチして復帰しようともしてみたが、結局復帰できないままになってしまった。他に、UdacityのTensorFlowでディープラーニングを学ぶというコース も覗いてはみたものの、こちらは本格的に取り組むことはなかった。 年の途中で一回仕切りなおしたかった。
- 発表 x2
- → Haskell Day 2016 で SAT/SMT solving in Haskell という talk をした(slideshare, PDF)他、小ネタとしては恒例のICSE2016勉強会で論文2本を紹介(PDF)したのと、某イベントでMOOCについて簡単に紹介した(slidehare, PDF)くらいか。 お仕事での発表が全くできていないのが残念……
- 勉強会やイベント参加頻度を増やす
- プログラミングコンテストとかセキュリティとかはまあボチボチと
- → CTFについては、DEF CON CTF 2016 Qualifiers (writeup), MNCTF2016 (writeup), Trend Micro CTF 2016 Online (writeup), HITCON CTF 2016 (writeup), SECCON 2016 Online CTF (writeup) と、5回参加できた。 ただ、あんましセキュリティ的な要素のない問題ばかり解いていたので、セキュリティ系のスキルが向上した感じはないけれど。
- → プログラミングコンテストは、ICFP Programming Contest がせっかくの日本開催の貴重な機会だったので、運営側のチームに混ぜてもらったのだけれど、途中で脱落してしまった。 参加者としては参加せず、運営の様子を裏からちょっと見ていて、それはそれで貴重な機会ではあったけれど、本当に残念なことをした感じ。 他には Google Code Jam とかに参加したくらいで、これもパッとせず。
- 語学はコツコツと
- → rarejobは結局年の初めと終わりの数えるほどしかできず。iknowの方はもう少しできたけれど、まああんまりコツコツ続けられた感じはしない。TOEIC(IP)はちょっとだけ上って925に。
- どっか海外旅行
- → どっかアジアにでも行きたいと思っていたが、結局行けず。
- ランニング 400km
- → 距離はトータルで179kmほどで、目標の45%ほどに留まった。 月別では1月19.6km、2月14.3km、3月39.0km、4月9.9km、5月14.9km、6月16.2km、7月8.4km、8月2.5km、9月7.6km、10月2.8km、11月11.1km、12月32.4kmという感じ。 倦怠感に負けた。
- フルマラソン
- → フルマラソンには結局挑戦できず。 ハーフマラソンについては、2015年のかつしかふれあいRUNフェスタでは2時間をギリギリ切れなくて残念だったところ、2016年はネットタイムで 1:59:19でなんとか二時間切れた(RunKeeper)のは良かった。
