Yabu.log

ITなどの雑記

論理学をつくる練習問題80(2)解答

論理学

本に回答が乗っておらず、ネットに載せておく意義があると思ったので公開。 練習問題80(2)はND公理系(自然演繹)で式集合が矛盾するか、どうかの解答と矛盾していればそれを証明(自然演繹で示す)をする問題。 (a),(b),(c)とあるが式集合は全て矛盾しているためその証明(自然演繹による⊥の導出)のみを示す。

※間違ってたらすいません

論理学をつくる

論理学をつくる

問題

Γ⊢NDA, Γ⊢ND¬Aなる論理式Aがあるとき、ΓをND矛盾しているということにする。次の うちND矛盾している論理式の集合はどれか、そしてそれがND矛盾していることを示せ。

  • (a) {P∨Q, ¬P→Q, ¬P}
  • (b) {P∨Q, ¬(P∧Q), P↔︎Q}
  • (c) {P→Q, P, ¬Q}

回答

(a)

P∨Q      Prem
¬P→¬Q    Prem
¬P        Prem
--------------
¬P→¬Q    Rep
¬P        Rep
¬Q        → elim

    Q    Prem
    ---------
    ¬Q    Reit
    ⊥    ¬intro*

Q→⊥    →intro

    P    Prem
    ---------
    ¬P   reit
    ⊥   ¬intoro*

P→⊥   →intro
Q→⊥   Rep
P∨Q    Rep
⊥      ∨elim

ポイント:演繹三行目で∧intoroをつかって¬P∧¬Qを導けるが、これが前提のP∨Qと矛盾していることは明らか(真理値表を書けば真になる割当が見つからない)。またド・モルガンの法則により¬P∧¬Q = ¬(P∨Q))だが、自然演繹に¬P∧¬Q,P∨Qから⊥を導くルールがなく、自然演繹の中のルールで他の式から⊥を導く必要がある。

(b)

P∨Q       Prem
¬(P∧Q)    Prem
P↔Q       Prem
---------------
    P    Prem
    ---------
    P↔Q    Reit
    Q       ↔elim
    P∧Q    ∧intro

P→(P∧Q)    →intro
     
    Q    Prem
    ---------
    P↔Q    reit
    P       ↔elim
    Q       Rep
    P∧Q    ∧intro

Q→(P∧Q)    →intro
P→(P∧Q)    Rep
P∨Q         Rep
P∧Q         ∨elim
¬(P∧Q)      rep
⊥           ¬intoro*

(c)

一番簡単と解答に書いてあったやつ。これを(a)にして最初に解かせてほしかったな。

P→Q
P
¬Q    Prem ⊥
--------------
P→Q    Rep
P       Rep
Q       →elim
¬Q      Rep
⊥      ¬intor*

なにかあればコメントください。

ちなみに、論理学をつくるはまだ挫折しておらず、ノートをサブブログの方に書き出しています。Twitterやめた僕が悪いんだけど、アクセス数3とかなので悲しい(涙)

yuyubu-sub.hateblo.jp

フィッチスタイルの自然演繹のやり方

論理学

完全に個人のメモ。復習+忘れた時に思い出す用。範囲としては論理学をつくるp214~p235。気が向いたら述語を自然演繹で導出対象にするやり方も書くかも。

論理学をつくる

論理学をつくる

式集合の充足可能性の検査には真理表、タブロー、などの複数のやり方があり、自然演繹もそれの一種。

導出線と前提棒

(1) P → Q (前提)
(2) Q → R (前提)
(3) R → S (仮定)
(4) P      (仮定)
(5) Q      (4)と(1)より {P → Q, P}
(6) R      (2)と(5)より {Q → R, Q}
(7) S      (3)と(6)より {R → S, R}
(8) P → S (4)と(7)より {P⊨S}
(9) (R → S) → (P → S) (3)と(8)より

上記だとどの式がどの前提に依存しているのかわかりにくい。 仮定が生きてるスコープを表すために、導出線、仮定の宣言に前提棒というシンタックスを導入する

  • パソコンでノートを作る都合上、導出線をインデントで表す。
  • 前提棒を式下の---------で表す。
(1) P → Q (前提)
(2) Q → R (前提)
-----------
    (3) R → S (仮定)
    -----------
        (4) P      (仮定)
        ------
        (5) Q      (4)と(1)より {P → Q, P}
        (6) R      (2)と(5)より {Q → R, Q}
        (7) S      (3)と(6)より {R → S, R}
    (8) P → S (4)と(7)より {P⊨S}
(9) (R → S) → (P → S) (3)と(8)より
  • 導出棒上の演繹は自分が書かれた導出棒より浅い(左)に存在する前提を参照することはできない。

演繹規則

表記

  • 適応した演繹規則を導出した論理式の右側にやや空白をあけて表記する
    • 本ブログではスペース4個とする
  • みやすさの観点から、同じ階層の導出ではこの規則表記を一番長い論理式のスペースに合わせる
例

P       Prem
P→Q    Prem
Q       →elim

前提規則(premiss rule:Prem)

  • (1)導出開始時の最初の前提棒状に書ける論理式の個数に制限はない。 例:(i)
  • (2)それ以外の前提棒の上には一つしか論理式をかけない。 例:(ii)

(i)

P → q Prem
¬Q∧R   Prem
S→¬P  Prem
------

(ii)

P → q Prem
¬Q∧R   Prem
S→¬P  Prem
-----------
    P  Prem
    -------

繰り返し規則(rule of repetition: Rep)

  • その導出の前提棒の上にある式を繰り返し書いて良い。
    P    Prem
    ---------
    P    Rep
P → P    → intro

復活規則(rule of reiteration:Reit)

  • 依存している導出(有効なスコープである前提)を繰り返し書いても良い。

例

(P → Q) ∧ ¬Q    Prem
---------------------
P → Q    ∧ elim
¬Q        ∧ elim
    P         Prem
    ---------
    P → Q    Reit
    Q         → elim
    ¬Q        Reit

→除去規則(→ elimination: → elim)

  • A → B と A が同じ導出に出てきたら、Bをその導出中に書き加えて良い
P →Q    Prem
P        Prem
---------
P →Q    Rep
P        Rep
Q        → elim

→導入規則(→ introduction: → intro)

  • 前提AからBへの導出を含んでいるならば、A→Bをその導出後の項目に書き加えて良い。
P→Q    prem
Q→R    prem
    P         prem
    ----
    P → Q    reit
    Q         → elim
    Q→R      reit
    R         →elim
P → R    → intro

∧除去規則(∧ elimination: ∧ elim)

  • A ∧ Bが導出の一項目として現れているなら、A,Bいずれもその同じ導入の項目として書き足して良い。
A ∧ B    Prem
A        ∧ elim

あるいは

A ∧ B    Prem
B        ∧ elim

∧導入規則(∧ introduction:∧ intro)

  • AとBがいずれも同じ導出の項目として現れているなら、A∧Bをその導出の一項目として書き足して良い。　
A
B
A ∧ B    ∧ intro

↔︎除去規則(↔︎ elimination:↔︎ elim)

  • A ↔ ︎BとA(あるいはB)が導出に一項目として現れていたら、その導出にもう片方のB(あるいはA)を書き加えて良い。
A ↔︎ B
A
B        ↔︎ elim

↔︎導入規則(↔︎ introduction:↔︎ intro)

  • A → BとB → Aが一つの導出に一項目として現れてきていたら、その導出にA ↔ ︎︎︎Bを書き加えて良い。
A → B
B → A
A ↔︎ B    ↔︎ intro

¬削除規則(¬ elimination: ¬ elim)

  • ¬¬Aの導出に¬Aを書き加えて良い
¬¬A

A    ¬ elim

¬導入規則(¬ introduction:¬ intro)

  • Aを仮定とした導出から矛盾(contradiction)が発生した場合、導出の次の項目に¬Aを加えて良い
    A    prem
    ---------
    ...
    B
    ...
    ¬B    contradiction !
¬A    ¬ intro

∨除去規則(∨ elimination:∨ elim)

  • A ∨ B,A→C,B→Cが導出に出てきた場合、Cを書き加えて良い
A ∨ B
A→C
B→C
C      ∨ elim

∨導入規則(∨ introduction:∨ intro)

  • AかBが同じ導出において以前に一項目として出てきているなら、A ∨ Bを書き加えて良い
A
A ∨ B    ∨ intro
B
A ∨ B    ∨ intro

矛盾記号(⊥)の導入

  • contradiction!を論理定項として使うとほかの∨ elimや→ introなどのオペランドとして使えるのでより演繹の自由度が上がる。
  • 矛盾記号⊥を導入する。

¬elim*

  • 矛盾する式集合(A,¬A)が導出に現れた場合、⊥をその導出に書き加えて良い
A
¬A

⊥
  • ※矛盾記号の¬elim*を導入する場合、これまでの¬elimの規則はDNという名前に変更する

¬intro*

    A
    --
    ⊥
¬A

自然演繹の攻略法

【攻略法:→を目指すには】

  • A → Bに達したい時,Aを前提とし、一番下にBが出てくるような導出を構成し、→ introによってA → Bを得るようにする

【攻略法:∧を目指すには】

  • A ∧ Bに至りたかったら、AとBをそれぞれ別個に得るようにし、そのあとに∧ introを用いると良い。

【攻略法:間接証明】

  • ¬Aを仮定して矛盾を起こして¬¬Aを導出し、¬elimでAを得ることができる。
    • 個人的に背理法のような戦略だと思う

NPクラスのNondeterministic polynominal algorithmについて

complexity computer science

4部作その3。組合せ最適化のページ(p422~423)の理解メモです。100回くらい同じページを読んだ結果、本書の記述だけだと不十分に感じたの類書を参考にしています｡

組合せ最適化 第2版 (理論とアルゴリズム)

組合せ最適化 第2版 (理論とアルゴリズム)

余談:NP(Nondeterministic polynominal)という特性

※重要だと思って精読しましたが、乱択アルゴリズムを考えないときはあまり重要ではないので個人の判断で読み飛ばしてください。本書でもnon-deterministic polynominalを何かの前提・準備として紹介していません。

NPで扱える決定問題の種類はdeterministicに限らない。NPのNondeterministicという名前は決定問題のアルゴリズムとして採用できるアルゴリズムの制約からきている。

以下は同値である。

  • 決定問題に多項式時間非決定性アルゴリズム(nondeterministic polynominal algorithm)がある
  • 決定問題がNPに属する

命題15.14 決定問題は、多項式時間非決定性アルゴリズムを持つとき、そしてそのときのみ、NPに属する

非決定性アルゴリズムはランダム化アルゴリズム(randomized algorithm)の一種。

ランダム化アルゴリズムはf(s)→Tに対して以下のものと定義されています。

  • 関数g:{s#r:s∈S,r∈{0,1}k(s)}→T
    • S:元の問題のインスタンスの集合
    • r:ランダムビット
    • 関数k:引数に対して整数を返す関数(k:S⇨Z+)。引数sに対して多項式サイズであることを表しています。

ランダム化アルゴリズムはある問題f(s)インスタンスのサイズに依存する多項式時間個のランダムビットrを使って元のアルゴリズムと近い決定ができるアルゴリズムです。元のアルゴリズムとどの程度精度が一致しているかで以下のように分類されています。

algorithm definition (※全てp422からの抜粋)
モンテカルロアルゴリズム インスタンスによらず少なくとも正の確率pで正しい答えを出力する
片側誤差のあるランダム化アルゴリズム f(s)=0となるどのs∈Sに対しても、全てのr∈{0,1}k(s)でg(s#r)=0となる
非決定性アルゴリズム f(s)=1となる各s∈Sに対してg(s#r)=1を満たすr∈{0,1}k(s)が少なくとも1個存在する
ラスベガスアルゴリズム すべてのs∈Sに対してg(s#r)=f(s)である理想的な場合

下図のような閉包関係があります。

f:id:yuyubu:20190613181315p:plain

ここまで読んでまともな人ならお気付きかと思いますが、非決定性アルゴリズムの

f(s)=1となる各s∈Sに対してg(s#r)=1を満たすr∈{0,1}k(s)が少なくとも1個存在する

という特性はモンテカルロアルゴリズムの

インスタンスによらず少なくとも正の確率pで正しい答えを出力する

という特性がすでに満たしているように読めるはずです。すなわち本書の記述のみを頼りに考えると「片側誤差のあるランダム化アルゴリズム」と「非決定性アルゴリズム」の集合のサイズは完全一致になるはずです。

本棚があったので類書を少し調査してみました。

乱択アルゴリズム (アルゴリズム・サイエンス・シリーズ―数理技法編)

乱択アルゴリズム (アルゴリズム・サイエンス・シリーズ―数理技法編)

すると、この本のp12を読むと片側誤差のあるランダム化アルゴリズムについて興味深いことがわかりました。

乱数の出方に寄らず常に正しい結果を与える乱択アルゴリズムをラスベガスアルゴリズム(Las Vegas algorithm)と呼ぶ。これに対して、乱数の出方によって誤った結果を与えることが実際にあるアルゴリズムをモンテカルロアルゴリズム(Monte Carlo algorithm)と呼ぶ。(中略) 対象とする問題が、判定問題(decision problem),つまりYESかNOと答えるタイプの問題である場合、モンテカルロアルゴリズムはさらに、片側謝りアルゴリズム(one-sideed error algorithm)と両側謝りアルゴリズム(both-sided error algorithm)の二つに分類される。真の答えがYESの時だけ、あるいはNOの時だけ誤る可能性があり、反対の場合には必ず正しく答えるアルゴリズムは片側誤りアルゴリズムである。どちらの場合にも誤る可能性のあるアルゴリズムは両側誤りアルゴリズムである。

黄色い本と白い本のone-sided error algorithm(片側謝りアルゴリズム、片側誤差のあるランダム化アルゴリズム )について定義を比較してみましょう

本 定義　
黄色い本 f(s)=0となるどのs∈Sに対しても、全てのr∈{01}k(s)でg(s#r)=0となる
白い本 YESあるいはNOの時だけ誤る可能性があり、反対の場合には必ず正しく答える

白い本のone-sided error algorithmの定義がより厳密と仮定すると、片側誤差ありアルゴリズムはYESインスタンスまたはNOインスタンスのどちらかは正しく決定することができるアルゴリズムということになります。黄色い本は"YES sideに誤差がありNo sideは完璧に答えるアルゴリズム"を暗黙の前提にしています。

上記を踏まえて乱択アルゴリズムの表は次のように再構成できます。

algorithm definition (※全てp422からの抜粋)
モンテカルロアルゴリズム インスタンスによらず少なくとも正の確率pで正しい答えを出力する
片側誤差のあるランダム化アルゴリズム YESインスタンスもしくはNoインスタンスのどちらかを完全に正しく決定できる
非決定性アルゴリズム NOインスタンスを正しく決定できる
ラスベガスアルゴリズム すべてのs∈Sに対してg(s#r)=f(s)である理想的な場合

f:id:yuyubu:20190923043342p:plain
再整理した乱択アルゴリズムの分類

上記の分類は黄色、白い本の内容と矛盾なく乱択アルゴリズムをうまく分類できているように思えますが、専門家ではないのですこし自信がありません。*1 　

非決定性アルゴリズムが存在する↔︎クラスNP なのはなぜか　

証明をそのまま載せてしまうのはアレなので概略だけさっと書きます。ランダムビットrをcertificateと読み替えて、ランダム化アルゴリズムをそのまま証明検証アルゴリズムに置き換えることが出来ます。

非決定性アルゴリズムの定義

f(s)=1となる各s∈Sに対してg(s#r)=1を満たすr∈{0,1}k(s)が少なくとも1個存在する

から、NP問題の定義

任意のyes-インスタンスに対してのみ多項式時間で検証できる証明の存在だけが要求される。

補足:検証アルゴリズムの定義 Y = {y∈X:y#c∈Y'であるようなc∈{0,1}[p(size(y))]が存在する}

を導くことが出来ます。

補足情報

具体例としては以下の資料で2-SATをランダム化アルゴリズムを使って解く方法が挙げられています。

http://www-imai.is.s.u-tokyo.ac.jp/seminar/reading/resume/02summer_11.pdf

若干この本ではnondeterministicの話はわかりにくかったので、アルゴリズムイントロダクションという本を参照したところ、NP問題の特にnondeterministic側の問題に焦点を当てた本として以下のものが提示されていた。

アルゴリズムイントロダクション 第3版 総合版：世界標準MIT教科書

アルゴリズムイントロダクション 第3版 総合版：世界標準MIT教科書

Hopcroft and Ullman [180] give a good presentation of NP-completeness in terms of nondeterministic models of computation.

  • [180] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

Introduction to Automata Theory, Languages, and Computation: Pearson New International Edition (English Edition)

Introduction to Automata Theory, Languages, and Computation: Pearson New International Edition (English Edition)

和訳もあるようです

オートマトン言語理論 計算論〈1〉 (Information & Computing)

オートマトン言語理論 計算論〈1〉 (Information & Computing)

オートマトン言語理論 計算論2 <第2版>

オートマトン言語理論 計算論2 <第2版>

note:本エントリでは深入りしませんが、非決定性アルゴリズムより広い乱択アルゴリズムを考えたときの計算クラスもあるようです。

*1:余談ですがyes-sideが完璧になってる片側誤差ありアルゴリズムはco-NPで出てきそうだなと書いてて思いました。

PとNPについて

complexity computer science

4部作その2。組み合わせ最適化第二版のp419~421の理解メモです。前回の決定問題の知識を前提に記事を書いています。　

yuyubu.hatenablog.com

組合せ最適化 第2版 (理論とアルゴリズム)

組合せ最適化 第2版 (理論とアルゴリズム)

Nondeterministicについてちょっと小話

ちょっとわかりにくいのがNPですね。Not Pではありません。この話題に入る前にNondeterministic Turing Machineはドラえもんの秘密道具並みにヤバイ存在だということを頭に入れておくと、理解が深まります。NP問題を多項式時間で解くとされる「非決定性チューリング機械」は思考実験的アナロジーであり、任意のNP問題の非決定性アルゴリズムを多項式時間で解く計算機は実存していません。

またNondeterministicという単語が一般的なシステム用語と少しスコープが違う使われ方をしているように感じます。*1

  • イメージとしてはこんな感じです。
    • △常に同じ答えを出さない
    • ⭕️常に最良の乱数を選ぶことができる

NPとP

  • NP:決定問題のうち、証明検証アルゴリズムがPで終わる証明(certificate)が存在しているもの。*2

クラスNPでは、多項式時間アルゴリズムは要求されず、任意のyes-インスタンスに対してのみ多項式時間で検証できる証明の存在だけが要求される。(p421)

多項式時間アルゴリズムが存在する全ての決定問題のクラスをPで表す。(p420)

証明検証アルゴリズムの箇所にも書いたが、Pの決定アルゴリズムはそのまま判定アルゴリズムとして利用することができるのでPはNPに含まれる。

決定アルゴリズムの時点で速度が十分ある(任意の問題を多項式時間で決定できる)場合は決定アルゴリズムをそのまま証明検証アルゴリズムに流用することができる。決定アルゴリズムを使った検証では#cが不要になる。(前回エントリより)

よってNP ⊇ Pという包含関係が成り立つ。ただしこの包含関係が真部分集合であるかどうかは30年以上前からの重大な未解決問題(P ≠ NP予想)になっている。

Pが見つかっていないNPとNP完全

NPである問題に多項式時間アルゴリズムが見つかれば、その問題はPに分類することができる。

NP完全といわれるNP中の特殊なクラスの場合は少し話が違っていてPで解けるアルゴリズムが見つかった場合は全てのNP問題がPで解けるという、ある種革命的な状況が発生してしまう(P=NP)。

これ以外のNP問題、つまり現状でNP完全なのかPなのか分かっていない問題はNP-intermediateと言われている

en.wikipedia.org

ただしP=NPが判明すればNPIは空集合になる。P ≠ NPの場合はNPIが存在する。PapadimitriouのComputational Complexityにこのクラスの存在証明が乘っているらしい。

ぼくには簡単ではありませんが (^^;) Papadimitriou の Computational Complexity に証明が載っていました。対角線論法を使ってうまいこといったはず。

srad.jp

Computational Complexity

Computational Complexity

  • 作者: Christos H. Papadimitriou
  • 出版社/メーカー: Addison Wesley
  • 発売日: 1993/11/30
  • メディア: ペーパーバック
  • 購入: 1人 クリック: 1回
  • この商品を含むブログを見る

実際に本を確認してみたところ、以下の記述がそれらしい

Theorem 14.1: IF P ≠ NP, then there is a language in NP which is neither in P nor is it NP-complete(p330)

Theoremのあとに証明が続くが割愛

Papadimitriouの本以外にも以下の本にもNPIの章と証明はあった

Computational Complexity: A Modern Approach

Computational Complexity: A Modern Approach

どの本に乗っている証明も以下の論文の引用になっていた

  • Ladner, Richard (1975). "On the Structure of Polynomial Time Reducibility".

素因数分解やグラフ同型問題が今の所、このクラスだろうと考えられている

ちなみに多くの専門家はP=NPではないと予想している。(2012年時点で126/152人)

http://dopal.cs.uec.ac.jp/okamotoy/PDF/2013/complexity10confusions.pdf

*1:Nondeterministicの一般定義というのはないと思うので、あくまで業務システムに触れることが多い一個人の感想です。

*2:NPの定義が「多項式時間で検証できる」という分かりやすい書き方になっていない理由は後続エントリのnon-deterministicを扱う際に重要になる

ubuntu18.04で英字キーボード(101)キーボードを使う備忘録(主に日本語/英語切り替え)

ubuntu

日本語版ubuntuの英字キーボードのデフォルト設定に不満があったためカスタマイズしたかったが設定がわからりずらすぎて消耗したのでメモ

1.pkg-reconfigureでキーボードレイアウト設定

sudo dpkg-reconfigure keyboard-configurationで該当するキーボードを選択。

102を勧めているqiitaがあったけど、

qiita.com

Shiftとzキーの間になにかキーがあればそれは102キーボードだけど、多分そのキーがない101キーボードのほうが日本では一般的なのでそちらを選択する可能性のほうが高い。(手元のキーボードの配列を調べてあってるものを選んでください。)

2.言語設定からmozc(日本語)以外をすべて削除

設定>Region & Language のinput SourcesからEnglishを削除して「日本語(Mozc)」のみの状態にする

f:id:yuyubu:20190704172454p:plain
mozcいがい全部消す

3.mozcのツール>プロパティ>キー設定で「入力キー」hankaku/zenkakuのを切り替えに使いたいキーに入れ替える

キー設定の選択[MS-IME]は多分プリセットなので適当に自分が慣れているものを選びましょう。設定後は「カスタム」に変わるはずです。

f:id:yuyubu:20190704172939p:plain
プリセットは自分が好みのものを選ぼう

f:id:yuyubu:20190704172907p:plain
中段の４つを全部ctrol + spaceとかに入れ替える

f:id:yuyubu:20190704172535p:plain
mozcの設定の入り口は画面右上の方にある

上記手順完了のち、ログインし直して設定は完了。設定したキーで日本語英語切り替えできるようになっているはず。

Amazonで新品の本を注文したら表紙が一部破損しているものが届いた

日記 Amazon

ちょうどブログのネタになるかなと思ったので半年ほど前にあったことを書き残しておきます。

経緯

買った本はWeikum本ことトランザクションの本です。

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems) (English Edition)

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems) (English Edition)

kindle版を持っていたが、この本は「ここで以前説明したtheorem 5.4によると...」という感じでページを行ったり来たりするので紙の本もあると良いなと思って購入した。

ちなみにこの本のKindle版は固定PDFのような形になっておりフォントサイズが変えられないため、iPadだと読めるがパソコンだと文字が小さくてかなり読みづらい。

ですので一応紙の本も買ってみる事にした。

ちなみに現在電子版を買うならDRM FREEのPDFが変えるのでそっちがおすすめ*1

で、本が届くと表紙にヒビが入っていた。

f:id:yuyubu:20190130132748j:plain
表紙にヒビがはいってる

対処

この本はその重すぎる自重故に、持ち運んでいるとそのうちバラバラになってくるらしいが、そもそも最初から破れてるのはおかしいんじゃない？とのアドバイスをもらったので、一応クレームを出してみる事にした。

表紙がひび割れた状態で到着しました。新品のものを買った認識ですが、この件に関するサポートは受けられますか？

破損している商品の写真を求められたのでそちらをメールで送付した。輸送中の破損は仕方ないと思うので、売り手、買手で五分五分で手を打つのが筋なんじゃないないかと個人的に考えています。50%返金とかになるかな？

交渉

とりあえず、20%の返金で良いか？という提案がきた。なぜ20%？何を基準に？少し調べてみると、Amazonにはマーケットプレイス保証というものがある。

Amazon.co.jpのウェブサイトで出品者から商品を購入するお客様は、配送料を含めた購入総額のうち、最高300,000円まで保証されます。

www.amazon.co.jp

「返品ポリシー」に合致して返品を却下された場合、Amazonが30万円まで保証してくれるらしい。

調べる過程で見つけましたが、amazonのseller向けフォーラムというものの存在を知り、軽く巡回してみたが以下のことがわかった

https://sellercentral-japan.amazon.com/forums/

  • 返品に関しては購入者が有利になっている。

一応新品を買って破損していたので、返品に応じなければマーケットプレイス保証が使えるはず。 と言っても、返品は流石に可愛そうなので50%返金 or 交換の選択肢で交渉に挑んでみた。

20%は安すぎませんか。

ここは新品と交換が筋だと思いますが、時間がどれぐらいかかりますか？(また在庫的に可能でしょうか？)

交換が難しい場合は、50%返金でどうでしょうか。

結果

  • 再送(返品不要)

という事になった。50%返金 or 交換の選択肢でなぜ再送という判断になるんだろうか。 向こうの負担的には50%返金が一番ダメージ少ない気がするけど。 tx本の在庫処分に困っていたのだろうか。

なぜか我が家にはweikum本が3冊(normal + 破損 + kindle)あるという自体に... とりあえず会社と自宅に置いておく事にした

*1:多分ここ:https://www.elsevier.com/books/transactional-information-systems/weikum/978-1-55860-508-4

Transactionのinterpretation(herbrand semantics)について

transaction database

herbrand semanticsのメモです。主にFSRを理解するための準備です。このエントリはChristos Papadimitrioupapa:Theory of Database Concurrency Control(通称papa本)の5~9ページのまとめです。

データベースの世界にはherbrand semanticsというConflictやSerializabilityを考える時に使う便利な道具があります。いつからherbrand semanticsと呼ばれるようになったのかはわかりませんが、papa本ではinterpretationという名前で扱われています。 近年ではトランザクションの教科書にもherbrand semanticsと書かれていることもありますので、本エントリではpapa本からの引用以外はこちらの名前を使います。

weikum本寄りの解説はぱとさんがあげているので、今回はpapa本寄りのメモを書きたいと思います。

taityo-diary.hatenablog.jp

Theory of Database Concurrency Control

Theory of Database Concurrency Control

transactionとreadとwrite

まずはトランザクションの定義から。トランザクションは任意のentityに対するreadとwriteの有限集合。

Difinition 1.1 A transaction A is a finite sequence fo steps A = a_1,a_2...a_n. The steps are assumed to be distinct symbols, and two differencttransactions cannot have steps in common. With each step a_j of A we associate an action ACTION(a_j) ∈ {W,R}, and an entity ENTITY(a_j) ∈ E.

read:対象entityの現在の値をプログラム中の変数へ割当てることを意味する。

If some step a_j reads entity x. This means that a particular program variable t_j in the underlying program is assigned the current value of x in the database: t_j := x.

write:対象entityに対するプログラムで計算した値の割り当てを意味する。

If ACTION(a_j) = W and ENTITY(a_j) = x , then the step write x. By this we mean that x is assigned a value computed by the program, which is potentially a function of all previously read(by the same program) values of entities: x := fj(t_i1,ti_2,...t_ik),where the ip's are all indices smaller than j for which ACTION(a_ip) = R

なおこのwriteで書く値の計算はwrite step以前のすべてのreadを引数にとる関数fとして定義することができる。この関数の厳密な定義がherbrand semanticsになる。

interpretation

条件分岐や繰り返しなどの制御構文を含むアプリ(プログラム)から発行されたdatabaseに対するread/writeのdatabase stepの意味をdatabase側から解釈する。プログラムが発行したdatabase stepのまとまりはtransactionになる。transactionは制御構文を持たないので、アプリとは別の解釈が必要となる。

A transaction, as defined above, is a purely syntactic object, subject to different interpretations. Intuitively, specifying an interpretation of a transaction means fixing a particular application program from which the transaction has originated, disregarding of course any control structure the program may have.

トランザクションの実行はある状態からある状態への写像と解釈する。

An interpretation of A(注:このAは任意のtransactionを指している) is a pair I = (D,F), where D = {D_x,D_y,...} is a set of domains, onefor each entity in E; each domain is a set of values for the corresponding entity. F = {f_a:a is a step of A and Action(a)=W} is a set of functions, one for each write step of A. For each such step a, f_a is a mapping

f_a: \prod_{x \in B(a)} D_x \to D_{ENTITY(a)}

  • writeのオペレーションはそれまでに読んだ値のドメインの直積からwrite対象のentityのドメインへの写像になる。
  • B(a)はa以前に読んだ全てのentityの集合。

B(a_j) = {x \in E : {\bf For \, some }\, i \le j \, ACTION(a_i) = {\bf R \, and \, }ENTITY(a_i) = x}

具体例として1トランザクション前提(1並列)で以下の送金プログラムで説明されている。

program transfer(amt:integer);
    entities x,y: integer;
    variables temp1,temp2:integer;
    begin
    temp1 := x;
    if temp1 ≧ amt then
        begin
        x := tmp1 -amt; 
        temp2 := y;
        y := temp2 + amt
        end
    end.

ローカル変数へのentity代入をread,entityへの値の書き込みをwriteのデータベースステップと考えると上記のプログラムは以下のschedule(Action)を作る。

A = R(x)W(x)R(y)W(y)

この時、各database stepのherbrand semanticsは以下のようになる。

t1:=x
x:=f2(t1)
t3:=y
y:=f4(t1,t3)

f4の関数の内容はf4(t1,t3)=t3+50で、t1は一切使わないが、このt1はherbrand semanticsでは必要とする。 どのパラメータが実際に使われているかという情報はアプリ(DBMSを読み書きするプログラム)の完全な情報がないと分からない。そしてconncurency controlを考える時にアプリのコード全体が把握できるケースは極めて稀*1であるため、writeの前に発行されたreadは全てwriteを表す関数の引数として扱う。

Situations such as this of Example 1.2, in which we have complete information about the program and the value of their parameters, are rare in concurrency control

同じentityへの各database stepは1回まで

オペレーションごとにherbrand semanticsを考えることができそうだが、correctなスケジュールなら1つのentityへの複数回のread,writeは冗長なので、herbrand semanticsを考えるときは同じトランザクション内では

  • read/writeは1つのentityに対して1回まで
  • writeしたentityの値をreadしない

という前提を置く

It is quite natural-and, it turns out, simplifying-to make the following assumptions about the structure of the transactions.

(a)In a transaction an entity is read at most once, and is written at most once.

(b)In a transaction, no entity is read after it is written.

後述しますが、本来ならあるトランザクションの何番目のステップのfというような表記になるところを上記の前提を置くことで 、あるトランザクションのあるentityに対する操作(f)、またはあるトランザクションの何番目の操作(f)というシンタックスで表現できる。ちなみに、weikum本では前者のシンタックスを採用し、papa本では後者を採用している。*2

Hs(wi(x)) := fix(Hs(ri(y1)),...,Hs(ri(ym))), where the ri(yj), 1 ≤ j ≤ m, represent all read operations of ti that occur in s before wi(x)

weikum本より引用。f_{ix}のiをトランザクションの添え字、xをentityとするシンタックスにしている

Interpretationとshcedule

If s is a schedule involving the transactions A_1,...,A_k, then an interpretation I of s is a k-tuple of interpretations I_j = (D,F_j), all with the same choice D of domains for the entities.

scheduleにinterpretationを適応すると、schedule中の任意のdatabase stepをa_s(I,X)で表現することができる。

Suppose that s is a schedule, I an interpretation, and X an initial state, that is a value for each entity. We say that every database step a of s computes a value a_s(I,X).

また、スケジュールの実行結果、つまり最終状態をs(I,X)という特別なシンタックスで表現する

The final state resulting from the execution of s, denoted s(I,X)

まとめ

  • 各entityがとりうる値(domain)の集合をDとしている
  • writeの関数fのすべての集合をFとしている。
  • 上記二つのペアをinterpretation(herbrand semantics)としている。
    • interpretationと初期値Xを使うことでtransaction中の任意のstepを関数で表現できる

*1:ストアドは例外

*2:上記のプログラムのread/writeへのherbrand semanticsの適当を見ると、最初のwriteは2回目のオペレーションなのでf2となっている