12月ごろ思いついたことであろうか。

地球は磁石であって、磁石の極と自転の極はすこしずれている。これを利用すると、地球の自転を遅くしながら発電することができるに違いない。どういう仕掛けがあればいいんだろう。

とりあえず、どのくらいのエネルギーを取り出すと、地球の自転が1%遅くなるのか計算してみよう。ん、しかし自転が遅くなるだけではなくて、磁極とか自転の極とかが、どうしても動いちゃうのだろうか。よくわからない。

きょうしたこと

• 底本と校訂(というほどたいしたことはしていない)した原稿を送る
• 郵便局で為替を買う
• 銀行でなんかの支払い手続きをする
• 用紙サイズの合ってないデータを送ってプリンタを止めて先生を困らせる(わざとではない)
• 麻疹風疹混合ワクチンの接種を受ける
• キャンパスの中にある会社のオフィスにお邪魔する
• 小学校の友人と再会して世間話をする　京都とか、他の学部とか

あと、インタビューの記録を音から文字に起こさないと。これは一旦眠ってしまうと、どうしようもなくなりそうだ。

ちょこまかしているが、ちょろまかしているわけではない。

ダウンロードして試してみた。速すぎてちょっとついていけない感じ(?)。不都合な事がみつかったらここに追記します。via みずぴー日記

すこしずつ確実に、顔を出している。まだ皮をかぶった部分も、その下のでこぼこが感じられるようになってきた。気になって舌の先で触ってしまう。はえたばかりの歯は鋭いのだろうか、舌の先が傷ついてすこし痛い。

いったい何を思ってこの時期に生えてきたのであろうか。はぐきの中から外に出ようがでるまいが、赤みをおびた暗がりの中で、ときどき押されたり揺らされたりして暮らしているだけなのだろうと思うのだが。生えてみるとよいものであるか、親知らず。たしかに光というのは、ときたまちらちらと見えるのが美しいのかもしれない。

ちょっと痛い。でも土地はひろびろと余っているし、すなおにまっすぐはえてきているので、放っておこう。下手に抜いたりしたら隣の歯が倒れてきそうだ。

月曜から水曜まで仙台です。

なんとずれ具合まで計算できるらしい。このまえ都庁の前で地球の重力に反対と叫んでしまったのがよくなかったのだろうか。ごめんなさい。ニュートンのバケツっぽく、地球の自転が影響してたりして。

わけあってMALLのカット除去手続きを書いた。パーサを先に書こうか、肝心な拡張を先にしようか。

これが簡約されて

output : (beta : A  (P) delta : A ) ,
input : (input0 : ~A  (X) input1 : ~A )
{
  on internal_in -- internal_out plug
    split output as beta, delta in
      fork internal_in as
      | alpha with beta : A -> alpha =A=> beta
      | gamma with delta : A -> gamma =A=> delta
  to
    split internal_out as param0, param1 in
      fork input as
      | input0 with param0 : A -> input0 =A=> param0
      | input1 with param1 : A -> input1 =A=> param1
}

こうなる

output : (beta : A  (P) delta : A ) ,
input : (input0 : ~A  (X) input1 : ~A )
{
  split output as beta, delta in
    fork input as
    | input0 with beta : A -> input0 =A=> beta
    | input1 with delta : A -> input1 =A=> delta
}

(追記) キーボードとスクリーンなるdummy証明を用意したら急に楽しくなってきてしまった。同時に証明が簡約されていく様子が一段ずつ表示されると楽しいかもしれない。

(追記)わーいわーい

こんどフランスからやってくる留学生のなまえがわかったので、そのひとの論文を読んでみた。フランス語は忘れかけているぞ。メゾ領域の統計物理っぽい。んー、んー、んー。
にょろーん、ころーん、ごろーん、ばるーん 。