読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

minecraft 1.11 MOD開発メモ

1.11準拠のMOD開発に関するメモ 詳しいことは自力で調べてね的なスタンス 概要 proxyを用意して、common proxy側にMOD本体の処理、client proxyに描画関係の処理をかくようにする ゲーム内のオブジェクトの管理はすべてナントカregistryがやってくれてる だいた…

自作PC組んだよ2017

構成は次の通り niku.webcrow.jp 自分で使うPCを自作したのは初めてだったので色々調べながらパーツを選んだ。 一応個人的な選定基準とかを書いておく。 用途は、主に開発・たまにコンパイルとか動画編集・たまーーーにゲーム とか色々。 パーツ選び CPU Cor…

凝りたいけど凝りたくない妥協デスクトップLinux環境

今のデスクトップLinuxの環境をまとめておこうと思った。 新しいPC買った時に見る用ということで。 できればどんどんより良く設定していきたいので、またこの時点から色々変わってきたら新しく記事を書こうと思います。 (少なくともこの記事を書き換えること…

ペンタブを買った

追記 DIGImendを公式からパッケージを落として入れたら何かと競合したみたいで ペンタブが一切認識されなくなった。 sudo rmmod hid_uclogic && sudo insmod /lib/modules/$(uname -r)/kernel/drivers/hid/hid-uclogic.ko で直ったけど、USB挿して動くならDI…

2016年のまとめ

もうすぐ2016年も終わるので今年したこととかをまとめる。 研究・勉強 割とずっとtyped lambda calculusのsyntaxやらsemanticsやらやってた気がする。 Proof Assistantももう少し調べなきゃなーと思いながらあんまり欲しい結果を出してる論文とかもないしこ…

Recursive Typeの実装

前回はsimply-typedの拡張としてλμを実装したけれど、 今回はsimply-typedにrecursive typeを実装してみた。 recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。 recursive typeはType ->…

λμのTypeCheckerの実装

λμのtypecheckerを実装したので (ソースコードは参考文献[3]を参照) λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。 syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。 型なしの項を受け取って、それにうまく型をつ…

依存型による定理証明Tips: coherenceは型で表せ

この記事はTheorem Prover Advent Calendar 2016 12日目の記事です。 この記事は定理証明初心者向けの記事です。 普段から依存型を用いた定理証明をされている方は読む必要がありません。 "coherence condition"と呼ばれる条件があり、訳すと「一貫性条件」…

鬱モード全開だったときに

今から大体3年くらい前の、大学学部2回生の頃に唐突に精神が死んだことがあった。 という話をするけど、この先読んでも特にオチはありません。 ただの身の上話なので。 非常に運がよかったため自分は3回生の進路振り分け的なものに必要な単位を前期で全て揃…

Theorem Prover Haskellの紹介

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。 今年も残り1ヶ月になったことを信じたくないと思いつつ、 まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。 今回のアドベントカレンダーのネタを必死に1週間くらい前から…

Programming in Scalaを読んでいる時のメモ

Programming in Scala: A Comprehensive Step-by-Step Guide, Third Edition (English Edition)作者: Martin Odersky,Lex Spoon,Bill Venners出版社/メーカー: Artima Press発売日: 2016/04/27メディア: Kindle版この商品を含むブログを見る を読んでいる時…

λ→のtyping & unification algorithm

この記事のunification algorithmは間違っているので λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください λ→のtypingアルゴリズム. variableとabstractionは型が一意に決まるので, 問題はapplication. MN:aからM:?x -> aの?xをどうやって決定す…

tmuxからのpowerlineで優勝せえへん?

メモです. 現状イマイチなところがありありなのでどうにかしたい. 環境 以下に同じ端末環境を作りたかった. Ubuntu 16.04 Mac OS X El Capitan Debian jessie (Mac上のVM環境) zsh zshを入れてデフォルトのshellをzshにする. prezto github.com を入れる. 入…

React ComponentにImmutable.jsは(多分)だめ

github.com ここにもはっきり書いてあるように, Note that state must be a plain JS object, and not an Immutable collection, because React's setState API expects an object literal and will merge it (Object.assign) with the previous state. Reac…

variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com の続き. いくつか疑問が解消されたのでそれについて. var-free type theoryについて syntaxはcontext, type, term, substからなる. contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtype…

データ型のCPS変換について

HaskellでCPS変換とか調べているとデータ型のCPS変換というのが出てくる. 関数のCPS変換は継続を引数に追加して末尾再帰の形にすればだいたいOKなのでまあわかるのだけど, データ型のCPS変換というのは何なんだという話. 継続は何を継続しているのかがいまい…

type theory with variable-free syntax

(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox -- 文献に突然登場して?ってなったので. 調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい. で…

CoC7th キャラクターシート(印刷用)

CoC7用にキャラシを作った. 表面のみ. png: pdf: CoC7th キャラクターシート

Coinductiveのintro rule

Type Theory & Functional Programmingに出てきたCoinductive typeのintro ruleに少し悩んだので. Coinductiveは最大不動点の形でかけるような型. 例えばStream(無限リスト)はP X = N × Xの時のPの最大不動点である. テキストにはCoinductiveのintro規則と計…

AviUtlスクリプト 「自由落下と衝突」 v1.0

この前MAD動画を作るのに作ったAviUtl用のアニメーション効果を公開 概要 上からオブジェクトが落ちてきて, 地面に衝突して跳ね返る動きを実現します. オブジェクトの位置(Y座標)が地面の高さに対応. パラメータについて 加速度: 重力加速度. 落下にかかる時…

Theorem Prover Leanの紹介

Microsoftが開発したTheorem Prover Leanを紹介します. 特徴 他の言語と軽く比較する. あくまで個人的な感想です. Lean Coq*1 Agda Isabelle 証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic 開発環境 emacs ema…

オートマトンで遊ぶやつを作った

この記事はHaskell Advent Calendar 2015 18日目の記事です. Automatoy(オートマトン)で遊ぶやつを作ったので紹介します. github.com ブラウザで遊べる. 以下それっぽい解説. Automatoyについて http://myuon.github.io/automatoy/ "Def"タブでオートマトン…

『ふたりのハードプロブレム』 感想

ncode.syosetu.com 以下, ネタバレ注意. ジャンルとしてはSFでしょうが, 話自体は人間ドラマに重きが置かれているという印象でした. 登場人物がみんな感情豊かで人間臭いのがまた良いところ. あまりあらすじ等を確認していなかったので, 前情報なしだといい…

『Normalize Human Communication のまひゅ』 感想

http://mukiryokukan.sakura.ne.jp/NormalizeHumanCommunication.htm以下, ネタバレ注意.ずっと前から友人から勧められていたのでやりました. プレイしてから多少時間が空いてしまったので記憶が少し曖昧ですが感想を述べることに. 一言で言うと「緩やかな死…

ノベルゲーム「人形劇が終わる夜」をリリースした

もう2週間近く前ですがノベルゲームをリリースしました.www.freem.ne.jp反省会を兼ねてその話. 企画 前のノベルゲームをリリースしたのが2年近く前ということもあり, そろそろなんとなくノベルゲーム作りたいなと思ったこと. 諸般の事情で現実逃避先として「…

ListのT代数の非自明な射は何か?

ListのT代数の非自明な射は何か?という感じの話. List Monad, T-Algebra 以下のようなmonoid free functorとforgetful functorの随伴がある: free functorは集合を自由モノイド(wordの集合, 演算は結合)に飛ばし, forgetful functorはモノイドを底集合に飛…

ノベルゲームシナリオ論

※ 以下は全て個人の感想です。 長さは「正義」 長いゲームは飽きられやすいけれど、その点さえ解決できれば長さは完全に正義である。 長時間プレイしてくれたプレイヤーは大抵どのキャラにも相応の愛着が沸いているので、キャラクターらしささえ損なわなけれ…

Monadic functor(後で調べる)

$G : \mathcal{C} \to \mathcal{D}$がmonadic functorということは、圏同値の差を無視してforgetful T-algebra functor $G ^ T : \mathcal{C}^T \to \mathcal{C}$と同じだと思えるってことだ. ここから何か分かったりしないんだろうか.

MonadPlusとNearSemiringで反例探し

"MonadPlusは単なる自己関手の圏における近半環だよ。何か問題でも" の理解を試みる - scalaとか・・・d.hatena.ne.jp 上の記事を読んでちょっと考えたこととかをまとめる. NearSemiringとは和についてモノイド, 積について半群で, 0が左吸収元で…

Haskellで大富豪を作ろう (5)勝敗の判定をしよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox Haskellで大富豪を作ろう (3)カードの組を判定しよう - Just $ A sandbox Haskellで大富豪…

Haskellで大富豪を作ろう (4)基本のルールと場の流れを作ろう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox Haskellで大富豪を作ろう (3)カードの組を判定しよう - Just $ A sandbox 第四回 基本のル…

Haskellで大富豪を作ろう (2)ターンを進めよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox 第ニ回 ターンを進めよう 実際にゲームとして動かすために, まずはいわゆるメインループにあたる部分を作ろう. ゲームに必要な変数をGame型として定義してお…

Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう

まえがき Haskellでなんか動くものを作ろうと思った. 規模と知名度等を考えて大富豪あたりが妥当なところかと思ったので, 今回はCUIの大富豪を作ろうということにした*1. コード自体は完成しているので, 何回かに記事を分けて説明をつけて投稿していくつもり…

Haskellで大富豪を作ろう (3)カードの組を判定しよう

前回までの記事 Haskellで大富豪を作ろう (1)トランプを用意しカードを配ろう - Just $ A sandbox Haskellで大富豪を作ろう (2)ターンを進めよう - Just $ A sandbox 第三回 カードの組を判定しよう 前回はカードを捨てられるようになったので, 次は同じ数字…

Lens from Scratch

久しぶりのLensの記事です. 5億回は繰り返されてきたであろうLens再実装を通して, Lens, Getter, Setter, Iso, Equality, Traversal, Prism, Foldの仕組みを理解するのが目的です. 亜Lens family Getter Getterは基本的にはConstをかぶせる操作とそれを剥が…

無限ループによる証明

Software FoundationsのIMPあたりをやってて疑問が湧いた. w = while True do Skip endが停止しないことを示したい. つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)…

de Bruijn Indexとβ変換

$ KMN \equiv (\lambda xy. x)MN \longrightarrow_{\beta} M $を示したいとする. α変換 $y \notin \text{FV}(M)$ならば, $ (\lambda xy. x)MN \to (\lambda y. M) N \to M[y:=N] \equiv M $となる. 問題は$y \notin \text{FV}(M)$ならば$ M[y:=N] \equiv M $…

原始帰納的函数で素数を計算

原始帰納的函数; 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の戦闘システムについて(アイデア)

概要 RPGの戦闘システムとして考えたやつ。戦闘は普通のターン制。各ターンに1つのアクションが取れる(攻撃・防御・回復 など)。 プレイヤーは戦闘の前に、アクションを並べて作った列をスロットという形で保存しておく。 敵との戦闘時、プレイヤーの作った…

DataKindsとGADTの使い方について

Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある. {-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero…

ワンナイト人狼の基本戦略

ワンナイト人狼とは ワンナイト人狼は一夜で決着が着く人狼(ジャンルとしては多人数推理ゲーム)。 ワンナイト人狼のルール ゲームは3~5人向けだが、今回は4人でプレイするとして解説をする。 初めに6枚のカードを用意する。 内訳は「人狼2枚、村人2枚、占い…

Linuxで音声読み上げ

ゆっくりしていってね! 棒読みちゃん 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に関するエラ…

Grothendieck群とBurnside環の定義

局所有限トポス上の離散数学の構築を目指して という論文で、Burnside環という環を扱っていた.定義は「局所有限トポスの同型類から得られるGrothendieck ring」らしく, これではよく分からなかったので調べた. Grothendieck群 Grothendieck群は可換モノイド…

美少女と学ぶ圏論(2)

本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします. 1.2 SpecialなObjectたち レポートをやるというのは話を切り上げ…

美少女と学ぶ圏論

ここまで書いて飽きました. 1章 圏とその構造 1.1 圏の定義と千景の講義 「4月からのゼミはもう決めた?」「うん. とりあえず,クラスの子とホモロジー代数ゼミをやろうと思ってるよ. 春休みのうちに予習を進めないと」「ふぅん,ホモロジー代数ね」 千景は読…

objective覚書

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 Monad

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…

Agdaで集合論をやろうとして上手く行かなかった

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した. 写像の定義を _⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる. x ∈ A を像の方に押し込めて _⟶…

矛盾の証明

矛盾を示すときに使える方法としては主に以下の2つだと思う 命題 ¬P に P をぶつける 矛盾 ⊥ の特徴付けを使う 矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから, 空集合の公理がそのまま矛盾の特徴付けになる. ∃ \(A : Se…

Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。 標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているよ…