PCがスリープできない。 実際はスリープができないのではなく、スリープすると起動しない。 しかも強制終了してみると、次回の起動時に起動しないし、強制終了してもまた同じ状態に！ リセットスイッチを押してみたら起動はしたので、まぁよしとしよう…。 さ…
ATSという言語のコンパイラをインストールしたのでメモ。 なんでATSを選んだのか 常々型システムが強力なC言語が欲しいと思っていた。 ATSはC/C++並のパフォーマンスが出るらしい言語で、 依存型とか線形型とかが使えるらしい。 （線形型とは何かよく知らな…
PNaClのチュートリアルのコード（のコメント）を読んだメモ。 PNaClとはなにか NaCl(Google Native Client)というものがある。 これは、Web上の任意のコードを安全に実行するためのサンドボックス技術らしい。 サンドボックスとブラウザはPepperAPIというAPI…
共有オブジェクトファイルのグローバル変数へのアクセスってどうなってるんだろう？ という事で、実験してみました。 Macの共有ライブラリ ココとか ココとか を読んだ。 Macでの共有ライブラリは.dylibという拡張子で作るらしい。 コンパイラには-dynamicli…
17日に研究室に配属されました。 10日に配属の発表があったとか聞いてない… （初日を知らずに昼ごろになって呼び出される羽目に…） とりあえず、課題が出たのでやったのでその記録。 課題 いわゆる「ナンプレ」を解くプログラムを作ります。 方針 やったこと…
カリー＝ハワード同型対応とか難しい事は分からんが、型と証明が一対一で対応するらしい。 型理論の枠組みの中でプログラミングを行おうとする言語には、証明が出来るものがある。 という事で、Agdaというプログラミング言語を習得しようとインストールして…
年の瀬なので今年やるはずだった事と、出来たこと、次にやる事を書き出して見る。 今年やるはずだった事 Rubyを習得 Railsを習得 集合・位相入門を読む 数理論理学を読む 数理統計学入門を読む 確率・統計演習１、２をする PRMLを読んで機械学習の基礎を習得…
Xcodeの使い方が少しわかったと思うのでメモ。 Xcodeで複数の実行ファイルを作成するプロジェクトを作る Xcodeでは一つの実行ファイルに一つのTargetというものが対応しているみたい。 このTargetというのはプロジェクトについていろいろ設定するところから…
brew updateしようとすると、Server aborted the SSL handshakeというエラーが出てアップデートに失敗した。 なんてことはない。KasperskyさんがHTTPSを確認したときにAbortさせちゃってるだけである。「安全なHTTPSを確認する」のチェックを外せばいい。
出来るだけ手間を省いてTeXを書く方法。PandocとXeLaTeXを使います。 Markdownで書いて、必要なとこだけLaTeXで書こうという魂胆。 ここに書いてあることのほとんど全部は ここ に書いてある。 最終目標はMarkdownで書いたレポートの体裁をPDFで出力すること…
π計算、続きます。と言っても、ここ読んで、一部Haskellで書いてみましたっていうだけ。 動作をちゃんと追ってないからなんで動くのかわからない←
π計算というものがある。 パイ計算というのは、並列計算のモデルで、言わばラムダ計算の並列版なのだとか。 で、日本語で書いてあるページがちょっと前まで探しても見つからなかったけど、 最近は結構検索上位にでも上がってきたのか、1ページ目にまで上がっ…
戸次大介という人の数理論理学という本の第二部第7章のヒルベルト証明論のところの練習問題。 「BCWB'C*がいずれもSKの定理であることを証明せよ」 とりあえずBだけできた。 1. (φ→(ψ→χ))→((φ→ψ)→(φ→χ)) : S 2. (φ→(ψ→χ))→((φ→ψ)→(φ→χ))→((ψ→χ)→((φ→(ψ→χ))→(…
あしたあたりにでもVisualStudion2012でLLVMをコンパイルしてみようかね。
数学とかの本を読むのはいいんだけれど、数式書くのが面倒くさい。 MathmaticaのStudent版を買ってしまおうか…
C#、特にWPFの話。 XmlDataProviderに設定するXMLファイルにスキーマを設定してると、 バリデーションに引っかかってる要素はバインドできないらしい。 xmlnsを外したらバインドできた。
jekllをC#で書き直せないかなと画策中。 コンフィグやオプションの扱いが面倒。 最終的にはGUIで動かすことが目標。 WPFはよく出来てて感動する。
引っ越しして、インターネットが利用可能になりました！！ この半月がとても長く感じられる… そういえば、回線はフレッツで契約したのだけれど、インターネットに接続する時に、CTUという物を設定しなきゃ行けない。 このCTUの設定はctu.fletsnet.comでアク…
英語がすらすら読めないので、LLVM 3.3の、Programmer's Manualの一部を訳してまとめた。 …いや、ほとんどの部分が、ただの訳だ… まとめた、もとい訳した部分は、The Type class and Derived Typesの部分。 LLVMのコアクラス 定義: include/llvm 宣言: lib/V…
Wikipediaを見て、これ以降に学ぶ必要があるだろう論理学の分野についてまとめた。 様相論理 ～でなければならない、～でありうる、～べきである、といった、 可能性や必然性に関わる命題を扱う論理 時相論理 時間との関連で問題を理解し表現するための規則…
C++では、定数マクロの代わりにconstを使おう！ってのがあるけれど、じゃあ関数マクロの方はどうするのかと思ったら、inline関数を使おうってのがあるんだね… 定数マクロの代わりにインライン関数を使えば、想定外の動きをしたり、コードが読みにくくなるの…
同居していた姉の卒業に伴って引っ越した。 さぁ早速インターネットを申し込もう！とおもったら、まさかの「機器がいっぱいいっぱいで、増設に３ヶ月ほどかかりますが…」。 やってられるかー！！！ 明日にでも（文句言うところが違うかもしれないが、）仲介…
顛末： LLVMでコンパイラつくってみたいな パーサとかめんどい パーサジェネレーターとかないかな…ついでにrubyとかで扱えるといいな ruby-llvm発見→紹介してたサイトのコードをダウンロードして実k…gemがないだと… bundle install →エラー：bundleがみつか…
統語論って何って話は、自分なりの理解を統語論と意味論ってなんなのかってのを以前書いた。（間違ってるかもしれんが仕方ない。） 今日はこの統語論について読んだ内容を書いて行こうと思う。 論理式に使われる記号 証明に表れる命題は、記号論理学では論理…
Rakefileの書き方のメモとか書こうと思ってたけど、面倒臭くなったので、これを書く。 ３記事/dayへの道は遠い… という訳で、今年度中にやっておきたいこと、もとい、勉強しておきたいこと。 数学基礎論について本を読み、理解する 型理論とかモデル理論とか…
もしかして、LLVM IRのBasicBlockが空行区切りで分割されてしまう？ なんかClangで-emit-llvmを指定して出力すると、ラベルが入るところに空行が入っていて、 予想だけれども、brに指定された変数は、自動的に次のBasicBlockのラベルになるのではないだろう…
今週末に引っ越しをする。 そこで今日（昨日）はバイトから帰ってきてから荷造りというか、荷物の整理をした。 これまで買ってきた本がそれなりにあるのだけれど、それで段ボールが４箱ほどいっぱいになった。 この段ボール、多分一回り大きかったら、持てな…
Twitterなどをどう使うべきかを考えてみたというだけの話。 1.Twitterの場合 Twitterは、なんとなく思いついたことをつぶやくようにしようとおもう。 つまりブレインストーミングてきな。 あるいは誰かがリプライで助言をしてくれるかもしれないし、 TL上に…
ニコニコ大百科の論理学のページを見て、統語論と意味論というものについて、初めて理解できた気がする。 統語論と意味論 何が論理式や推論であるのかを決める規則が統語論、推論が妥当かどうかを決める規則が意味論だそうな。 ニコニコ大百科の論理学のペー…
タイトルの通り。 数理論理学って何をするの？って話を自分なりにまとめてみた。 あくまで個人の理解なので、間違ってるかもしれない。 数理論理学の目的と記号論理学の方法 数学の証明の妥当性は、数学的な訓練を受けた人であれば直感的に判断できる。 論理…
