「クロージャを作る」というのは英語だと closure creation なのか、 closure generation なのか、 closure allocation なのか、 どれが一般的なのかなぁ、と思って検索すると、 closure creation が多いようだ
うぅむ、クロージャを作るというのは (メモリに必要な情報を格納するというのは) そこまでクリエイティブな感じはしないのだが、そうなのかぁ
Coq 8.16.0 では、以前報告した、 Coq Issue #7061: OCaml extraction can generate infinite recursion という問題が直っているようだ
これで、たぶん、(再度) strong normalization になったと思うのだが...
LaTeX の listings パッケージや minted パッケージはソースコードをハイライト (色付け) したりしてみやすく表示するものである
ここで listings は TeX でぜんぶ実装されているのに対し、minted は pygments という外部ツールを使う (そのため、minted を使うには、latex の実行に -shell-escape オプションが必要になる)
出力は minted のほうがきれいだといわれているようである (たとえば、Ruby の文字列に埋め込む式は、listings では文字列の一部としてハイライトされるけれど、minted では式としてハイライトされる)
ところで、listings には literate という機能があって、文字列を置換することができる。 たとえば、forall という単語を $\forall$ にしたり、-> という ASCII文字の矢印を $\rightarrow$ にしたりできる。 これは出力がコンパクトになるし、数学の記法の矢印の代用として -> を使っているのが正しい文字になるのがよい
残念ながら minted には literate に相当するような機能は提供されていない (と思う)
しかし調べてみると、いくらかがんばれば、literate に相当することを実現できるようだ。 肝心なところは pygments の lexer (RegexLexer) に callback という機能があってソースとは異なる出力を生成できるというところである
まず、pygments は入力する言語を処理するための lexer というものと、 出力を行う formatter というものがいろいろ用意されている
今回は formatter として latex のみを考える
lexer は自分でいじる必要があるので、LaTeX 文書と同じディレクトリで管理したい
pygments にはそういうときのために、カレントディレクトリから lexer を探すという -x オプションがある
では minted で -x を指定するにはどうするかというと、普通は lexer の名前を書くところに mylexer.py -x というように書けばいいようだ (ひどい)
\begin{minted}[escapeinside=@@]{mylexer.py -x}
...
\end{minted}
なお、ここの escapeinside=@@ というオプションは、@...@ の内側は LaTeX として扱うという指定で、 mylexer.py が生成する中で @...@ という出力を使うためである
まぁ、毎回こう書くのはつらいので、\newminted と \newmintinline で shortcut を定義しておけばいいだろう (ファイルから読み込む \newmintedfile もやってもいいかもしれない)
\newminted[mycode]{mylexer.py -x}{escapeinside=@@}
\newmintinline[mycodeinline]{mylexer.py -x}{escapeinside=@@}
\begin{mycode}
...
\end{mycode}
\mycodeinline|...|
で、mylexer.py を用意する。 おそらく、ふつうは対象の言語の lexer をもとにカスタマイズするのだろうが、 今回は literate 相当のことをする説明のために、それだけを行うものとした
# -*- coding: utf-8 -*-
import re
from pygments.lexer import RegexLexer, words
from pygments.token import Text, Operator, Keyword
__all__ = [' CustomLexer ']
class CustomLexer (RegexLexer):
literate_keyword = {
'forall' : '@\\ensuremath{\\forall}@'
}
literate_operator = {
'->' : '@\\ensuremath{\\rightarrow}@',
'=>' : '@\\ensuremath{\\Rightarrow}@',
}
def literate_keyword_callback(lexer, match):
yield match.start(), Keyword, lexer.literate_keyword[match.group(0)]
def literate_operator_callback(lexer, match):
yield match.start(), Operator, lexer.literate_operator[match.group(0)]
tokens = {
'root': [
(words(list(literate_keyword), prefix=r'\b', suffix=r'\b'),
literate_keyword_callback),
(r'(%s)' % '|'.join(list(literate_operator)[::-1]),
literate_operator_callback),
(r'.', Text),
],
}
重要なのは、literate_keyword_callback (や literate_operator_callback) で、 ソースでマッチした match とは異なる文字列を yield している、というところである
ここでは、ソースの forall に対して @\ensuremath{\forall}@ を、-> に対して @\ensuremath{\rightarrow}@ を、=> に対して @\ensuremath{\Rightarrow}@ を、 生成している
(生成するところが数式モードでもそうでなくても、\ensuremath により \forall, \rightarrow, \Rightarrow は数式モードとして扱われる)
そうすると、LaTeX の出力では ∀ などと表示される
たとえば、以下の例を処理できる
t.tex:
\documentclass{article}
\usepackage{minted}
\newminted[mycode]{mylexer.py -x}{escapeinside=@@}
\newmintinline[mycodeinline]{mylexer.py -x}{escapeinside=@@}
\begin{document}
\begin{mycode}
nat -> nat.
forall (T:Type), list T -> nat.
\end{mycode}
foo \mycodeinline|nat -> nat, forall (T:Type), list T -> nat| bar
\end{document}
PDF生成:
pdflatex -shell-escape t.tex
Coq の manual に、 Coq の (positive) coinductive type は subject reduction を壊す、 と書いてある
Coq reference manual, Coinductive types and corecursive functions, Caveat
subject reduction というのは、たしか、reduction を行っても (計算が進んでも) 型が変わらない、という性質である
具体例は載っていないのだが気になって検索してみると、以下を見つけた
Towards a fix to the loss of subject reduction with corecursion?
あまりよくわかっていないが、ぜんぜん違う型に変わってしまうわけではなく、 等しいことを証明できるけれど、型検査器が見抜けるほどには等しくない (convertible でない)、というようなものに変わるようだ
さらに manual を読み直した
そーか、具体的に与えた ql から Pl' が決まり、Ci : sqi を成立できるように si が選ばれる、 という仕掛けか
そこで ΓP' は、partial application で ql が与えられなかった部分はそのまま残るから別にいいのか
ということは manual も実装も問題ない、のかな
いや、以下の例では変?
Inductive I (A B : Type) : Type :=
| C1 : A -> B -> I A B
| C2 : I A (B * B) -> I A B.
Check (fun (A : Set) (B : Set) => I A B).
(*
fun A B : Set => I A B
: Set -> Set -> Set
*)
B は recursively non-uniform parameters なので、 Ind-Family の中で B は扱われず、 ΓP' の中で B は Type として扱われ、 C1 : A -> B -> I A B で B が Type なので A -> B -> I A B は Type となる、 はずなのに、Set になっている、と思う
manual に対して実装が拡張されている?
Coq 8.15.2 の manual の Template polymorphism のところを 読んでいて疑問に思ったのだが、なんか Ind-Family の規則が、partial application に対応しているようなのだが、 実装はそうなっていない気がする
Coq 8.15.2, Template polymorphism
ふと思いついて、古い manual を見てみると、 Template polymorphism が入った当初の 8.1 でだけ、(fun A:Set => prod A) という例の結果が異なるようだ
Coq 8.1pl4 の manual:
Coq < Check (fun A:Set => prod A).
fun A : Set => prod A
: Set -> Type -> Set
Coq 8.2pl2 の manual:
Coq < Check (fun A:Set => prod A).
fun A : Set => prod A
: Set -> Type -> Type
prod は 2引数で、引数を 1つしか与えていない prod A は partial application なのだが、 これの型が Type -> Set になるか Type -> Type になるかが異なる
なんとなく、prod A B で、A が Set であっても B が Type だったら prod A B を Set にするのはまずいような気がするので、 実装が正しい、のかなぁ。 実装を直したけれど manual が直っていないという感じか?