2005-10-03 [長年日記]
λ. 『司法のしゃべりすぎ』, 井上馨
先日の大阪高裁判決に関連して幾つかのブログで紹介されていたので、読んでみた。それなりに面白かったし、論理的に書かれているので、読んでいて気持ちよかった。ただ、同じことを何度も繰り返してクドイという印象はあるが。
判決の理由欄に記載されるのは、判決主文を導くのに必要十分なものであるべきで、それ以外の関係ないものは蛇足(傍論)であり、氏名欄に住所を書くが如くに不適切なものであるという。そして、その蛇足を含む判決は現実に数多く存在し、弊害を生んでいるのだそうだ。
どんな弊害があるかといえばまあ色々あるわけだが、著者の主張は余計なものを作るために必要となる様々なコストの問題と、「理由欄中の判断には法律的効果は無いにも関わらず、現実には社会的な影響力を持つため、蛇足を盛り込むことは裁判所がその領分(具体的紛争の裁定・解決)を越えた影響力を行使することに繋がる」ということに要約できそうだ。
(追記予定)
先日の大阪高裁判決
このような考えに基づけば、先日の判決の理由でも「控訴人らが主張するような権利ないし利益が侵害されたものと認めることはできない」ということに関する部分だけが、棄却という判決に関係していて、それ以外の「参拝の職務行為性」や「違憲性」は原告側の請求の棄却を導くのには全く不要な蛇足ということになるだろう。
高松高裁判決
(2005-10-06 追記) 10月5日に高松高裁判決が「参拝が原告に何らかの強制力を及ぼしたり、不利益を課したとは認められない」として損害賠償請求を退けたが、こっちは「損害賠償請求が認められない以上、裁判所が抽象的に合憲性を判断する権限はない」として憲法判断にも踏み込まなかった。これは具体的紛争の裁定・解決という司法の領分を守ったということになるか。この本を読んだとたんに対照的な判決を見ることが出来て面白かった。
λ. Overloading in Agda. Catarina Coquand
を見た。
- 「Similar to Axiomatic Type Classes in Isabelle」と書いてあるけど、Isabelleにも似たようなのがあるのか。
- Possible Extension の「Since we can name instances, we could have overlapping instances that is not used in constraint solving」の部分がちょっと良く分からなかった。
【2006-03-28 追記】 以下のような例を考えるとm1とm2は両方ともmを対象としているのでオーバーラップしているという話か。「that is not used in constraint solving」はどういうことを言っているのか良くわからないが、こういう場合はどう扱うのがいいのかね。
join (|m::Set->Set) (|a::Set) (|m1::Monad t) (|m2::Monad t) :: m (m a) -> m a join = (>>= id)
λ. この日記でのスライド等の扱い
スライドのためだけに新しいカテゴリを作るのも面倒なので、 とりあえず「論文」カテゴリに入れておこう。