天泣記

2022-11-26 (Sat)

#1 クロージャを作る

「クロージャを作る」というのは英語だと closure creation なのか、 closure generation なのか、 closure allocation なのか、 どれが一般的なのかなぁ、と思って検索すると、 closure creation が多いようだ

うぅむ、クロージャを作るというのは (メモリに必要な情報を格納するというのは) そこまでクリエイティブな感じはしないのだが、そうなのかぁ

2022-10-31 (Mon)

#1 Coq 8.16.0

Coq 8.16.0 では、以前報告した、 Coq Issue #7061: OCaml extraction can generate infinite recursion という問題が直っているようだ

これで、たぶん、(再度) strong normalization になったと思うのだが...

2022-09-12 (Mon)

#1 LaTeX の minted で、listings の literate 相当のことを行う

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

2022-08-31 (Wed)

#1 Coq の Coinduction は subject reduction でない

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 でない)、というようなものに変わるようだ

2022-07-28 (Thu)

#1 Coq の Template polymorphism (2)

さらに 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 に対して実装が拡張されている?

2022-07-26 (Tue)

#1 Coq の Template polymorphism

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 が直っていないという感じか?

2022-06-08 (Wed)

#1 ounit issue

GitHub gildor478/ounit/issues/93: assert_command foutput of OUnit 2.2.6



田中哲