日々の流転

λ. Infinite Objects in Type Theory. Thierry Coquand.

を読んだ。 guarded induction についての多分最初の論文。

どうでも良いけど、表記が少し珍しい気がする。 普通「f : (N -> P) -> P」と書くところを「f : ((N)P)P」と書き、「λx.u」と書くところを「[x]u」と書いている。

【2007-09-11追記】 「[x]u」は「自由変数としてxを含む項u」という意味だろうし、「((N)P)P」についても同様だろう。 なので、上記部分は私の勘違いだろうと思う。

Quotation

In order to establish that a proposition φ follows from other propositions φ₁,...,φ_q, it is enough to build a proof term e for it, using not only natural deduction, case analysis, and already proven lemmas, but also using the proposition we want to prove recursively, provided such a recursive call is guarded by introduction rules. We call this proof principle the “guarded induction principle”.

sec. 2.8 より。 Guarded Induction on Final Coalgebras で引用されていたのと同じところを引用するのは、ちょっと癪だけど。

分からなかった点など

impredicative proof of Tarski's fixed point theorem.

Tarskiの不動点定理について良く知らないことに気づいた。どの辺りがimpredicativeなんだろう... <URL:http://www.hss.caltech.edu/~fede/wp/pf-tarski4.pdf> とかは関係ある?

strong positivity

P.Dybjer. Inductive Families. を参照。