Just $ A sandbox

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

依存型による定理証明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 $…