プログラミングにおける〈式〉についての考察

「プログラムとは何か」という質問に対する、最も素朴な回答は「プログラムとは、機械に与える命令文の並びのことです」というものだ。命令文を解釈する機械が、プログラムに記された命令に従って、装置を制御し、計算処理を実行する。このようなことは、情報科学の基礎として学校で教えていると思う。

一方で、今日の高水準言語によるプログラミングでは、〈式〉という概念を理解していることがとても重要だ。特に、関数型プログラミングが注目されるようになった今日では、もはや単なる数式としての理解では十分でない。

しかし、プログラミング言語における〈式〉は〈サブルーチン〉や〈関数〉のような概念に比べると自明であるように思われているためか、あまり精緻な説明がなされないようだ。実際、Wikipediaにおける式 (プログラミング) - Wikipediaの記述の短さを見て欲しい。英語版であれば少しだけ記述が長いが、それでも十分な記述には程遠いものだろう。

プログラミングにおける〈式〉は、もっと語られてもいいはずだ。以下では、プログラミングにおける〈式〉の概念について、いくらか考察してみる。

プログラミング・パラダイムにおける式の観点の違い(概論)

以下、各プログラミング・パラダイムにおいて、式がどのような働きをしているかを考察する。各用語は、簡単な表現で説明できるように再定義しているため、巷での用法とは必ずしも一致しないことに注意を要する。「論理型プログラミング」や「関数型プログラミング」といった用語が、巷ではどのような意味で使われているかというのも興味深い話ではあるが、ここではその議論をしない。

命令型プログラミングにおける式

命令型プログラミングとは、〈プログラムとは命令文の並び〉という観点から行われるプログラミングのことだ。命令文を解釈する機械に命令を与えると、そのとおりに順次処理していくから、計算の仔細な手順(狭義のアルゴリズム)を、命令列によって与えれば、機械に計算を行わせることができる。

しかし、人間は大抵の場合、数学的な概念や計算を数式の形で記述ている。そのような数式を人間の手でアルゴリズムに変換するのは煩わしい。数式を与えると、その式の値を計算してくれる〈評価プログラム〉や、数式を与えると、その式の値を計算するための命令列を出力してくれる〈翻訳プログラム〉があると、楽で良い。〈プログラムとは命令文の並び〉という観点のプログラミング言語でも、高水準言語は当然のように〈数式〉を持っている。FORTRANの名の由来も「数式翻訳」“formula translation” だ。(FORTRAN - Wikipedia

命令型プログラミングにおける式は、ポピュラーな数学におけるような、計算して値を求めるための数式だろう。

論理型プログラミングにおける式

命令型プログラミングが〈プログラムとは命令文の並び〉という観点でプログラムするが、論理型プログラミングは〈プログラムとは平叙文の集まり〉という観点でプログラムする。平叙文というのは、「今年の平均気温は昨年より1度高かった」だとか「晴れている日に軒先に何か洗濯物を吊るしておくと、その洗濯物は乾く」のような、世界に関する事実や法則を表現する文だ。これを論理式の形で表現したものを、表明 (assertion) という。

命令型プログラミングによるプログラムの実行方法は、ただ「実行せよ」という命令であるのに対し、論理型プログラミングによるプログラムは、疑問文の形をとる。たとえば「月曜日の掃除当番は誰ですか」というような疑問を、自由変項 (free variable) という、「誰」や「何」に相当する分からない部分を指す項を含んだ論理式の形で与える。この論理式を、ゴール (goal) という。そうすると、マシンはプログラムされている事実や法則と、数理論理学に基づいた汎用の推論アルゴリズムを使って、ゴールが成り立つような例を見つけ出し、「月曜日の掃除当番は お父さん です」のように疑問に回答するわけだ。

事実と法則を与えておくだけで疑問に答えてくれる、ということが実現できるなら、それは人工知能と呼べるのだけれども、論理型プログラミングで推論がうまくいくのは、ごく限られている場合だけだ。きちんと問題が解けるようにするには、推論アルゴリズムの性質を理解し、適切な形で知識と法則を与えなければならない。だから、論理型プログラミングは、ごく基本的な使い方をする分には難しくないが、高度な使い方をしようとすると、途端に難しくなる。

論理型プログラミングにおける式は、自由変項を含んだ論理式であり、これを充足する解を求めるためのものだ。

関数型プログラミングにおける式

命令型プログラミング、論理型プログラミングを「プログラムとは○○」の形で簡潔に表現してきた。その流れで、関数型プログラミングは〈プログラムとは関数の集まり〉という観点でプログラムすることだと定義する。(繰り返しになるが、世間一般の用法とずれることを厭わず、こう定義している。)

関数は式を抽象したものだ。ここで言う抽象とは、式の可変部分を仮引数 (parameter) によって表すような操作を指す。具体例を挙げると、 10 \times 4 + 2という式があるときに、これを抽象し、f(x, y) = 10 \times x + yという関数を抜き出すことができる。

この関数を使えば、元の式は、関数に実引数 (argument) を指定した f(4, 2)という式で表現できるし、また f(7, 5)という式で 10 \times 7 + 5という式を表現できる。

関数型プログラミングによるプログラムの実行は、関数を含む式の値を計算することだ。ここまでの説明だけでは、関数で複雑なプログラムを書くことが出来るということが想像しがたい。しかし、実践的な関数型プログラミングにおいては、式の値としてポピュラーな数だけではなく、より複雑な構造を持った数学的オブジェクトを扱うので、とても実用的で汎用的なプログラミング・スタイルとなっている。

より一般的な〈式〉概念の説明

ここでは、式とは何かをより包括的に考えられるように、一般的に通用する定義を与え、プログラミング言語における〈式〉概念について考察する。

式 (expression) とは、プログラムのうち、値 (value) を持つ部分を指す。

式の望ましい性質には、次のものがある。(各項目の見出しは、例によってここでの議論における命名であって、一般的な用語とは必ずしも一致しない。)

  • 確定性 (definiteness): 式の値は一意に存在している。
  • 構成性 (compositionality): 式の値は式の構造と部分式の値のみから決定される。
  • 純粋性 (purity): 式は式の値以外の意味を持たない。

確定性があることによって、式の意味が明確に定まる。純粋性と構成性があることによって、部分式を、同じ値を持つ別の式と交換しても、式全体の値や意味が変化しないと言える。このような性質は、式に接している時に暗に了解している性質だ。

しかし、これらの性質を満たしていない式も多く存在している。例えば、 \frac{0}{0}という式の値は不定で、確定性がない。System.currentTimeMillis()という式は評価される時刻によって値が決まるから、構成性がない。System.out.println("Hello")という式は、値以外に〈標準出力へ文字列“Hello”を出力する〉という意味を持ってしまっていて、純粋性がない。

あるプログラミング言語の式が確定性・構成性・純粋性を持たないとしても、式の値の考え方を変えると、これらの性質を持つようになる場合がある。たとえば、「 \frac{0}{0}という式の値は不定」とせず、「 \frac{0}{0}は〈不定値〉という値を持つ」と考えることで、言語の本質的な仕様を変えずとも、式に確定性を持たせることができる。場合によっては、言語全体で式の値についての考え方を大きく変えなければならない場合もあるが、この方法は大抵実践可能だ。更に言えば、文のように元来値を持たないプログラムの構成要素に対しても、値を与えることで式にできる。

文のような、本来値を持っていない構成要素を式にできる、と言われても、抵抗があるだろうと思う。なぜ抵抗があるかというと、文の値を考え、文を式とした場合、言語の本質的な仕様を変えないという前提の下では、本来文だった式とそうでない式との間で、不公平な仕様が残る場合があるからだ。具体的には、もとの言語の仕様が「式の値は変数に代入できるが、文には値がないので代入できない」という仕様であったとすると、文に値を与えたところで、本質的な仕様の変更なしには、文は相変わらず変数に代入可能ではないままだからだ。しかし、「式の値は変数に代入可能であるべきだ」のような、個々の言語において望ましいとされている性質は、ここでは議論せず、まずは上記の3つの性質に絞って議論したいと思う。

つづく。

Everybody Loves Somebody

述語論理に限定継続を追加して、everybodyやsomebodyを表す項を作ってみる。

以下、{\bf C}, \langle \cdot \rangle はそれぞれ shift0, reset0 とする。

{\displaystyle
e = {\bf C}k. \forall x. k \hookleftarrow x \\
s = {\bf C}l. \exists y. l \hookleftarrow y
}

{\displaystyle
\langle L(e, a) \rangle \\
= \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), a ) \rangle \\
\leadsto \forall x. \langle L( \square, a ) \rangle \hookleftarrow x \\
\leadsto \forall x. \langle L( x, a ) \rangle \\
\leadsto \forall x. L( x, a )
}

{\displaystyle
\langle L(a, s) \rangle \\
= \langle L( a, ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\
\leadsto \exists y. \langle L( a, \square ) \rangle \hookleftarrow y \\
\leadsto \exists y. \langle L( a, y ) \rangle \\
\leadsto \exists y. L( a, y )
}

同時に複数使うと、引数を右から評価するか左から評価するかで継続が異なるため、結果が一意にならず、英語の表現と同様に曖昧になる。

左から評価すると:
{\displaystyle
\langle L(e, s) \rangle \\
= \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\
\leadsto \forall x. \langle L( \square, ({\bf C}k. \exists y. k \hookleftarrow y) ) \rangle \hookleftarrow x \\
\leadsto \forall x. \langle L( x, ({\bf C}k. \exists y. k \hookleftarrow y) ) \rangle \\
\leadsto \forall x. \exists y. \langle L( x, \square ) \rangle \hookleftarrow y \\
\leadsto \forall x. \exists y. \langle L( x, y ) \rangle \\
\leadsto \forall x. \exists y. L( x, y )
}

右から評価すると:
{\displaystyle
\langle L(e, s) \rangle \\
= \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\
\leadsto \exists y. \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), \square ) \rangle \hookleftarrow y \\
\leadsto \exists y. \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), y ) \rangle \\
\leadsto \exists y. \forall x. \langle L( \square, y ) \rangle \hookleftarrow x \\
\leadsto \exists y. \forall x. \langle L( x, y ) \rangle \\
\leadsto \exists y. \forall x. L( x, y )
}

以下、Racketでの実装。

#lang racket
(require racket/control)

(define (forall x f) (if (null? x) #t (if (f (first x)) (forall (rest x) f) #f)))
(define (exists x f) (if (null? x) #f (if (f (first x)) #t (exists (rest x) f))))

(define (every x) (shift0 k (forall x k)))
(define (some x) (shift0 k (exists x k)))

(reset0 (even? (every '(10 20 30))))
(reset0 (even? (every '(10 20 5))))
(reset0 (even? (some '(5 7 9))))
(reset0 (even? (some '(5 7 10))))

0の0乗

はてなブックマークで、0の0乗についての記事がホットエントリーになっていた。

0の0乗の正解がネット検索しても見つからないので作成した。 | 子育ての達人 | 妊娠・出産・育児・子育ての毎日を楽しく

「いろんな言い分は多々見受けられましたが、正しい解答に言及しているサイト(ページ)は見つからなかった」というが、この記事自体に問題があると感じた。しかし、色々考えたけれども、あまりうまくまとめることができなかった。とりあえず、考えたことを以下にメモとして残しておく。

この記事では、一方で「なぜ2の0乗は1になる」と問うておきながら、マイナス乗については、「定義は定義としてすんなり受け入れなければいけません」と主張している。これはチグハグだ。

定義というのは、そこからの議論を厳密に行うために必要なものだ。数学で議論の対象になるもの(「数学的対象」という)は、無数に存在している。互いに似通った対象が多数存在するわけだから、数学では議論を始める前に定義を行い、どの言葉がどの対象を指しているかを決めておかなければならない。そうして、決めておいた定義や公理から推論して、様々な定理を導き出す。これが純粋に数学な議論だ。

「定義は定義としてすんなり受け入れなければいけません」という話は要するに「数学は定義が与えられて初めて議論が始められる」ということだ。マイナス乗をa^{-x} := \frac{1}{a^x}と定義するように、ゼロ乗もa^0 := 1 ~ (a \neq 0)などと定義して、数学的な議論を始めることができる。

しかし、件の記事の議論は違う。

累乗の説明が終わったので0乗の説明に行きます。ここまで来ると簡単です。

2^0=2^{1-1}=2^1 \times 2^{-1}=2/2=1

つまり、2の0乗というのは2/2(2÷2)なので1なのです。

例として2で進めましたが2以外の数でも同じです。従って、0の0乗とは、0/0(0÷0)のことです。

明らかに、これは定義から推論して法則を導き出す数学的な証明ではない。指数法則が成り立つように、a^0 := \frac{a}{a}と定義したいという、定義の動機の話だ。

「なぜ2の0乗は1になるか」「なぜ0の0乗は未定義になるか」という問いは、2通りに解釈できるということでもある。数学で「なぜPか」と言ったら、普通は「なぜPか、Pを証明して示せ」ということを意味している。しかし、2^0の定義がないうちには、「2^0 = 1を証明せよ」という純粋に数学的な問いは成り立たない。「なぜPか」という文のもう1つ、「なぜ数学者は(数学では)Pが成り立つような定義を採用するのか」を意味するだろう。これは数学者の動機の問題で、純粋に数学的な問題ではないし、コンセンサスも存在しない。

付録: なぜ私は2^0 = 1となるような定義を採用するのか

「定義の理由」にコンセンサスがあるわけではないけれども、「冪乗」と「指数関数」を使い分けて説明すると、理由を納得しやすいと思う。

掛け算の繰り返しで定義されている冪乗a^xには指数法則a^{x + y} = a^x \cdot a^yが成り立つ。一方で、別の方法で定義されている*1指数関数\exp_a xにも、指数法則\exp_a(x + y) = \exp_a{x} \cdot \exp_a{y}が成り立つ。xが正の整数であるときには指数関数と冪乗は一致し、\exp_a x = a^xとなる。だから、数学では多くの場合指数関数を冪乗と同じ記法で表しているし、同一視することもある。
この説明は、\exp_2 0 = 2^0 = 1となる理由を説明できるが、高校数学の範囲での指数関数は、底が0 < a \land a \neq 1の範囲でしか定義されていないから、0^x1^xの定義には、別の説明が必要になる。
考えが変わったので、取り消す。11月23日

定義の理由の理解がどのようであれ、定義自体が共有されているのであれば、数学的な議論を行う上で問題はない。

付録: 基数における冪の定義

濃度 (数学) - Wikipedia

集合Aの濃度を\#Aと書き、集合A, Bをそれぞれドメイン、コドメインとする写像の集合を{\rm Map}(A, B)と書く。基数 (cardinal number)  a, bの冪はa^b := \#{\rm Map}(b, a)と定義され、この定義の下では0^0 = \#{\rm Map}(\emptyset, \emptyset) = 1となる。

*1:指数関数の定義は同値の定義が複数存在している

RDFa Liteのここが酷い

RDFa LiteはRDFa Coreのサブセットで、とても短い仕様なのだけれども、一点気に入らない。

なぜ、@aboutではなく@resourceを採用したのか。

RDFa 1.1 Primerによれば、@aboutと@resourceの違いは、同じ要素に@propertyが設定されている場合の意味の差だけだ。どう違うかというと……

  • @aboutは、いつでも関係の主体 (subject) を設定する。
  • @resourceは、@propertyが設定されていない場合は@aboutと同様関係の主体を設定する。@propertyが設定されている場合は@hrefと同様関係の客体 (resource object) を設定する。(ただし、hrefと違って、クリックできないリンクになる。

属性名からも明らかなように、RDFa Coreの@resourceはリソースオブジェクトを設定するのが主用途だ。@propertyが設定されていない場合の意味は、「ついで」で決められていることに過ぎない。*1(これ自体センスがない仕様だ。意味が無い指定であれば未定義として残しておけばいいのであって、無理やり@aboutと同義にする必要がない。)

@resourceの唯一の意義であった「@hrefと違って、クリックできないリンクになる」という性質だって、今日のHTMLの仕様と組み合わせるのであれば、a要素の代わりにlink要素を使えば達成できるのだから、いよいよ@resourceの存在意義は無い。

@aboutを捨てて@resourceの方を選ぶというのは、全くセンスがない。他の属性が設定されているかどうかによって意味が変わる属性とか、ありえない。@propertyと@resourceを同じ要素に設定する“間違い”をしでかす人間は必ず出てくるし、仕様を策定する人間にセンスがないと、全世界に迷惑を掛ける。RDFa 1.1 Primerにその“間違い”を例示するぐらいだったら、最初から@aboutをプライマリとして採用してくださいよ。

*1:追記: subject、object両方とも、URIで指定されるのはresourceであり、resourceという名前がobjectを指しているという指摘は不当なので取り消す。しかし、場合によってsubjectの指定であったりobjectの指定であったりすることの筋の悪さに変わりはない。

schema.org/URLってダメ

Poor schema.org/URL - Ryusei’s Notes (a.k.a. M59のブログ)の雑な日本語訳。というか、原文が雑な英語すぎるし、まとまってない。)

schema.org/URL というデータ型が定義されているんだけど、これって酷いよね。「この属性のデータ型って何?」「URL。」って、答えになってないじゃん。

URLってのは、単なる識別子だよ。これはURLだなんて分かってる。ウェブにあるモノってのは、だいたいそれを指すURLを持ってる。知りたいのは、それがURLってことじゃなくて、そのURLが指しているモノの型が何なのかってことなんだから。

URLは、schema.org/Textのサブタイプであるべきじゃない。ハイパーリンクとして指定されているURLは、モノがある場所として解釈されるべきで、URLそれ自体がモノとして解釈されるべきではない。

Poor schema.org/URL

schema.org/URL is one of data types defined for linked data. I hate it, because it is totally useless. “Hey, what is the data type of this attribute?” “URL.” That is nonsense.

An URL is just an identifier. That is URL, I know. Almost every thing on the web have an URL that denotes it. What I want to know is the data type of the thing that the URL stands for.

URL should not the subtype of schema.org/Text. The URL specified for a property as hyperlink should be interpreted as the location that the thing is. Not be the URL itself the thing.

ソースコードは基本設計図か

www.nikkei.com

用語ミニ解説として、オープンソースが「基本設計図である「ソースコード」が公に開示されているソフト」と解説されているのだけれども、ソースコードは基本設計図なのだろうか。

基本設計図というのは建築における用語だ。建築では、設計図には基本設計図と実施設計図とがある。建築工事に必要なのは、実施設計図だ。www.homes.co.jp

建築における基本設計図とソフトウェアにおけるソースコードの間には、重大な差異がある。基本設計図の段階ではまだ建物は建てられないのに対して、ソースコードは既にビルドできる状態のもので、ビルドすれば実働するソフトウェアが得られるという点だ。建築にたとえるなら、ソースコードはすでに「建築工事」に回せる段階のものだから、これはむしろ「実施設計図」に相当する。

コメント欄についてのコメントまとめ

Twitterのツイートをまとめました。

2012年


2014年1月17日

NATROMの日記のコメント欄が承認制になった時のコメントです。











2015年1月6日

Qiitaというウェブサイトのコメント欄が荒れた時のコメントです。

2015年7月28日

またQiitaのコメント欄が荒れていました。その時のコメントです。






2015年8月5日

コメント欄について議論する分野はどこなのかについての疑問です。



望ましいコメント欄の姿はなんだろう。

この記事は、イケダハヤト氏の記事に反応して書かれたものだ。コメント欄について、私は過去にもいくらか考えてきた。Twilogからコメント欄についてのコメントを拾い、あらためて自分の意見を確認した。

www.ikedahayato.com

この記事ではコメント欄を閉鎖する理由を「ゴミの掃き溜めです」、「建設的ではありません」と、説明している。一方で、「サイトコンテンツを拡充するという観点では、コメント欄は本来的には有意義」とも書いている。前者は、コメント欄につくコメントは無価値であると言っていて、しかし、後者はコメント欄が本来的に有価値であることを訴えている。

私もブログのコメント欄は閉鎖したほうがよい場合があると考えているが、それはコメント欄にゴミのようなコメントしか付かないから、議論が建設的でないから、といった理由ではない。だいたい「ゴミのような」だとか「建設的でない」のような判断は主観的な価値判断に過ぎないもので、ゴミのようなコメントが付いたり、建設的でない議論が繰り返されること自体から、何らかの意味を見出すこともできる。ゴミのようなコメントが付くコメント欄は十分有意義で、ただ記事の著者にとっては不都合・不愉快である場合があるというだけだ。

私が撤去したほうが良いと考えるコメント欄には、個々のコメントの管理の問題と、話題の管理の問題がある。

個々のコメント管理の問題というのは、社会的に問題のある発言を削除しなければならないということだ。もしコメント欄の管理を記事の著者自身で行っていると、コメント投稿者に、記事の著者にとって都合の悪い発言や反論が不当に削除・検閲されているのではないかという疑念を抱かせてしまう。最初から外部のサービスにコメント管理を委譲してしまい、著者自身で管理できないようにしてしまえば、著者は他人のコメントに何ら責任を負う必要がなく、とても気楽だ。

話題の管理の問題というのは、コメント欄が荒れることだ。はてなブログのコメント欄のように、コメントが一列のリストになっている場合、コメント欄の荒れが問題になりやすく、荒らしに脆弱だ。コメント欄が荒れて機能不全を起こすのは「記事に対するコメント」と「コメントに対するコメント」が区別されていないからで、スラドのようにツリー構造のコメント欄であれば、ツリーごとに異なる話題を続けられるから、ひとつの枝が荒れていても、他の枝に影響しづらい。あるいは、ツイッターのように、コメントどうしが勝手に参照しあうような構造でもよい。ツイッターのような構造は議論には向かなくなり、よりコメントらしい使い方になる。はてブのように、コメント量を制限しても、荒れることはない。

そういうわけで、撤去せずとも良いコメント欄は次の性質を持つ。

  • 著者自身が管理できない。個別のコメントの削除はコメントした人自身か、コメントサービス提供者が行う。記事の著者が他人のコメントに責任を負ってはいけない。
  • コメント欄の話題が1つにロックされない。複数の話題を持てるツリー型や、話題が存在しないツイート収集型、コメント量を制限するブックマークコメント型などにする。

Facebookコメント、Twitterの検索結果タイムライン、そしてこのブログにあるような、はてブコメント欄のどれも、この性質を満たしている。あとはコメント欄をブログに埋め込むかどうかは個々人の“衛生観念”の差で決まるもので、自分に対して批判的なコメントを読むのは精神に悪いからコメント欄を設置しないというのも、別にいいのではないかと思う。

CSSでヒラギノ角ゴシックのウェイトを指定する方法

※追記あります

Mac OS X El Capitanのヒラギノ角ゴシック — Medium

ヒラギノ角ゴシックは10ウェイトあるが、CSSでは9つ(100から900まで100間隔)でしか指定できない。しかも、具体的にどのウェイトで表示されるかが、ブラウザによって異なっているようだ。

f:id:mandel59:20151003203853p:plain:h411

font-weightと実際に使われるウェイトの対応の表:

CSS font-weight Firefox Chrome
100 W0 W0
200 W2 W1
300 W3 W3
400 W4 W4
500 W5 W5
600 W6 W6
700 W7 W7
800 W8 W8
900 W9 W9

また、normalとboldはそれぞれ400と700を指定するのと同じなのだが、今までのヒラギノ角ゴではW3とW6を使ってきたのだから、これでは少し太いかもしれない。こういう時は、@font-faceを使って、ウェイトと実際に使われるフォントの関係を直接指定してしまえばいい。

@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W0);
  font-weight: 100;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W1);
  font-weight: 200;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W2);
  font-weight: 300;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W3);
  font-weight: 400;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W4);
  font-weight: 500;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W5);
  font-weight: 600;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W6);
  font-weight: 700;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W7);
  font-weight: 800;
}
@font-face {
  font-family: "Hiragino Sans";
  src: local(HiraginoSans-W8);
  font-weight: 900;
}
@font-face {
  font-family: "Hiragino Sans W9";
  src: local(HiraginoSans-W9);
  font-weight: 900;
}
div {
  font-family: "Hiragino Sans";
  font-size: 20pt;
  line-height: 1.5em;
}
<div style="font-weight: 100">ヒラギノ角ゴシック W0</div>
<div style="font-weight: 200">ヒラギノ角ゴシック W1</div>
<div style="font-weight: 300">ヒラギノ角ゴシック W2</div>
<div style="font-weight: 400">ヒラギノ角ゴシック W3</div>
<div style="font-weight: 500">ヒラギノ角ゴシック W4</div>
<div style="font-weight: 600">ヒラギノ角ゴシック W5</div>
<div style="font-weight: 700">ヒラギノ角ゴシック W6</div>
<div style="font-weight: 800">ヒラギノ角ゴシック W7</div>
<div style="font-weight: 900">ヒラギノ角ゴシック W8</div>
<div style="font-family: 'Hiragino Sans W9'">ヒラギノ角ゴシック W9</div>

f:id:mandel59:20151003204830p:plain:h410

10月4日追記

上の方法だと、Firefoxでは正しく表示されるが、SafariGoogle Chromeだと、W5が正しく表示されない。
f:id:mandel59:20151004131621p:plain:h406 Safariでの表示
本来boldでないW5にfont-weight: 600を指定していると、機械的にboldになってしまうようだ。
やはりfont-weightを使わず、直接指定するのが無難だろう。

指定例: A Pen by Captain Anonymous

GMailのリプライをスレッドにまとめる機能は完全にダメ

GMailのアプリは関連するメールを一つにまとめる機能があるけど、この仕様を把握していないせいで完全に失敗した。メールに新規の未読のリプライが付いても、それは既読のメールの下に表示されるわけで、これじゃあ未読のリプライの内容を読み逃してしまうに決まっているじゃないか。なんでこんな仕様なんだ。

f:id:mandel59:20151001142047p:plain

https://support.google.com/mail/answer/5900?hl=ja

人力検索はてなの質問をキャンセルしたら内容が消えてしまったので、こちらに残しておく。

昔読んだ数学の児童書を探しています。 内容は断片的にしか覚えていません。おそらく12年以上前に図書館で読んだ本です。 小説仕立ての本であり、ワープロフロッピーディスクに、奇妙な外字で書かれた文書が保存されていて、それはコンピューターに住む未知の生命体の残した、未知の数学に関するメッセージだったというような話だったように思います。いくつかのトピックがあったと思いますが、そのひとつとして、p進数(p-adic number)に関連するようなトピックがありました。もしかしたら、大きめの判型の本で、上下で2冊分の本だったかもしれませんが、確かではありません。 少ない情報ですが、心当たりがあるかたはよろしくお願いします。

http://q.hatena.ne.jp/1443281726

www.amazon.co.jp

www.amazon.co.jp

ありがとうございました。

関数とラムダ計算の話

bugrammer.hateblo.jp

この記事へのツッコミみたいなことを書くつもりだったけど、あんまり関係ない話になったので、サイドストーリーみたいにして読んでください。

分野によって「関数」が違うこともある

前回、数学的な関数の定義の話があったけど、あれは写像の定義であって、個々の分野で「関数」と呼ばれているものと、いつでも一致するとは限らない。まあ普通は関数と言ったらほとんどの場合写像を指すので、少し違う物を指すときは、多価関数とか連続関数みたいに、別の名前を付けていることも多い。

で、プログラミングに関する文脈で「関数」と呼ばれるものが写像と一致するかといえば、もちろん一致しない。ある程度似た部分もあるけど、違う性質を持っている。この違いを、数学的にどうやって説明するかが問題になる。計算の性質を説明するための抽象モデルが抽象書換系で、ラムダ計算の意味も、抽象書換系によって定義できる。この定義の方法は、写像の定義とは大きく異なっている。

写像とラムダ項の間には、具体的にどういう違うがあるのだろうか。

一方で、写像には右一意性\forall a \in A, \forall b_1, b_2 \in B, ((a, b_1) \in G_f \wedge (a, b_2) \in G_f \Rightarrow b_1 = b_2)という性質があるが、ラムダ計算には合流性という性質があり、計算が停止する範囲では、写像とよく似た性質を持っているということが言える。

ラムダ計算の派生

ラムダ計算には、簡約の方法を制限したり、型を付けたりするといった、色々な派生系が存在していて、それぞれの体系が異なる性質を持っている。例えば、単純型付きラムダ計算は、型なしラムダ計算と異なり、計算が必ず停止する。(強停止性を持つ。)

よく知られている関数型言語の多くは、ラムダ計算から派生した体系を使っているが、ラムダ計算以外の体系を使った関数型言語も考えられる。

アクションと関数、式の値の話

bugrammer.hateblo.jp

  • a -> bというのは、引数にa型の値をとり、b型の値を返す関数の型だ。
  • Monad mが存在するような任意の型コンストラクタmについて、m aというのは、a型の値を生成する(Monad mの)アクションの型だ。

という型の意味を理解していれば、関数(>>) :: Monad m => m a -> m b -> m bは、その型から、

  • Monad mが存在するような任意の型コンストラクタmについて、
    • m a型の値(アクション)(これをxとする)を引数にとり、
    • m b -> m b型の値(関数)(これは(>>) xと表せる)を返す関数で、つまりその返される関数は、
      • m b型の値(アクション)(これをyとする)を引数にとり、
      • m b型の値(アクション)(これは(>>) x yと表せる)を返す関数で、つまりその返されるアクションは、
        • b型の値を生成するアクション

だということが読み取れる。

一方で、「m a型の値(アクション)xを破棄する」といったことは、型から読み取ることはできないし、事実でもない。実際、(>>) x y = (>>=) x (\z -> y)と定義でき、アクションxは破棄されない。破棄されるのはアクションxが生成する値で、それはxではなくzだ。

関数が値を返すということと、アクションが値を生成するということには大差がないように見える。実際に、多くのプログラミング言語は関数に副作用を認めていて、関数とアクションを区別しない。しかし、関数が、引数が定まれば返り値も一意に定まるという性質を持っているのに対し、アクションは、生成する値が定まるという性質を持っていないから、同列に扱おうとすると、式の値が一意に決まらなくなる、という困ったことが起きる。

そもそも、式の値はなんだろうか。(ここで書いている「手続き型プログラミング」「関数型プログラミング」という分け方は一面的なものに過ぎないから、あんまり深刻に考えないで欲しいのだけれども、)手続き型プログラミングにおいて、値というのは手続きから手続きへ渡されたり、変数に代入されたり読み出されたりするものであって、「式が値を持つ」という考えは、算術の式に対しては考えていても、プログラム一般に敷衍されるものではないように思われる。プログラムは文の集合だ。文は意味を持つが値を持たない。それが、手続き的なプログラミングにおいて一般的な考え方だ。

一方、関数型プログラミングでは、プログラムは式だ。関数型プログラミング言語の式は部分式と関数適用から構成されていて、どの部分式も値を持つ。関数型プログラミングでは、プログラムの構造を内包した値を扱うことでプログラミングするようになる。直和型の値は分岐構造を内包しているし、リスト型の値は反復構造を内包している。モナドは、手続き型言語における各種副作用を持つ、逐次構造を内包した型の集まり(型クラス)ということになる。このように複雑な値を使うことで、関数型プログラミングではプログラムの意味と式の値を同一視できるようになる。

プログラムの意味と式の値を同一視できると何が嬉しいかというと、意味を持つプログラムの断片がすべて値を持つので、プログラムを処理するプログラムが書きやすくなる。プログラムのどの断片も、関数として抽象化することができる。他の関数に渡すことが出来る。変数にプログラムを代入できる。

話をアクションに戻す。Haskellにおいては、アクションが生成する値と、アクション自体は別だ。たとえば、getChar :: IO Charは標準入力から文字を1文字読み込み、その文字に対応するChar型の値を生成するアクションなのだけれども、Haskellでは、式getCharの値は「標準入力から文字を1文字読み込み、その文字に対応するChar型の値を生成するアクション」自体であり、生成されたChar型の値ではない。アクションgetCharの生成する値を取り出して言及するには、do {z <- getChar; k z}zgetChar >>= \z -> k zzとでも言うしかない。

色々書いたけど、結局、値とは何かという話に合意が得られていない状況ではどうにも話が通じないという点が問題で、以前からココらへんの考え方を整理して参照透過性についてなんとか説明しようと試みたりしているのだけれども、やっぱり難しいですね。

追記のメモ書き

ツッコミどころ

  • Haskellにも値を持たない、式より上位の宣言の構造があるじゃん
  • プログラムの意味と値が一致しない純粋でない関数型言語なんてザラでしょ
  • 値を返す手続きを第一級の値として持てれば、純粋でなくても高度なプログラミングが簡単にできる上に、手続きを取り扱うだけのためにモナドを取り入れる必要がない。プログラムの意味と値を一致させる必要ってないんじゃないのか。
  • モナド以外に、一意型を使って値の複製を制限し、制御(ハンドラ)を表す値を導入することで、プログラムの意味と値の一致を図る方法がある。