Phantom property pattern

TypeScriptは、JavaScriptエンジンの動的セマンティクス上に、静的な型システムのセマンティクスが重なっているものです。ここで、JavaScriptとしては正しく実行できても、TypeScriptの型システム上ではちゃんと型が付かないという場合もあります。ときには、TypeScriptで型がつくように大幅に書き換えないといけない場合も出てきたりして、そうなると大変です。それでも、TypeScriptの型システムは高度な機能を持っているので、大体の場合は、うまく表現してやると、JavaScriptらしい書き方のままで型をつけることができてしまいます。今回は、JavaScriptでよくある、プリミティブ値をそのまま取り回すパターンに型を付けたいと思います。

プリミティブ型を扱うプログラミングは、素朴でわかりやすいですが、型の考えからするとかなり悪いものです。こういうプログラミングを行うと、あらゆるデータを文字列で表す様子から、ときに”stringly typed”と揶揄されます。文字列は、表したいものはとりあえず何でも表現できるのでとても便利ですが、いろいろな種類のデータが一つの型で表されてしまうのなら、型が役立たずになってしまいます。すべてがstring型のプログラムで、どうやってその文字列の中身がテキストなのか、URLなのか、メールアドレスなのかを判断するのでしょうか? 文脈を読み込んで察するか、ハンガリアン記法に回帰するか、さもなくばエスパーで当てるしかないでしょう。

この問題に対処するひとつの「まっとうな」方法は、プリミティブ値を直接使わず、適宜ラッパーオブジェクトを作り、その上でプログラミングを行うことでしょう。プリミティブ値ではなくオブジェクトを使えば、メソッドを追加することも容易です。しかし、実際にJavaScriptでそういうことが行われづらい原因として、ひとつはプリミティブ値をコンストラクタでラップするが手間だという点、ひとつは===による同一性比較がオブジェクト型に対しては工夫を加えなければ意味上の同値性比較にならない点、ひとつは性能上の問題点、ひとつはシリアライズ・デシリアライズの自明さが失われる点が挙げられます。要するに、プリミティブ値をオブジェクトで包むのはわりとデメリットもあるわけです。

今ここに、この問題へのもうひとつの対処方法、幽霊プロパティパターン phantom property pattern を提唱します。このパターンを使うと、プリミティブ値の型を好きなだけ定義できる。つまり、言語組み込みのプリミティブ値を取り回すプログラムでありながら、各プリミティブ値を別々の型として取り扱うことができるようになります。

幽霊プロパティパターンでは、まず、次のような型を定義します。

export type Tag<X, R extends keyof any, Y> = X & {
    [rel in R]: Y
}

x: Tag<X, R, Y>は「xはXで、xのRはYである」というような意味になります。

次に、幽霊シンボルを定義します。

// This is a phantom symbol, which does not exist at run time
declare const _unit: unique symbol
export type unit = typeof _unit

_unitは幽霊シンボルで、宣言しますが、実際には定義しません。_unitの型はユニークシンボル型ですが、このままでは型に名前がなく使いづらいので、unitというエイリアス名を付けます。

ここに定義したTag型コンストラクタと幽霊シンボルを組み合わせると、プリミティブ値の性質を幽霊プロパティとして表現できます。

例として、角度の単位を幽霊プロパティとして付加した型を定義してみましょう。

export type Scale<X, U> = Tag<X, unit, U>
export type Radian = Scale<number, "radian">
export type Degree = Scale<number, "degree">

ここで定義したRadian, Degreeは両方ともプリミティブ値の数値を元とする型ですが、実際には存在していない[_unit]プロパティの型が異なるため、相互に代入不可能となっています。

{
    const x: Degree = 30 as Degree
    const y: Radian = x // type error!
    console.log(x, y)
}

いいですね。これを使って、たとえば三角関数双曲線関数に単位をつけてあげるといい感じになります。

export const sin = Math.sin as (x: Radian) => number
export const tanh = Math.tanh as (x: Radian) => number
export const asin = Math.asin as (x: number) => Radian
export const atanh = Math.atanh as (x: number) => Radian

{
    const x = 30 as Degree
    const y = sin(x) // type error!
    console.log(y)
}

弧度法で渡すべきところをうっかり度数法で渡すミスを、これで防げますね。 相互に変換する関数も用意してあげましょう。

// Ref: https://tauday.com/tau-manifesto
const τ = 2 * Math.PI

/** converts radian to degree */
export function toDegree(x: Radian): Degree {
    return (x / τ * 360) as Degree
}

/** converts degree to radian */
export function toRadian(x: Degree): Radian {
    return (x / 360 * τ) as Radian
}

{
    const x = 30 as Degree
    const y = sin(toRadian(x)) // ok
    console.log(y)
}

例をもう一つ、今度はUnix時間とISO8601を扱ってみます。 今度は単位ではなくデータフォーマットの話なので、新しくdataformat型を定義しています。

declare const _dataformat: unique symbol
export type dataformat = typeof _dataformat

export type UnixTime = Tag<Unit<number, "millisecond">, dataformat, "unixtime">
export type ISODateTime = Tag<string, dataformat, "iso8601">
export const now = Date.now as () => UnixTime
export const toISODateTime = (t: UnixTime): ISODateTime => new Date(t).toISOString() as ISODateTime
export const toUnixTime = Date.parse as (d: ISODateTime) => UnixTime
export function isISODateTime(s: string): s is ISODateTime {
    return /^\d{4}-\d{2}-\d{2}T\d{2}:\d{2}:\d{2}(?:\.\d{1,3})?Z$/.test(s)
}

{
    const t = 1514810096000 as UnixTime
    console.log(toISODateTime(t))
    const d = "2018-01-01T12:34:56Z"
    if (isISODateTime(d)) {
        console.log(toUnixTime(d))
    }
}

UnixTime型はデータフォーマットだけでなく、単位も幽霊プロパティで付加していますね。一口にUnix時間と言っても、実際にはミリ秒単位のものと秒単位のものが混ざっていることがよくあるのですが、こういう工夫が事故を防いでくれるはずです。

ISODateTime型の方は、型ガード関数を用意しました。こういう関数を用意して使うほうが、直接as ISODateTimeでダウンキャストするよりも安全です。

欠点

  • 本当ならinterface Tag<X, R, Y> extends X { [rel in R]: Y }とでも定義したいところですが、現状のTypeScriptではプリミティブ型を拡張できないため、やむなく交叉型 intersection type で表現しています。
  • 幽霊シンボルそれ自体はexportしないほうがいいでしょう。実在しない識別子なので、アクセスしても型エラーになりませんが実行時エラーになる可能性があります。型レベルで使うだけでシンボル自体はなくてもいいので、シンボルの型に名前を付けて、そちらをexportするといいです。
  • interfaceではないため、スニペットコンパイラのエラーメッセージ等で、型エイリアスが展開されて表示されてしまいます。unique symbolと表示されるだけなのは非常にまずいです。
    • f:id:mandel59:20180901034739p:plain
    • ワークアラウンドとして、幽霊シンボル自体にタグをつけるように書き換えると、なんとか分かるようになります。
      • f:id:mandel59:20180901035321p:plain
declare const _unit: unique symbol
export type unit = Tag<typeof _unit, "name", "unit">
export type Unit<X, U> = Tag<X, unit, U>

declare const _dataformat: unique symbol
export type dataformat = Tag<typeof _dataformat, "name", "dateformat">

まとめ

幽霊プロパティパターンを使うと、実行時コストに影響を与えることなく(ゼロコストで)、プリミティブ値にユーザー定義の型をつけることができるようになります。

2019/08/20追記: この記事を書いた時点では、先行事例があるということをちゃんと調査していませんでしたが、実は"Branding"と呼ばれて、それなりに使われている技法であることを知りました。(TypeScriptのソースコードでも使われています。

以下の記事では、Brandingや、その変形であるFlavoringについて解説されています。 Need Flexible Nominal Typing for TypeScript? Use Flavoring, not Branding

高校の教科書に載っている「情報」の説明が変だという話

数研出版の教科書『高等学校 社会と情報』(平成24年2月27日検定済、平成27年1月10日発行)の序編第II章では、「情報の特徴」と題して、情報とは何かとその特徴についての説明が行われているのだが、そこで行われている「情報の有無」の説明にいまいち納得が行かない。

情報の有無

16本のマッチ棒をテーブルの上に投げたとき,たいていは,図1のような乱雑な並び方になる。偶然にマッチ棒が,図2のように「SOS(または505)」の文字の形になる可能性もあるが,きわめて確率が低い。私たちが,図2を見たら,人が手で並べたと思うだろう。

この2つの状態(図1の並び方と図2の並び方)のちがい(差)は,何だろうか。私たちが一目見てわかるように,この2つには大きな差がある。そのちがい(差)が,情報である。

f:id:mandel59:20170102025120j:plain

(『高等学校 社会と情報』14ページ)

並び方の乱雑な「テーブルに投げたマッチ棒」と、並び方に秩序があるように感じられる「人が並べた?マッチ棒」とを比較し、その差が情報であるとする「説明」は、理屈ではなく人間の直感に訴える説明であるため、理屈を気にしない人間ほど納得してしまうのではないかと思うけれども、しかしこの説明は変だ。

この説明は、乱雑な図1「テーブルに投げたマッチ棒」が〈情報がない方〉で、秩序だった図2「人が並べた?マッチ棒」が〈情報がある方〉だという想定で書かれているのではないかと思う。この説明をされて、何かが読み取れる方が〈情報がある方〉、何も読み取れない方が〈情報がない方〉だと受け取るのは、普通の感覚だと思う。

しかし、考え方によっては「左の方が情報が多い」と結論づけることもできる。どういうことか? こんな遊びを考えてみよう。

この遊びは2人でやる。片方の人間が、机の上のマッチ棒の状態をできるだけ少ない言葉で説明する。もう片方の人間は説明を聞いて、元の状態を見ずに、マッチ棒の状態を言葉だけから再現する。

図1と図2、それぞれでこの遊びをやるとどうなるだろうか。図1のマッチ棒の状態は乱雑で、素直に説明する言葉が見つからない。「マッチ棒が散らばっている」と言うだけでは図1の状態を精度よく再現することはできないから、マッチ棒1本1本について、その位置と向きを細かく説明する必要がある。一方、図2のマッチ棒の状態は秩序だっている。「マッチ棒が505の形に並んでいる」という言葉だけでも、ある程度再現可能だろう。マッチ棒の向きが問題だとしても、それぞれについて上下左右で指定すればいい。

結局、図1は図2よりも説明に必要な言葉が多いので、より情報が多いと考えられる。

こういう説明もできることを考えると、図2の方が〈情報がある方〉なのは一目瞭然だとするわけにはいかないはずだ。

乱雑に並んだマッチ棒は、意味のわかるパターンを含んではいない。しかし、意味のわかるパターンを含まないというのは、情報を持たないということではない。例えば、ジャングルの木々の並びにも、人間にとって直接意味のわかるパターンは含まれていないが、しかし、ジャングルの木々の並びを覚えることで、自分が今ジャングルのどこにいるのかを知ることができるようになり、ジャングルでの生活に役立てられるだろう。件の教科書は「情報」とは「意思決定の材料になるもの」(15ページ)だという考えを載せているが、その考えで情報を捉えるとしても、ジャングルの例で分かるように、人間が意図しない自然発生の差異もまた人間の意思決定の材料となる「情報」であるはずだ。

人間の作成したコンテンツを主に取り扱っていると「情報は人間が生む」という錯覚に陥りがちだが、情報を生むのは人間だけではない。宇宙のあらゆる存在が情報源となりうるのであり、それは人間がその意味を読解できるかとは関係がない。

「What Is Functional Programming? に対する反論」を読んで考えたこと

lyrical-logical.hatenablog.com

読んでいて引っかかった部分について考えました。

mutable変数は「入力とは呼べない」?

この記事で僕が伝えたいのは、君が書くあらゆる関数には二組の入力と二組の出力があるってことだ。

間違いなく、InboxQueue の状態はこの関数の本物の入力だ。

この隠れた入出力にはちゃんとした名前があって、その名を「副作用」という

InboxQueue は、その関数スコープから参照可能な変数の一つに過ぎない。たまたまその関数の環境から触れるというだけで、入力というよりは、環境の中の mutable な変数の一つ、以上のことはないし、これを入力とは呼べない。これはプログラムの状態だ。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

問題のプログラムはこれです。

public void processNext() {
    Message message = InboxQueue.popMessage();

    if (message != null) {
        process(message);
    }
}

これはJavaのコード断片ですけど、断片だと分かりづらいので、JavaScriptでプログラム全体を書いてみることにします。

let Processor = {
  inbox: null,
  console: null,
  processNext() {
    let message = this.inbox
    if (message != null) {
      this.console = message
    }
  }
}

function main() {
  Processor.inbox = "hello"
  Processor.processNext()
  console.log(Processor.console)
}

main()

このコードのprocessNextメソッドは、元のコード断片より簡略化されているけど、議論の要点はおさえているはずです。

確かに、Processor.inboxはProcessor.processNextメソッドから参照可能なmutableプロパティですが、同時にmain関数からも参照可能です。このことが、mutableプロパティを一種の「共有メモリ」として使った2関数間の通信を可能にしています。

プロパティ経由の値の受け渡しが、「プログラムの状態」としてプログラミング言語のセマンティクス内で説明できる動作だとしても、Processor.inboxはProcessor.processNextへの入力となっていると表現して問題ないはずです。

このコード例から、次のことが言えます:

  • 関数の外部から書き換え可能で、関数の内部から参照可能なmutable変数は、関数への入力として使うことができる。(このような入力を副原因という。)
  • 関数の内部から書き換え可能で、関数の外部から参照可能なmutable変数は、関数からの出力として使うことができる。(このような出力を副作用という。)

副原因と副作用は対称的で、Processor.inboxはProcessor.processNextにとって副原因の源ですが、mainにとっては副作用の対象です。つまり、副原因があるとき、対になる副作用も現れ、大域的に見れば両者は同一の現象です。

「暗黙的に環境内の変数を参照するよりも、陽に変数を取るようにしたほうがいい」?

言いたいことは分かる。暗黙的に環境内の変数を参照するよりも、陽に変数を取るようにしたほうがいい。

public void processNext(InboxQueue inboxQueue) {
    Message message = inboxQueue.popMessage();

    if (message != null) {
        process(message);
    }
}
http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

環境に依存した関数の定義には注意すべし、それは一般に言って正しいことだと思うし、反論するつもりはない。しかしそれを「関数型プログラミングって何?」という文脈で話すのは、違和感が強い。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

ここで言っている「環境」って、何を指しているんでしょうか? グローバル環境のことでしょうか? それとも、関数の引数ではなく、ブロックスコープに宣言された変数を、環境内の変数と呼んでいるのでしょうか? あるいは、次のようなクロージャーで、関数g内で参照されているxはgの引数ではないわけですけど、こういう場合も「暗黙的に環境内の変数を参照する」に入るんでしょうか?

function f(x) {
  return function g(y) {
    return x + y
  }
}

「あらゆる関数」?

しかし * あらゆる * 関数に二つの入力がある、と記事では主張している。つまり上のコードでは不足だろう。
ならもうちょっと別の書き方をしよう。コードは疑似的なもので、こんな API がある言語は知らない。

public void processNext(Frame frame) {
    Message message = ((InboxQueue)frame.getEnvironment.getVariables.searchVariable("InboxQueue")).popMessage();

    if (message != null) {
        process(message);
    }
}

あるいは、InboxQueue の状態をある種の precondition としてとってもいいかもしれない。

public void processNext(InboxQueueState state) {
    // state を使って何かしたいときもあるかもしれない。以下は一例だ。関数の意味は変わる。元記事では関数の前提条件について何も触れられていないので、これは自分が勝手に加えたものだ。popMessage は blocking API かもしれないし、そうであればこのような前提条件は妥当でない。
    if (state.isEmpty()) throw new IllegalArgumentException("InboxQueue must has some elements.");
    // これは assert を書いて precondition をコード上で陽にしているのと大した差はない。
    assert(!state.isEmpty());

    Message message = InboxQueue.popMessage();

    if (message != null) {
        process(message);
    }
}

一歩譲って、これらをもってして、あらゆる関数には二つの入力がある、という主張を受け入れたとしよう。しかしそれは「関数プログラミングにとって」大事なことなんだろうか。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

このくだりはほとんど意味が分かりません。「関数型プログラミングって何?」の酷さを示すために、書かれたとおりにやってみて酷さを示すというにしては、そもそも書いてもいないことを突然やりだしたように見えます。「上のコードでは不足だろう」と思った理由もはっきりしなければ、それで例に出した「別の書き方」をそう書いてみたワケも、書かれていません。

“I put it to you that every function you write has two sets of inputs and two sets of outputs.” という一文中の “every” という一語が気にくわないということ以上ではないのであれば、よく分からない例なんか出さずとも、記事最初の例

public int square(int x) {
    return x * x;
}

には副原因も副作用もないよね、と指摘すれば済むのでは、と思ってしまいます。

でも、ただ「 * あらゆる * 関数に」って書き方じゃなくてevery function you writeなんだし、自分はこれは記事に食い付かせる「釣り」のたぐいの表現なんじゃないでしょうか。まあ、こういう正確さに欠けた表現はちょっと気に障るってのは分かります。

「本当にそうだろうか」?

これで、この関数は入力(や出力)を隠し持たなくなった。

本当にそうだろうか。上の主張は関数内で読んでいる関数が純粋であるという仮定が成り立つときに限る。"getSchedule" "programAt" が純粋でないなら、そこには状態が潜んでいる。関数内で呼び出している関数のスコープにある状態に触れている、依存している可能性がある。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

もう少し前に、こう書いてあります。

この関数には現在時刻 (new Date()) という入力が隠れている。

http://okapies.hateblo.jp/entry/2016/12/15/021550

"getSchedule" "programAt" が純粋でないなら、「この関数には現在時刻 (new Date()) という入力が隠れている」という部分で一緒に副作用(あるいは副原因)のある関数としてリストアップされなければ、話の構造上不自然です。ここでリストアップされていない以上、 "getSchedule" "programAt" は純粋だということが暗に示されてます。それを、陽に示されていないからといって「"getSchedule" "programAt" が純粋でないなら」と言い出すのは、揚げ足取りに見えます。

「一般的な説明でよいだろう」?

引数にのみ依存し値を返す、同じ引数に対して常に同じ値を返す関数であるという一般的な説明でよいだろう。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

「引数にのみ依存し値を返す、同じ引数に対して常に同じ値を返す関数」という定義には問題があります。この定義では、副原因を持たないが副作用を持つ、次のような関数を除外できないのでダメです。*1

let a = null

function out(x) {
  a = x
  return x
}

「読めば訳された記事がイマイチなのは分かる」?

結論。住井先生がわざわざ記事書いてくれてるんだから、まずそれを読もう。読めば訳された記事がイマイチなのは分かると思う。

http://lyrical-logical.hatenablog.com/entry/2016/12/15/135831

“A functional language actively helps you eliminate side-effects wherever possible, and tightly control them wherever it's not.”って、住井先生の「関数型言語とは、……関数型プログラミングを推奨・支援するプログラミング言語」「(関数型プログラミングとは)副作用をできるだけ(あるいは全く)用いず、式や関数で計算を表すプログラミングスタイル」ってのとほぼ同じこと言ってますよね。まあ、住井先生の記事の方はリファレンスがちゃんと張ってあるのがいいと思います。

*1:こういう説明が簡単にできるようになるので、「副作用」と「副原因」を区別するのは有意義だと思います。

游ゴシックは何故Windowsでかすれて見えるのか

この記事は2016年当時の状況を書いています。その後のバージョンアップで、Windowsでのフォントレンダリングは改善され、ガンマ補正周りのエラーはなくなっているようです。当時の状況を資料として残しておきますが、記事を参照する場合はご注意ください。

TL;DR

游ゴシック体は単に細いから薄いのではなく、ガンマ補正が2重、3重に掛かっているために、グレーが本来よりも明るくなりすぎている。ガンマ補正を逆に掛けると、正常な表示になる。

かすれた游ゴシック

Windowsでは游ゴシックがかすれて見える。細字だと薄くて読みづらいから、より太いウェイトを指定しろという話もある。(Windowsで游ゴシックが汚いのは、結局誰が悪いのか? | Cherry Pie Webなど)だが、かすれて見える原因は、ウェイトが細すぎるからではない。

例えば、本文に游ゴシックを使っているWIREDの記事(「癌」という名のドラゴン──父はゲームをつくった。死にゆく息子のために | WIRED.jp)のキャプチャ画像を見てほしい。



WIREDの記事をFirefoxで表示したもののキャプチャ

注目してほしいのは、ただ文字が薄いというわけではなく、線によって濃さが違うということだ。曲線の多い仮名に比べて、ピクセルに沿った直線の多い漢字の方が黒くみえる。

また、アプリケーションによって字のかすれ具合が違う。たとえば、次の画像は游ゴシックを同じウェイト、同じポイント数で、それぞれFirefoxとメモ帳を使って表示したものだ。



Firefoxで表示したもの



メモ帳で表示したもの

どちらも薄くかすれて見えるが、メモ帳の方がより薄く見える。

ガンマ補正

Windowsのフォントレンダリングは、ただ薄いのではなく、線によって濃さが違う。その原因は、ガンマ補正が適切に行われていないことだ。

ガンマ補正とは何かを説明するために、色の仕組みから説明する。

多くの人が知っているとおり、コンピューターでは色を数値で表したものを処理する。色を数値で表す方法には色々あるけれども、いちばん有名なのは、RGBカラーコードだろう。たとえばCSSでは、カラーコードを使って、黒はrgb(0, 0, 0)、白はrgb(255, 255, 255)とも表せる。これは、色を構成するR(赤), G(緑), B(青)の三原色それぞれの輝度を、0から255までの数値で表現したものだ。

しかし、ここから先の話はあまり知られていないことだと思う。多くの人は、rgb(255, 255, 255)の半分の明るさのグレーは、rgb(128, 128, 128)だと思っている。だけど、それは間違いだ。実は、rgb(128, 128, 128)はrgb(255, 255, 255)の2割ほどの明るさしかない暗いグレーであり、本当に半分の明るさになっているグレーはrgb(188, 188, 188)なのである。*1

これには、ブラウン管モニターの特性に関する歴史的事情が関わっているのだけれども、深くは立ち入らない。大事なのは、rgb(128, 128, 128)が半分の明るさだと思ってプログラムを書くと、グレーが暗くなってしまうということだ。だから、暗くなる分を考慮して、明るめの画像を表示しないといけない。そのような補正処理を、「ガンマ補正」と言う。

Windowsのフォントレンダリングは、ガンマ補正が2重、3重に掛かっている

おそらく、Windowsのフォントレンダリングにおいてもガンマ補正が行われているのだが、どういうわけかガンマ補正が多重に掛かっているようだ。つまり、グレーを明るくする処理を重ねたためにグレーが明るくなりすぎている。(rgb(128, 128, 128)を補正してrgb(188, 188, 188)になるはずが、rgb(223, 223, 223)やrgb(240, 240, 240)になっている。)

参考として、GIMPのレベル補正機能を使ってガンマ補正を逆向きに(グレーが暗くなるように)行った画像を載せる。指定した0.46, 0.21というのは、ディスプレイのガンマ値2.2の逆数と、その2乗だ。


20161111005506
Firefoxで表示したものにガンマ補正(0.46)を掛けたもの


20161111005650
メモ帳で表示したものにガンマ補正(0.21)を掛けたもの

字のかすれが解消され、全体が同じ濃さの文字になっているのが分かるだろうか。この結果から、ブラウザーに関してはガンマ補正が2重に、メモ帳に関しては3重に行われていると考えられる。(※このことに関して追記あり

游ゴシック細字は本来この程度の黒さで表示されるべきなのであり、ただ細すぎるから薄くて読みづらいという話ではない。太くすると読めるようになるのは、グレーの領域が少なく、ガンマ補正が適切でないのが誤魔化されるだけであり、Windowsのフォントレンダリングが適切でないことには違いない。将来的にはガンマ補正を修正して、細い字もムラなくちゃんと表示できるようになるように改善してほしいと思う。

追記

追記2

ブックマークコメントでも意見を頂きましたが、メモ帳のようなGDIでClearTypeを使ってレンダリングしているケースに関しては、ClearTypeの設定によって表示が変わるようです。自分もメイリオ初期設定から変更していたように思います。なので、3重に補正が掛かっているというのは誤解で、たまたまそう見えるガンマ値が設定されていただけであるようです。

*1:色空間がsRGBの場合

プログラムを哲学する 2. 「概念記法」

以前、言語の完全性について言及した。今回は引き続き、言語の完全性について考える。

mandel59.hateblo.jp

フレーゲの「概念記法」

フレーゲは未定義の式の存在を「言語の不完全性」(einer Unvollkommenheit der Sprache)とみなしていた。論理学者のフレーゲにとって、表現の「意味」(Bedeutung; その記号があらわしている事物。表記対象 denotation や言及対象 referent に相当すると考えられる)が確定していることは重要なことであった。表現の「意味」は、ちょうど1つでなければならず、それより多くても、少なくてもいけない。*1そのような多義的ないし無意味な表現は論理的誤謬のもととなるので、学問から排除するべきだと考えた。

フレーゲの提案した「約定」(Festsetzung)とは、そのような「言語の不完全性」を排し、言語を完全化する方法である。ある表現に「意味」が複数考えられる場合や「意味」が考えられない場合には「約定」を行うことで、あらゆる文法的に正しい表現の「意味」をただひとつに定める。簡単に言えば、「意味」がないなら(「意味」が多いなら)、「意味」を決めてやればいいというようなことだ。

数学では「√」という記号は正の平方根を表すと決めることによって、「 \sqrt{4}」が 2だけを表すとし、 {-2}をも同時に表すことを退けているが、これも一種の「約定」だと言える。「言語の不完全性」を「約定」により避け、あらゆる表現の「意味」をただひとつに確定した「論理的に完全な言語」(einer logisch vollkommenen Sprache)をフレーゲは構想し、それを「概念記法」(Begriffsschrift)と呼んだ。フレーゲは、「言語の完全性」を達成するために、「概念記法」に次の要求を行った。

論理的に完全な言語(概念記法(Begriffsschrift))に対しては、すでに導入された記号から文法的に正しい方法によって固有名として構成された表現はすべて、実際上ある対象を表示することと、いかなる記号もそれに対する意味が保証されることなしに新たに固有名として導入されることはないという二つのことが求められている。[1]

ここで挙げられている要求は、おおむね〈構成性〉と〈原子確定性〉に相当する。(これらの用語は以前 Referential Transparencyの代わりに使える概念案 - Ryusei’s Notes (a.k.a. M59のブログ) で導入したものだ。)「概念記法」を規定する「約定」すべてに〈構成性〉と〈原子確定性〉を要求することで、「概念記法」全体の「論理的な完全性」=〈確定性〉を実現できる。*2

フレーゲの「約定」は表現の「意味」を唯一に定めることに主眼があるため、個々の「約定」に論理上の根拠は存在しない。むしろ、論理上の根拠が与えられないからこそ、約定によって表現の意味を決めるというのだろう。「約定」に論理上の根拠がなくとも、その「約定」が〈構成性〉と〈原子確定性〉を満たす形で行われるのであれば、どう「約定」しようとも「概念記法」全体の〈確定性〉は保証され、矛盾が生じることはなく、論理上は問題がない。

例えば、フレーゲ解析学の記号の「不完全性」を示す例として発散級数(収束値を持たない級数)を挙げ、発散級数はは数0を表すと「約定」することによって、この「不完全性」を排除することに言及している。この数0による「約定」はあくまでも例で、根拠があると言えないが、〈構成性〉と〈原子確定性〉を満たすどのような「約定」を行っても、矛盾が生じることはない。

出典

[1] フレーゲ, ゴットロープ (1986) 「意義と意味について Über Sinn und Bedeutung」(土屋 俊 訳), 坂本百大 編『現代哲学基本論文集』 1, p. 26, 勁草書房.
ドイツ語の表現はGottlob Frege. Über Sinn und Bedeutungから適宜引用

*1:フレーゲは命題文の「意味」とは真理値だと考えたから、命題文の「意味」は必ず真か偽かのどちらか一方だということでもある。

*2:追記:厳密には、原子式の意味が決定されるためには原子式の文脈が決定される必要があるため、〈文脈確定性〉も要る。

Windows 10 導入作業

Windows 10を導入する上でやったこと

ディスプレイの色調整

液晶の白が青かぶりしている感じだったので、ディスプレイの詳細設定から色設定を行う。

開発者向け機能

更新とセキュリティから、開発者向け機能に関する設定を行う

PackageManagement

ソフトウェア開発に使う各種ツール群をコマンドラインからインストール

Git for Windows

PackageManagement+chocolateyで入れるとデフォルトで改行コードの変換が行われる設定になるのでgit config --global core.autocrlf=falseしておく。

Visual Studio Code

{
  "editor.tabSize": 2,
  "editor.renderWhitespace": true,
  "files.eol": "\n",
  "terminal.integrated.shell.windows": "C:\\Windows\\System32\\WindowsPowerShell\\v1.0\\powershell.exe"
}

Suica専用自販機に見る形骸化した記号の話



この話を見た時、これはまさに「形骸化した記号」のよい例だろうと思った。ナンセンスな「電子署名」の話よりも、それが形骸であることがずっと分かりやすい。

普段から自販機を使っている大多数の日本人にとって、それがコイン投入口だということを認知するためにコインの絵や点字は必要ではなく、無意識に見過ごされた記号であったのだろう。だから、実際に困る人が現れるまでは、誰も気づくはずがなかった。

それで、教訓として得るべきなのはなんだろうか。マイノリティーへの配慮を充実させること? まあ、それはそうだろう。多様性を持つ利用者全般に対して不都合のないデザインであるか、よくテストを行うべきだと言える。アクセシビリティガイドラインを守り、マイノリティーを尊重し、適切なテストを行った後にプロダクトを出すのが理想だ。問いたいのは、理想を実現させるにはどうすればよいのかということだ。

あらゆるマイノリティーに対してアクセシビリティ上の困難がないかテストをするには多大なコストが掛かる。それは必要なコストだ、と頭で分かるとしても、感情が付いてこない。マジョリティーはマイノリティーに対する意識を高めなければならないのだけれども、それはアクセシビリティガイドラインを頭に叩き込むだけでは成しようがない。必要なのは、ルールの遵守というよりも、記号を多様な観点から見ることができる柔軟さだ。

記号の不完全さへの意識を高めるのに、笑いは重要な役割を果たしうる。私たちは記号を信用し、時に記号に裏切られる。記号の解釈には文化による差異があり、それによって起こる勘違いは、記号が引き起こす悲喜劇だ。記号はコミュニケーションのなかだちだけど、それが勘違いの種であり、常に不完全さを孕むことを認めよう。未知の存在との交流は常に勘違いの連続だ。私たちは記号と、記号が引き起こす勘違いを互いに笑いながら、少しずつ乗り越えていくしかない。異文化交流とは、寛容性を前提としなければ成し得ないと思う。

東京メトロの行先案内の多言語化で全言語にルビが付いていて賢いという話(だけど限界もある)




ルビ(振り仮名)が振ってあると、すごく日本っぽい感じがする。ハングル一色の画面を見れば、異形の文字を見慣れない人には忌避感を与え、ここは日本だぞと文句を付けたくもなるっていう人が出てくるんだろうけれども、ハングルに振り仮名するだけで、そういう人にとっても、なんだ日本語じゃないかと思えてくるのではないか。たぶん。まあ、それでも文句を付ける人は付けるんだろうけれども。

ルビは、昔から漢字と仮名を併用してきたからこそ生まれた、日本独特の組版文化だと言える。もちろん、発音を併記するのは中国語学習用のテキストとかでもやることではあるのだけれども、日本語のようにルビを常用する文化は他にないだろう。漢字と仮名という複数のチャンネルを使って情報を流すことで、字義と音価、あるいは意味と意味が新しい形で結びつく。そのことが、言葉を新しい視点から眺めることを教えてくれる。

ルビの欠点として、ルビは小さい。視力に自信がない人は、やっぱり平仮名の大表示も欲しいって思うだろう。そして、ルビを振ると画面が煩雑になる。大きな表示スペースがないと難しい。万人にとって良い画面を設計するのはほぼ不可能なことで、どうしたって切り捨てが生じてしまう。液晶ディスプレイによる時分割表示は、多言語対応の万能薬ではない。

そもそも、公共のディスプレイに表示しようとするから、万人が読める表記という難題を解かなければならないのであって、一番いいのは、個々人に最適化された案内表示がなされることだろう。スマートフォンに表示する分には、他人の目を気にすることなく、自分の都合のよい表示方法に設定できるはずだ。案内情報を局所的に配信する仕組みは絶対に必要だと思うのだけれども、誰か真剣に取り組んでくれないだろうか。

花押の件について判決文を読んでみたけどよく分からなかった話

www.jiji.com

今回の裁判の要旨は「いわゆる花押を書くことは,民法968条1項の押印の要件を満たさない」ということですが、その理由を抜き出してみます。

 3 原審は,次のとおり判断して,本件遺言書による遺言を有効とし,同遺言により被上告人は本件土地の遺贈を受けたとして,被上告人の請求を認容すべきものとした。
 花押は,文書の作成の真正を担保する役割を担い,印章としての役割も認められており,花押を用いることによって遺言者の同一性及び真意の確保が妨げられるとはいえない。そのような花押の一般的な役割に,a家及びAによる花押の使用状況や本件遺言書におけるAの花押の形状等を合わせ考えると,Aによる花押をもって押印として足りると解したとしても,本件遺言書におけるAの真意の確保に欠けるとはいえない。したがって,本件遺言書におけるAの花押は,民法968条1項の押印の要件を満たす。
 4 しかしながら,原審の上記判断は是認することができない。その理由は,次のとおりである。
 花押を書くことは,印章による押印とは異なるから,民法968条1項の押印の要件を満たすものであると直ちにいうことはできない。
 そして,民法968条1項が,自筆証書遺言の方式として,遺言の全文,日付及び氏名の自書のほかに,押印をも要するとした趣旨は,遺言の全文等の自書とあいまって遺言者の同一性及び真意を確保するとともに,重要な文書については作成者が署名した上その名下に押印することによって文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保することにあると解されるところ(最高裁昭和62年(オ)第1137号平成元年2月16日第一小法廷判決・民集43巻2号45頁参照),我が国において,印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い。
 以上によれば,花押を書くことは,印章による押印と同視することはできず,民法968条1項の押印の要件を満たさないというべきである。

http://www.courts.go.jp/app/hanrei_jp/detail2?id=85930

読みづらいので、箇条書きにして原審の判断と最高裁の判断を整理してみます。

原審の判断:

  • (1.) 花押は,文書の作成の真正を担保する役割を担い,印章としての役割も認められており,花押を用いることによって遺言者の同一性及び真意の確保が妨げられるとはいえない
  • (2.) そのような花押の一般的な役割に,a家及びAによる花押の使用状況や本件遺言書におけるAの花押の形状等を合わせ考えると,Aによる花押をもって押印として足りると解したとしても,本件遺言書におけるAの真意の確保に欠けるとはいえない
  • (結論1.) したがって,本件遺言書におけるAの花押は,民法968条1項の押印の要件を満たす

原審では押印の要件をどのように考えていたのかが抜けているので、これだけでは妥当な論証にはなっていません。原審の判決文を確認する必要がありそうです。

最高裁の判断:

  • (3.) 花押を書くことは,印章による押印とは異なる
  • (4.) (3.)から,〔花押を書くことは,〕民法968条1項の押印の要件を満たすものであると直ちにいうことはできない
  • (5.) 民法968条1項が,自筆証書遺言の方式として,遺言の全文,日付及び氏名の自書のほかに,押印をも要するとした趣旨は,(5-1.)とともに,(5-2.)にあると解される
    • (5-1.) 遺言の全文等の自書とあいまって遺言者の同一性及び真意を確保する〔こと〕
    • (5-2.) 重要な文書については作成者が署名した上その名下に押印することによって文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保すること
  • (6.) 我が国において,印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い
  • (結論2.) 花押を書くことは,……民法968条1項の押印の要件を満たさないというべきである

この論証は妥当な論証ですが、結論を導くのに必要なのは(5.)の〈(5-1.)と(5-2.)をともに満たす⇔押印の要件を満たす〉という趣旨の命題と(6.)の〈花押を書くことは(5-2.)を満たさない〉という趣旨の命題だけです。(3.)と(4.)は、それが否定されると結論も否定されるような命題です。

論証自体は妥当ですが、そこに挙げられている前提(5.), (6.)は妥当なのでしょうか。

(5.) の主張のために「最高裁昭和62年(オ)第1137号平成元年2月16日第一小法廷判決」が参照されていますが、この裁判の要旨は「自筆遺言証書における押印は、指印をもつて足りる」ということです。こちらも、その理由を抜き出してみます。

 自筆証書によつて遺言をするには、遺言者が遺言の全文、日附及び氏名を自書した上、押印することを要するが(民法九六八条一項)、右にいう押印としては、遺言者が印章に代えて拇指その他の指頭に墨、朱肉等をつけて押捺すること(以下「指印」という。)をもつて足りるものと解するのが相当である。けだし、同条項が自筆証書遺言の方式として自書のほか押印を要するとした趣旨は、遺言の全文等の自書とあいまつて遺言者の同一性及び真意を確保するとともに、重要な文書については作成者が署名した上その名下に押印することによつて文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保することにあると解されるところ、右押印について指印をもつて足りると解したとしても、遺言者が遺言の全文、日附、氏名を自書する自筆証書遺言において遺言者の真意の確保に欠けるとはいえないし、いわゆる実印による押印が要件とされていない文書については、通常、文書作成者の指印があれば印章による押印があるのと同等の意義を認めている我が国の慣行ないし法意識に照らすと、文書の完成を担保する機能においても欠けるところがないばかりでなく、必要以上に遺言の方式を厳格に解するときは、かえつて遺言者の真意の実現を阻害するおそれがあるものというべきだからである。もつとも、指印については、通常、押印者の死亡後は対照すべき印影がないために、遺言者本人の指印であるか否かが争われても、これを印影の対照によつて確認することはできないが、もともと自筆証書遺言に使用すべき印章には何らの制限もないのであるから、印章による押印であつても、印影の対照のみによつては遺言者本人の押印であることを確認しえない場合があるのであり、印影の対照以外の方法によつて本人の押印であることを立証しうる場合は少なくないと考えられるから、対照すべき印影のないことは前記解釈の妨げとなるものではない。そうすると、自筆証書遺言の方式として要求される押印は拇印をもつて足りるとした原審の判断は正当として是認することができ、原判決に所論の違法はない。論旨は、採用することができない。

http://www.courts.go.jp/app/hanrei_jp/detail2?id=52210

平成元年の判決の判断:

  • (結論3.) ……押印としては、遺言者が印章に代えて拇指その他の指頭に墨、朱肉等をつけて押捺すること(以下「指印」という。)をもつて足りるものと解するのが相当である
  • (7.) 同条項が自筆証書遺言の方式として自書のほか押印を要するとした趣旨は、(7-1.)とともに、(7-2.)にあると解される
    • (7-1.) 遺言の全文等の自書とあいまつて遺言者の同一性及び真意を確保する〔こと〕
    • (7-2.) 重要な文書については作成者が署名した上その名下に押印することによつて文書の作成を完結させるという我が国の慣行ないし法意識に照らして文書の完成を担保すること
  • (8.) 右押印について指印をもつて足りると解したとしても、遺言者が遺言の全文、日附、氏名を自書する自筆証書遺言において遺言者の真意の確保に欠けるとはいえない
  • (9.) いわゆる実印による押印が要件とされていない文書については、通常、文書作成者の指印があれば印章による押印があるのと同等の意義を認めている我が国の慣行ないし法意識に照らすと、文書の完成を担保する機能においても欠けるところがない
  • (10.) (9.)ばかりでなく、必要以上に遺言の方式を厳格に解するときは、かえつて遺言者の真意の実現を阻害するおそれがあるものというべき〔である〕

(5.)は(7.)を参照していて、ほとんど同じ表現であることがわかります。(7.)の〈(7-1.)と(7-2.)をともに満たす⇔押印の要件を満たす〉という趣旨の命題は、(8.)の〈指印は(7-1.)を満たす〉、(9.)の〈指印は(7-2.)を満たす〉という趣旨の命題と合わせて、(結論3.)を妥当に導くための前提になっています。

(7.)が指印が印章の代わりになることを主張する際に考えられた前提であるのに対し、それを今回の判決の(5.)は逆に使われていて、花押が印章の代わりにならないことを主張するための前提になっていますが、主張(5.)自体は妥当で「押印の要件」つまり押印であると認められる必要十分条件になっていると思われます。そうすると、問題になるのは(6.)です。

(6.)は単に原審における前提(1.)の「印章としての役割も認められており,」を否認しているだけのように見えます。(原審の判決文は確認できていないので、原審で認められた「印章としての役割」が具体的にどのような役割を指しているのかははっきりしませんけれども。)そして、その前提にさらなる理由は与えられていません。

結局、判決文を読んで分かったのは、最高裁判所は「我が国において,印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存するものとは認め難い」という判断を行ったが、その判断には全く理由が与えられていないということでした。なぜ、こんなよく分からない判決文が許されているんでしょうか。「印章による押印に代えて花押を書くことによって文書を完成させるという慣行ないし法意識が存する」かどうかについて、十分審議が尽くされたのでしょうか。審議するまでもなく自明だという認識なんでしょうか。そこら辺が、よく分かりませんでした。

リファレンス

シンタックス・ハイライト機能はHaxeに対応してほしいです。

お題「シンタックス・ハイライト機能で対応してほしい言語」

Haxeに対応してほしいです。

class Test {
    static function main() {
        trace("Haxe is great!");
    }
}

HaxeActionScript風のシンタックスを持ちながらも、JavaScriptC#, PHPなど多数のターゲットに対してコードをトランスパイルすることができる言語です。

Flashとの互換性を持つOpenFLというフレームワークを抱えていたり、言語のオリジナル開発者がゲームデベロッパーで性能を重視した言語であるという面も関係して、ポストFlash時代におけるゲーム開発プラットフォームとして採用事例が多数存在しています。

また、複数ターゲットに出力可能であることから、クライアント側とサーバー側で共通のコードを利用することが可能だという点も魅力です。

文脈付き構成的意味論を構成的意味論に変換する

mandel59.hateblo.jp

ここでは, 自然数の集合  {\bf N} に0を含めることとする。

記法  \left ( a_k \right )_{k=m}^{n} \left (a_m, a_{m+1}, \cdots, a_{n-2}, a_{n-1} \right ) を表す。 m = n の時は  \left ( \right ) を表す。
記法  \bigwedge_{k = m}^{n} p_k p_m \wedge p_{m+1} \wedge \cdots \wedge p_{n-2} \wedge p_{n-1} を表す。 m = n の時は  \top (真理値の真)を表す。

形式言語

形式言語  L = \langle F, | \bullet | \rangle は関手集合  F, 関手の項数  | \bullet | : F \rightarrow {\bf N} からなる組である。

形式言語  L = \langle F, | \bullet | \rangle の式集合  E(L) を, つぎの帰納的定義によって定める:

  •  f \in F \land \left ( \bigwedge_{k = 0}^{|f|} t_k \in E(L) \right ) \Rightarrow f(t_k)_{k=0}^{|f|} \in E(L).

これは, 次のようなことを含意している:

  •  f が項数  n の関手であり,  t_0, \cdots, t_{n-1} が式であるとき,  f(t_0, \cdots, t_{n-1}) は式である。
    • 特に,  f が項数  0 の関手であるとき,  f() は式である。
  •  t が式であるとき, ある自然数  n, ある項数  n の関手  f, ある式  t_0, \cdots, t_{n-1} が存在し,  t = f(t_0, \cdots, t_{n-1}).

構成的意味論

構成的意味論  \Sigma = \langle L, M, I \rangle形式言語  L = \langle F, | \bullet | \rangle, 意味集合  M, 解釈  I : f \in F \mapsto g \in [ M^{|f|} \rightarrow M ] からなる組である。

このとき  \Sigma のもとの式の意味  \Sigma \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow M を, つぎの帰納的定義によって定める。

  •  \Sigma \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I(f) \left ( \langle \Sigma \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )

文脈付き構成的意味論

文脈付き構成的意味論  \Sigma_\star = \langle L, C, V, I_\star \rangle形式言語  L = \langle F, | \bullet | \rangle, 文脈集合  C, 値集合  V, 解釈  I_\star : f \in F \mapsto g \in [ [ C \rightarrow V ]^{|f|} \rightarrow [ C \rightarrow V ] ] からなる組である。

このとき  \Sigma_\star のもとの式の意味  \Sigma_\star \unicode{x27e6} \bullet \unicode{x27e7} : E(L) \rightarrow [ C \rightarrow V ] \ を, つぎの帰納的定義によって定める。

  •  \Sigma_\star \unicode{x27e6} f(t_k)_{k=0}^{|f|} \unicode{x27e7} = I_\star(f) \left ( \langle \Sigma_\star \unicode{x27e6} t_k \unicode{x27e7} \rangle_{k=0}^{|f|} \right )

文脈  c \in C のもとの式  e の値は  \Sigma_\star \unicode{x27e6} e \unicode{x27e7} (c) \ になる。

文脈付き構成的意味論を構成的意味論に変換する

文脈付き構成的意味論  \Sigma_\star = \langle L, C, V, I_\star\rangle から自明な構成的意味論  \Sigma ' _\star = \langle L, [ C \rightarrow V ], I_\star \rangle を構成できる。

プログラム意味論の分かりやすい紹介

巷に膾炙しているプログラム意味論の説明は、正直言って何を言っているのか、部外者にはよく分からないように感じられる。プログラムの意味を論じる「プログラム意味論」の意味がよくわからないというのは本末転倒だろう。ここでは、プログラム意味論を分かりやすく紹介したい。

プログラムの意味

プログラム意味論とは、プログラムの意味に関する理論だ。

そもそも「意味」とはなんだろうか。「意味」の意味を知るために、デジタル大辞泉で調べてみよう。

言葉が示す内容。また、言葉がある物事を示すこと。「単語の―を調べる」「愛を―するギリシャ語」

ある表現・行為によって示され、あるいはそこに含み隠されている内容。また、表現・行為がある内容を示すこと。「慰労の―で一席設ける」「―ありげな行動」「沈黙は賛成を―する」

価値。重要性。「―のある集会」「全員が参加しなければ―がない」

いみ【意味】の意味 - goo国語辞書

「意味」の語義が3つ示されているが、要約すると、ひとつめは「言葉が示す物事」、ふたつめは「行為が示す物事」、みっつめは「行為が持つ価値」だ。この3つの「意味」の意味は無関係なものではなく、共通した構造が存在している。それは、何か言葉や行為という表に見えている表現は、その裏にある物事や価値に繋がっているという構造だ。

たとえば、店で「ビールあり〼」という看板を見たとする。ビールの実物を見ずとも、その店には実際にビールが用意されていて、店はそのビールを売る意図があって、自分はそれを注文して飲むことができるという場面を想像できる。その想像された場面や、その場面の持っている価値が、「ビールあり〼」の意味だと言える。

プログラムの意味も同様だ。プログラムの意味とは、そのプログラムによって実現される物事や場面のことだと言える*1。例えばalert(1)というJavaScriptのプログラムは、実行するとダイアログ・ボックスで“1”を表示する。すなわち、alert(1)の意味は「ダイアログ・ボックスで“1”を表示する」という場面だ。

プログラムの意味は、そのプログラムを動かしてみれば分かるように思うかもしれないが、プログラムを動かすにもコストやリスクが存在する場合がある。誤作動を起こすプログラムを実際に動かしてしまえば、重大な事故を引き起こすかもしれない。それを避けるためには、プログラムを動かすことなく、その意味を知る必要があるのだ。

優れたプログラマーが頭の中で考えたプログラムを一発で動かしてしまうのも、プログラムの意味を体得しているからだと言える。しかし、プログラムの意味を個人の経験によって身に付けるのは時間がかかるだけではなく、その厳密さにも限界がある。見慣れない種類のプログラムがどのように動くかは、経験からでは分からないのだ。そういう場合でも、プログラム意味論でプログラムの表現と物事の間にある関係を詳細に学ぶことで、プログラムの意味を正確に把握できるようになるだろう。

形式的意味論

意味論は表現と物事の対応を論じるものではあるけれど、現実の物事はすごく複雑で、それをありのままに考えて厳密に論じるのはとても難しい。そこで、普通は物事を抽象化した上で、厳密に考えることになる。*2物事を抽象化した上で、数学や論理学を使って厳密に論じられる意味論が、形式的意味論だ。形式的意味論には操作的意味論、表示的意味論、公理的意味論といった大別がある。

操作的意味論は、表現を操作する規則や抽象機械を使ってプログラムの意味を考える。この意味論では表現の操作過程や抽象機械の動作が、表現の意味となる。この意味論は、現実のコンピューターの動作に一番近い形で表現された意味論で、プログラムに対して、機械がどれほどの計算資源を使い、どのように動作するのかを厳密に議論するのに適した表現だと言える。その一方で、操作的意味論が扱った規則以外の方法でプログラムを処理することについては考慮しないので、プログラムの読みやすさや編集しやすさを議論するには適していないだろう。

表示的意味論は、表現から物事への写像(表示)を使ってプログラムの意味を考える。この意味論においては、表現からの写像が定義できる好きな領域を意味としてよい。この手法は、言語の意味を数理論理学や言語哲学と同様の手法を用いて考えており、プログラムを読み書き・編集するときの性質を分析するのに向いている。例えばプログラミング言語が「構成性」という性質を持っていることが意味論から分かるので、その性質を利用したプログラムの最適化を行う、といったことに使える。

公理的意味論は、表現と物事の間に成り立つ関係(仕様)を使ってプログラムの意味を考える。この意味論においては、仕様を公理として証明できる物事が、表現の意味となる。この意味論では、仕様にないプログラムの具体的な動き方は分からないが、プログラムの「停止性」のような抽象度のより高い性質を証明するのに向いている。

*1:「実行結果」と言ってしまえば済むように思うが、サーバーのように継続的に実行され続けるプログラムや、ギャンブル・ゲームのように非決定的な振る舞いをするプログラムもあるわけで、そのようなプログラムの意味も考えようとすると、単に「実行結果」と言うだけでは済まない。

*2:ここで「厳密に論じる」と言っているのは、他人に自分の論理を説明できる形で、論理的に論じるということだ。論じる問題が複雑になると、関係しあう事柄の組み合わせが爆発的に増えるせいで、論理を構成するのが極端に難しくなってしまう。だから、抽象化を行うことで一度に考える事柄を減らし、問題を厳密に論じきれる大きさにする必要がある。

プログラミングと哲学

プログラミングと哲学の間には深い関係がある。プログラミングが昔ながらの哲学と単純に対応するというわけではないけれども、だからといって全くの無関係というわけでもない。その理由として、プログラミングの方法論のひとつに、世界を分析し、それを記述するという方法でプログラムを書くという考えがあることが挙げられる。

それはまさにオブジェクト指向の理念である、と考える人は、プログラミングのことも哲学のこともよく知らない。世界の様子を記述するという性質はオブジェクト指向の専売特許などではなく、平叙型プログラミング*1に共通して見られる考えだ。すなわち、関数型プログラミングや論理型プログラミングもまた、世界の様子を記述する側面を持っている。

「世界を分析して記述する方法」というのは、古来哲学が対象としてきたことのひとつだ。それなら、哲学なんてプログラミングと関係ないとするほうが、伝統に則らない考えだというべきだろう。分かりやすい例として、論理型プログラミングと分析哲学の関係を挙げる。論理型プログラミングの記法は記号論理学に由来するが、遡ればフレーゲの「概念記法」にたどり着く。フレーゲは一方で分析哲学の祖ともされるが、フレーゲ分析哲学とは、概念記法の背景にある考えを記述したものに他ならない。

あなたが論理学や論理型プログラミング言語を使っている時、あなたはその背景にある「世界の分析方法」をも、気づかないうちに体得している。そういう無意識のうちに使っている考え方を、哲学者は積極的に言語化してくれているのだ。分析哲学を知らなくても論理学を使えるかもしれないが、分析哲学を知ることで論理学自体をよりよく知ることができる。

プログラミングと哲学を結びつけて考えるというのは、古臭い考えを無批判に受け入れるということでもなければ、突飛なこじつけをするというものでもない。むしろその反対だ。自分が無意識に使っている概念があることを既存の哲学を通して自覚することで、プログラミングをより深く理解し、批判的に接することができるようにする。古い哲学が自分の考え方を完全に説明していると思われなければ、新しく考えを付け足していく。そういう営みを意識的に行うことが、プログラミングと哲学を結びつけて考える意義だろうと思う。

*1:declarative programming. 定訳は「宣言型プログラミング」だが、言語学では「命令文 imperative sentence」「平叙文 declarative sentence」と言うのだから、当然「命令型プログラミング imperative programming」に対して「平叙型プログラミング」と訳すべきだ。

Referential Transparencyの代わりに使える概念案

Referential Transparencyという概念が指すものは漠然としているので、もっと意味が明瞭で使いやすい用語を定義し、色々な言語の性質を記述してみる。

前提として

  • 式は原子式か複合式である。
  • 複合式は関手(functor)と項(argument)から構成される。
〈純粋性〉
「式の意味」と「式の値」は同義である。
〈原子確定性〉
原子式の意味は原子式自身とその原子式の文脈から決定される。
〈構成性〉
複合式の意味は関手および項の意味から決定される。
〈弱構成性〉
複合式の意味は関手、項の意味および式の文脈から決定される。
〈文脈構成性〉
複合式の項の文脈は、その複合式の文脈と関手から決定される。
〈文脈弱構成性〉
複合式の項の文脈は、その複合式の文脈、関手および他の項の意味から決定される。
〈確定性〉
式と式の文脈から部分式の意味が決定される。
〈文脈確定性〉
式と式の文脈から部分式の文脈が決定される。
〈文脈同一性〉
部分式は式全体と同じ文脈を持つ。
〈同値置換可能性〉
部分式を、その式と同値の別の部分式に置き換えても、式全体は同じ意味を持つ。
  • 関手がすべて全関数である数式は〈原子確定性〉〈構成性〉〈文脈同一性〉を持つので、〈確定性〉がある。たとえば、 \{ a \mapsto 2, b \mapsto 3 \}という文脈において、式 a + bは確定した値 5を持つ。また、同じ変数は、ひとつの式の中では常に同じ値を指す。
  • C言語においては普通「式の値」でなく、副作用を含めた「式の動作」が「式の意味」だと考えるので、C言語は〈純粋性〉を持たないと言える。
  • Haskellにおいては普通「式の値」が「式の意味」だと考えるので、Haskellは〈純粋性〉を持つと言える。
  • 関手がすべて全関数である数式に非再帰的なlet式を加えても〈原子確定性〉〈弱構成性〉〈文脈弱構成性〉〈確定性〉は保たれる。

(〈弱構成性〉は、レカナティの「語用論的構成性」と同様の概念か。 http://www.wakate-forum.org/data/tankyu/42/42_09_takaya.pdf

Referential Transparencyについて取り急ぎ

Wikipedia日本語版に

参照透過性(さんしょうとうかせい、英: Referential transparency)は、計算機言語の概念の一種で、文脈によらず式の値はその構成要素(例えば変数や関数)によってのみ定まるということを言う。

https://ja.wikipedia.org/w/index.php?title=%E5%8F%82%E7%85%A7%E9%80%8F%E9%81%8E%E6%80%A7&oldid=46720534

とあるが、これは誤り。「文脈によらず式の値はその構成要素によってのみ定まる」という性質は、参照透過性ではなく構成性 (compositionality) と言う。

In mathematics, semantics, and philosophy of language, the principle of compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them.

https://en.wikipedia.org/w/index.php?title=Principle_of_compositionality&oldid=646872914

The meaning of a complex expression is determined by its structure and the meanings of its constituents.

http://plato.stanford.edu/entries/compositionality/

参照透過性は、英語版Wikipediaによれば次の性質だ。

An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).

ある式は、その式をその式の値に置き換えてもプログラムの動作が変わらないとき(いいかえれば、同じ入力に対して同じ作用と出力を持つプログラムになるとき)、参照透過であるという。

https://en.wikipedia.org/w/index.php?title=Referential_transparency&oldid=709215227

(この定義が正しいとは限らないが、日本語版の説明と食い違っていることは明らかだ。)

問題をややこしくするのは、式 (expression)、意味 (meaning) 、表現 (representation)、正規形 (regular form)、表示 (denotation)、参照 (reference)、値 (value)、動作 (behavior) といった用語が、文脈によってそれぞれ同義になったりならなかったりして、混同されるというところだ。それについては別に整理してまとめることにする。