Ikegami Daisuke ikedaisuke

Search lemma on the fly in ProofGeneral

A helm extension for Search command.

/disambiguation/

Emacs の git クライアント magit の個人的なまとめです。正確かどうかは保証しません。

こんな cheat sheet を参照するくらいなら magit の公式ドキュメント読んだほうがいいと思う。

git

みなさん、こんにちは、「発表者」です。この番組ではリスナーの皆さんに「定理証明」の話題をお届けいたします。たぶん、今回が最初で最後だと思います。

これから15分ほどの間、お付き合いくださいませ。

それではさっそくメールを読み上げていきたいと思います。ラジオネーム「とあるHaskell golfer」さんから質問をいただきました。

説明はあとで（適当に）します。このファイルを protocol.pml という名前で保存して、次の手順を踏みます：

> spin -a protocol.pml
> gcc pan.c
> ./a.out
> spin -M -t protocol.pml

以上で protocol.pml.ps という PostScript ファイルができあがります。

	;; How to use:
	;; impatient-mode
	;; M-x imp-set-user-filter
	;; markdown-filter
	;; see also https://github.com/skeeto/impatient-mode
	(defun markdown-filter (buffer)
	"Render a markdown document on your browser in real time by impatient-mode and markdown-mode."
	(princ
	(with-temp-buffer
	(let ((tempname (buffer-name)))

	Real world (functional) programming with dependent types!
	---------------------------------------------------------
	* we want to write a program with /dependent types/
	* shallow embedding vs. deep embedding
	* we want to prove some properties of each part of the program
	* we need reasoning about programs
	* especially, a program will run correctly
	* interactiton with I/O
	* mutable state
	* etc.

	; try the following code at http://rise4fun.com/z3/tutorial
	; data type Nat
	(declare-datatypes () ((Nat zero (succ (pred Nat)))))
	; plus as a rule
	(declare-fun plus (Nat Nat Nat) Bool)
	; rule P-Zero
	(assert (forall ((n Nat)) (plus zero n n)))
	; rule P-succ
	(assert (forall ((m Nat) (n Nat) (r Nat))
	(=> (plus m n r) (plus (succ m) n (succ r)))))

	# Current Trends on Gröbner Bases 関連文書まとめ

	The 8th Mathematical Society of Japan Seasonal Institute
	Current Trends on Gröbner Bases
	— The 50th Anniversary of Gröbner Bases —

	July 1 - July 10, 2015

	http://www.math.sci.osaka-u.ac.jp/~msj-si-2015/index.html

	Ruby の Array は関数型プログラミングの List とは違います。

	が、Ruby 1.8.7 以上で Enumerable は大きく変わりました。
	その結果、関数型プログラミングの文脈における List のかなりのことが、
	短いプログラム断片で書けるようになったと理解しています。

	関数型プログラミングでは、さらに List を抽象化できます。
	その一つが Rose tree [Bird 1998] です。

	Ruby でも、このような抽象化があれば役にたつと思います。