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

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

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

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

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

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

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版この商品を含むブログを見る を読んでいる時…

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

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

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…

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

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

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

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

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

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

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