原始帰納的函数; prf 原始帰納的函数(primitive recursive function; prf)とは, 以下で定義される函数 $ \mathbb{N}^n \to \mathbb{N} $ のこと: 定数函数 $zero : \mathbb{N}^0 \to \mathbb{N}$, 後続函数 $suc : \mathbb{N} \to \mathbb{N}$, 射影函数 $p^…
概要 RPGの戦闘システムとして考えたやつ。戦闘は普通のターン制。各ターンに1つのアクションが取れる(攻撃・防御・回復 など)。 プレイヤーは戦闘の前に、アクションを並べて作った列をスロットという形で保存しておく。 敵との戦闘時、プレイヤーの作った…
Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero…
ワンナイト人狼とは ワンナイト人狼は一夜で決着が着く人狼(ジャンルとしては多人数推理ゲーム)。 ワンナイト人狼のルール ゲームは3~5人向けだが、今回は4人でプレイするとして解説をする。 初めに6枚のカードを用意する。 内訳は「人狼2枚、村人2枚、占い…
ゆっくりしていってね！ 棒読みちゃん http://chi.usamimi.info/Program/Application/BouyomiChan/ 環境はwine 1.6.2, Bouyomichan 0.1.11.0 (beta 16) wineを32bit環境で動かすことと、.NET framworkをwinetricksで入れておくこと mscoree.dllに関するエラ…
局所有限トポス上の離散数学の構築を目指して という論文で、Burnside環という環を扱っていた.定義は「局所有限トポスの同型類から得られるGrothendieck ring」らしく, これではよく分からなかったので調べた. Grothendieck群 Grothendieck群は可換モノイド…
本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします. 1.2 SpecialなObjectたち レポートをやるというのは話を切り上げ…
ここまで書いて飽きました. 1章 圏とその構造 1.1 圏の定義と千景の講義 「4月からのゼミはもう決めた？」「うん. とりあえず,クラスの子とホモロジー代数ゼミをやろうと思ってるよ. 春休みのうちに予習を進めないと」「ふぅん,ホモロジー代数ね」 千景は読…
objective-0.6.1 O' = data Object e m = forall x. e x -> m (x, Object e m) = hom(e, m . (-,O')) (as Nat) functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ) O' = hom(hom(a,K-), m . (-,O')) = hom(K^-1(…
Codensity という型がある. 定義は以下. newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b } instance Functor (Codensity k) where fmap f (Codensity m) = Codensity (\k -> m (k . f)) instance Monad (Codensity f) wh…
この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した. 写像の定義を _⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる. x ∈ A を像の方に押し込めて _⟶…
矛盾を示すときに使える方法としては主に以下の2つだと思う 命題 ¬P に P をぶつける 矛盾 ⊥ の特徴付けを使う 矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから, 空集合の公理がそのまま矛盾の特徴付けになる. ∃ \(A : Se…
Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。 標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているよ…
問題 問. Haskellで以下のようなCライクなprintf函数を実装してください。 > printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] -- 出力結果: > Hello, World! > an integer:10 > a float…
Lensにほとんど触れたことのない人にはこちらの記事がオススメです：Lensで行こう！ - Just $ A sandbox Haskellでもオブジェクト指向をしましょう！ Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェク…
発端 ノベルゲームやりたいし誰か作ろう— いるたん (@t_iru) 2013, 9月 8 【告知】フリーノベルゲーム「チェイン・コンプレックス」を公開しました。 http://t.co/JcLhaqfAKs http://t.co/3fJcNInJlj— いるたん (@t_iru) 2013, 11月 13 で2ヶ月くらいでノベ…
Xubuntu 13.10で以下のようなエラーが出て起動できませんでした。 The disk drive for /home is not ready yes or not present. 私のHDDのパーティションは以下のような感じになっています。 /dev/sda2 /dev/sda7 /dev/sda5 Windows7 /home / /homeに当たる/…
この記事はwineに関して私が蓄積したベストプラクティスとバッドノウハウをまとめたものです。 Wineとは Wineとは、Linuxで*1Windowsアプリケーションが動くエミュレータではない何か*2です。 はじめに、Wineで全てのWindowsアプリが動くわけではないことを…
[追記:2013/11/02] この記事ではPython2.xを前提としていますが、Python3以降はsuperの引数を省略することができるようになっています。 [/追記] 次のPythonコードを見てください。 class A(object): def method(self): pass class B(A): def method(self): …
Best written projects on Python GitHub? redditで面白いポストをみつけたので日本語で軽くまとめておきます。 http://www.reddit.com/r/Python/comments/1ls7vq/best_written_projects_on_python_github/ エレガントで上手に書かれていて読みやすく練習に…
PythonでXML(HTML)を扱う高速で便利なライブラリがlxmlです。 非常に強力なメソッドが多数用意されているのですが、日本語の情報があまりないのが弱点です。なので今回、lxml.etree公式チュートリアルの一部を勝手に翻訳しました。 量が多いので全ては訳しき…
ubuntuを使っていたら突然音が出なくなりました。 結論から言うとpulseaudioとflashplugin-nonfree-extrasoundをインストールしなおしただけです。 環境 OS: ubuntu 12.04 LTS 問題のあったGoogle Chrome: version 28 経緯 最近Google Chromeで``Shockwave F…
はじめに：モナドが何かわからないけど分かりたい人へ この記事はあなたの為に書かれたものです！ 「モナドって難しいそうだしよく分からない、けどきっと賢い人たちが『モナドとは何か』について素敵な説明を与えてくれるはず！」 …そういう期待を持ってい…
は環 はアーベル群 , として、 はAbel圏でモナドを定め、T-代数は左加群になる*1。 *1:これよりわかりやすい例があれば教えて下さい
最近Haskellerの間で人気になりつつある(？)Operational Monadというものについての記事です。 サンプルプログラム Operational Monadは http://hackage.haskell.org/package/free-operational で定義されています。後でも説明しますがこれはFree Monadの構…
PSh圏とcolimit 位相空間Xに対して、X上の前層Fとは、Xの開集合から集合への写像 (で、かつ制限写像というものが定められているものの)のことです(詳しくは層 (数学) - Wikipedia等を参照)。 ここで、に包含関係で順序を入れてこれを順序集合の圏(と表記)と…
Haskellで時々Formatがしたくなる時があります。 しかしこれと言って便利そうなものが見当たらず、自作しました。 myuon/FuncFormat · GitHub import Text.FuncFormatとすれば使えるようになります*1。 ほんの少しだけTemplateHaskellの闇魔術を利用している…
abstract: this article shows how to install and run Yesod, a famous Haskell web framework for its simplicity to use and its difficulty to install. I wrote how I did it for whoever wants to install Yesod, and for myself. Yesodのインストール…
はてなブログにはいくつかテーマが選択できて、個人的には2カラムのテーマが好きなので一番シンプルなEpicというテーマを使っています。 しかしこのテーマ、横幅が短すぎるのです。プログラム関係の記事が多いためコードをよく掲載するのですが、ちょっと長…
LaTeX環境構築の話です。 Linuxだと最初から入ってるもの・入ってないからいれなきゃいけないもの(apt-getできるもの・install-elispできるもの・ソースから落としてビルドするもの)が混在しているためか環境構築はかなり面倒です(面倒でした)。 同じ思いを…
