今すぐ観るべき映画『聲の形』の81の良さポイント

概要 これは映画『聲の形』の良さ溢れるシーンのメモ書きです。 ネタバレを含みますが、良さをすでに理解している方向けの記事なので、映画『聲の形』の良さを知らない方はここでお帰りください。 映画『聲の形』について ここは理解している前提とし、説明…

ZFCはじめてみるの巻2

順序対の定義。 結構きつかったのでコメントもなしにガリガリ書いていた。もっときれいなやり方があるはず。 順序対の定義と性質 相変わらず、ComprehensionとかReplacementは先送りにしていますがどうなることか。

ZFCはじめてみるの巻

コメントなしコードだけ。 0 /= { 0 } の証明が一応出来ました。 ZFCカッコ仮

ssrnat 練習

今度はソフトウェアの基礎の演習問題. gist9c82a2ca96660cc64a87 cf. ソフトウェアの基礎 rewriteするときに, 右分配律mulSnrを使っています。 ------>> Ssreflect.ssrnatのMultiplication.にあるLemmaから. 牛刀振り回してる感じありますが、一応証明です。

ssreflect始めました.

ssrboolの練習。とりあえずソフトウェアの基礎とか見ながらやってます。 ssreflectっぽくないですが、そのうちrewriteとかガリガリ使っていきたいです。 gist31a74ec01b8961c4f506

覚書

覚書です hoge.htmlからhtmlへのリンクファイル一覧を取り出すコード $htm = cat hoge.html -Raw -Encoding UTF8 $regex = "<\s*a\s*[^>]*?href\s*=\s*[`"']*([^`"'>]+)[^>]*?>" $pat = $htm | select-string -pattern $regex -AllMatches $pat.matches | %{…

master thesis

毎々お世話になっております。 修論:"Rigid ω_1 Trees and Their Preservation" です、ご確認頂きたく。 と冗談はほどほどにしまして、修論です。 コピペはしてないです。あと英語が残念な点に関しては勘弁下さい。 あと、修論書いたあとに気付いた、という…

本日のmathoverflow案件

なんか最近mathoverflowの更新が少ないんだが 大学関係者はこの時期忙しい仮説. それは別として math.stackexchange のほうにいつぞや気になっていた質問投げました. About generically Knaster property 解答絶賛募集中なので知ってる人はなんかお願いし…

もうだめ

本日のmathoverflow案件 これについて. Question: In different books one can find different implicit definitions for a large cardinal axiom. My question is that which one of these definitions are more popular or standard amongst set theorist…

はてブロに移転しました

最近こんなことしかやってないな 本日のmathoverflow案件,をいこうとしたが,解答が来る前に質問者が自己解決してしまったのかどうかとにかくよくは知らないが,質問自体が引っ込められていてリンクを貼ることもできない. とんでもなくフラストレーション…

MathOverFlow-battle

さっそくですが参戦しました。 Preservation of some stationary sets by sufficiently closed forcing そんなことしてる暇あったら修論やれ

まじで勘弁して下さい、Hamkins先生

本日のmathoverflow案件 Can a Suslin line be 2-entangled? Dear J. D. Hamkins先生……… ここに書いてある定理、わたしの完成間近の修論に書いてるやつです。 いやもうちょっと丁寧にやったのでここまで簡単に証明はできていませんが、 修論の主定理にかなり…

archive管理を適当にやった話

sh

あれだ。面倒なのでコードだけ乗っける #!/bin/bash DATE=$(date +%F) WORKDIR=./ ARCHIVE=${WORKDIR}/archives LOGFILE=${ARCHIVE}/.log function archive_less { TIME="" while : do echo -n "When the article written?([ENTER] to display list): "; rea…

米田さんの話

圏論やってると米田さんにお世話になる機会も多いと思うが, イマイチ意味も使い方も分からんいう僕みたいな人向けの記事です. 記事を書くにあたって,主に 圏論番外:米田の補題の周辺から(via 檜山檜山正幸のキマイラ飼育記) や, MathAdventCalenderの12…

ちょっと入出力の練習

連投です. 某H社のtex記法がアレなのでGoogle Chart APIを使っているのですが, 直に打つのは面倒なので,latexの$$←こいつで挟んだ記法からGoogle Chartのイメージを取ってくるhtmlに変換するスクリプヨを書いていたわけです. まあgauche使います. いい入出…

安定のHamkins大先生

本日(昨日)のmathoverflow案件: Increasing and Descending Chains of Inner Models for Measurable Cardinals初見で(b)がわかったのでtwitterの鍵垢に書いたんだけど,一応ここにも書く. ただ時間的にその直後にHamkins先生のよりgeneralな回答が載ってい…

C85

コミケで薄い本"The dark side of Forcing II"のなかの一つの記事10pagesくらいを担当しました。 内容は、KunenのInconsistencyの定理についてです。 Reinhardt基数のことについて書いたのです。 ラインハルト基数。 でも書籍中ではリインちゃんと読んでいま…

Emacs で Racket の Repl を使えるようにするための覚えがき。

いいかげん乳離れならぬGauche離れをしたいと思っていたので。Geiserと呼ばれるパッケージを使うのが楽です。 Emacs で package-install して持ってきます。 (詳しくはこことかに載っています) 使うrepoはmelpaで、emacs上で [M-x] package-refresh-contents…

2013年とは一体何だったのか

手帳見ると思い出して涙が出るかもしれないので思い出せる範囲で書きます。1月某活してました。味噌カツではないです。セミナーセミナーセミナー。なおお金はほぼでない。2月某活つらいです。主に高速バス。 おそらく予算的にもJRバス使うのがたぶんいい。 3…

testes

This entry is made to learn how to use Google Chart API. The following mathematical article is based on a sequence of facts in set theory, that is known to be proved with ZFC:Let be the Cohen forcing which adds one Cohen real.Then the foll…

flymakeすげえ

flymake名前は聞いたことあったけど使ってみたらヤバかった。とりあえず、infoとして にゃあさんの戯言日記: http://d.hatena.ne.jp/nyaasan/20071216/p1 からとって来ました。CC-modeだけでは寂しいので、gaucheと連携させたい、というところで、 Higepon's…

終幕

2012年色々あったので適当にまとめておこうと思う。 1月: twitter再開した記録がある。あと適当にこなした卒研。 2月: 結構頑張った。最近研究してることの種は全部ここで蒔かれたと言ってもいい。 3月: 某つどいをネットで眺める。このへんの記憶はない。 4…

(੭ु´・ω・`)੭ु⁾⁾(੭ु´・ω・`)੭ु⁾⁾

SGL

SGLの4章読んでTopos導入をしている感じなのですが、 generalized elementってなんやねん という話で、ちょっと思ったことを書く。 Definition: をtopos、をその対象とします。 一般化元(generalized element)とは射のこと。 と言われてもなんのこっちゃ。 …

(੭ु´・ω・`)੭ु⁾⁾

演習問題淡々と。 3章を読んでいるのですが、ここら辺でSchemeの肝になってる静的スコープと説明と動的なデータをどうやっていじるかの説明が入っている感じです。 今回は3.3章のMutable Data Structureのところを読んでいます。 ;;;;;;;;;;;;;;;;;;;;;;;;;;…

にょん٩(๑❛ᴗ❛๑)۶

SGL読んでるけど、topos考えるときはやはりSetsとの対応を念頭にしながらするとよい、ということがわかりました(小並感)あと、この本、本当にIntroductionって形容がぴったりで、読みやすいですね。今まで敬遠してたのがバカバカしいです。 簡単なのでみん…

うにゃーーーー

Haskellでなんちゃって Turing Machine 作ろうとしたら謎仕様になったとうという話。 もともと monad 書く練習しようと思って色々データいじっていたんだけど、かなり脱線したので一応書いておきます。 実はこの辺は教科書で勉強したことがなくて、かなり記…

'(..'('(これはquoteのついた文章です)はquoteのついた文章です)はquoteのついた…

quotationがよくわかりません、という話になりました。実際、proc. (quote )はexpressionをすぐに評価するもので、なんですか、評価はapplicative-orderじゃないんですか!みたいな感じになりました。修行不足なので出直します。

おわり。

はい、今期はおわり。 お疲れ様です。にゃ

ゴゴゴゴゴッ

K(S(SI(K(S(K(S(S(KS)K)(S(S(KS)K)I)))(S(S(KS)K)I(S(S(KS)K)(SII(S(S(KS)K)I)))))))(K(S(SI(K(S(K(S(S(KS)K)(SII(S(S(KS)K)I))))(S(S(KS)K)(S(SII)I(S(S(KS)K)I))))))(K(S(SI(K(S(S(KS)K)(S(K(SII(S(S(KS)K)I)))(S(S(KS)K)(S(S(KS)K)(S(SII)I(S(S(KS)K)I)))…

meow〜ッ!

演習問題淡々と。面倒なので、実装しなさいみたいな問題の解答だけ: ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Exercise 2.65 implement the union-set, intersection-set for binary tree data (define (union-set1 tree1 t…