Hello worldの次は何やったらいいという人は、自分は本当になにをしたいのか問うほうがいい
https://blog.goo.ne.jp/xmldtp/e/761fd2136761fed4867a9e5de22ee1a4
で「２．２プログラムを学びたい場合、計算論とかの話になる。これは別エントリで」と書いた。
それについて
つまり、プログラムを書くとは？というのを突き詰めていくと、どうなるのか？
→サブテーマとして、プログラムは作成可能なのか？その根拠は論理的に説明できるのか？
→説明できないとしたら、どこかに論理のジャンプが起こることになり、
論理的にプログラムは書けない＝プログラムで論理性を養うというのはおかしい
ことになる。
あんまり詳しくないので、
ロリポおじさん程度の不正確さで書くので、まあ、大目に見てやってください
（書いてあること、信じないでね！）
【プログラム→計算可能まで】
プログラムを書くとはどういうことかを調べるのは、まずはいくつかのプログラミング言語で書いてみたり、調べたりすることになる。
そうすると、プログラムは大きく２種類の箇所に分かれていることが分かる
・意味的には各言語共通で表記方法が違う
：足し算、引き算などの四則演算など
・各言語ごとに特徴があり、目的に応じて使う
：Java等のクラス、Cのメモリアクセス（＝ポインタ）
ここで、目的の話はしないことなので、上のほうをつきつめる。
表記法はさておき、意味的に考えて、コンピューターはなんでも計算できるのか？
これは、計算可能性という話で、計算論という学問分野になる。
大きく２つの方法で議論できる
・１つは、チューリングマシン
・もう一つは、ラムダ計算。この分野には教科書的な本が昔あり（高橋正子「計算論 計算可能性とラムダ計算」）そこに出てくるけど、一般的に計算を定義して、どのようなものが計算可能か定義する（これは資源を考えない。資源を考えると計算複雑性という話になる）
この２つは、チャーチ・チューリングのテーゼによって、同じこと言っているということになる。
【ラムダ計算→型つきラムダ計算】
ところが、ラムダ計算で「正しさ」を議論していくと、不完全性定理のコンピューター版みたいな話（一階述語論理の決定可能性問題）になる。つまり、「正しいかどうかは停止しない限り判断できない」
そこで「正しい」ということが証明できないとこまるので、「強く正規化する」（つまり停止する）ものが求められた。そこでカリー・ハワード対応、型つきラムダ計算が出てきて（ただし、型つきラムダ計算の中には、強く正規化しないものもあるようだ）。この型つきラムダ計算は、Javaで出てくる多態性（ポリモーフィズム）なんかを議論したり、圏論へと広がっていく。また、型の話は、型と命題の関係にいく。ここから先の話は後述の「では、仕様をどう表現するか：意味論」へつづく。
一方、「正しい」ことを証明する話は、「形式仕様」という議論の場に移っていく。この形式仕様では、仕様を論理的に記述して正しいことを示す「形式仕様言語」(Z,B,Event Bなど）と、正しいかどうかは証明できないけど、正しくない場合には検出する「モデル検査」(SPINなど）が出てきた。形式仕様言語の場合、正しいことを証明するには停止しないといけないが、そもそも、組み込みのプログラムは停止しないから、証明できなくなってしまう（なので、組み込みは、モデル検査やシミュレーションをよく使う）。証明は大変なので、自動定理証明が出てきたり、証明支援が出てきたり（coqなど）・・・っていう広がりを見ている。
【要求仕様をプログラムに実装できるか】
今までの話は、どんなもの（WHAT)が計算可能かという話だった。これとは別に、どうやって（HOW)要求仕様から設計プログラミングに落とし込めるかという話が「別に」ある。実務上では、要求仕様→設計→プログラミングといくが、ここに一貫性があるのか、完全性を保ちながら要求仕様からプログラミングまでの変換は可能であるかという話だ。「ない」となったら、「トレーサビリティマトリックス」とか作っている私たちの立場は？ってことになる。
実際、「一貫性はない」という意見があった。
要求仕様は「WHAT」を定義していて、設計は「HOW」を定義している。WHATはHOWに”とらわれてはいけない”（要求分析者は設計方法に左右されずに要求を出さないといけない）。だからこの間には断層がある。これが佐藤正美氏の提唱する「SDLCの断層」だった。この論理はウォーターフォールではまあいいんだけど、アジャイルになると、設計と要求定義は混在化してくる。そうすると、あちらこちらに断層ができて、一貫化したプログラムは作れない！という話になる。
一貫性がないなら、一つの視点で表現することができない。結果として、ふるまいの部分はアクティビティ図、構造はクラス図など、様々な図を使って仕様を表すUMLが広まった。が、これらの図は、何がどうつながっているのかが分かりにくい・一貫性が見えない・完全性は大丈夫なのかわからない事態を生みだした。
しかし、Lamsweerdeがゴールという概念を用いてKAOSという手法を提唱することにより、この断層はなくなった。そして、UMLの各図はKAOSから導きだせることが、1冊の本(Requirements Engineering: From System Goals to UML Models to Software Specifications)で示された。
KAOSの考え方は、様相論理を用いる。システム化に成功するということは、「現状Pから、システム化に成功した状態（要求を満たした状態）Qへ、いつかは状態遷移すること」である（P→□Q）と考える。そしてこのP→□Qをゴール（一番初めに定義するゴールをトップゴール）とよぶ。そうすると、ゴールの状態Qを表現すること（WHAT）が要求定義であり、設計とは現状Pから状態Qに状態遷移させる方法を考えること（P→□Qの→に相当）である。となる。つまり、２つの行為は１つのゴールで表現できる。
そしてこのゴールP→□Qを「何らかの手法で」分割し（詳細化・洗練という）、さらにそのゴールを分割して・・・と分割していったとき、すべてのゴールは、ある人によって実現可能なプロセスを実行することによって達成されるならば、全プロセスが実行されたときにゴールは達成すると考える。
（なお、ここでは達成ゴールを紹介した。ゴールにはほかに、回避ゴール、維持ゴールなどあるけど、詳細な説明は省略。似た話だから）
これにより、どうやって（HOW)要求仕様から設計プログラミングに落とし込めるかという話は、システムのトップゴールP→□Qから、どうやって詳細化を行って、実行可能な末端ゴールに一貫性（完全性）を保ちながら分解できるかという話に帰着した。この完全性を保ちながら分解する方法は、What部分を分解する要素分解と、状態遷移を分解するマイルストーン分解を行えば可能でありそうということを直感的に言っている人もいるが、数学的にはまだ証明されていない。ここが最前線。
なお、(Requirements Engineering: From System Goals to UML Models to Software Specifications)の表紙には、バベルの塔が書かれている。システムをUMLの様々な図というか言語（UMLのLは言語のL)で表した混乱を、この本で終止符を打つということでしょうか？日本はともかく、世界的にこの本は要求仕様の教科書となっている。
【では、仕様をどう表現するか：意味論】
ただ、ここではP→□Qの状態PやQの表現方法については議論していない。なので、次は「状態はどのように表現できるか。単なる記号ではなく、意味を持った形で表現できるのか？」ということが議論の対象になる。
現状は、この状態（要求仕様）を自然言語で書いているが、それだとあいまいになる。そこで、論理式で書くことになる（そもそも、様相論理なので、論理式だよね）。記号を論理式で書く・・・この方向は、記号論理学の話から、ミニマリストプログラム、CCG(Combibatory Categorial Grammars)、DisCoCatへとつながっていく。ここら辺が最新なの？
また命題と型とが結びついて、すべての命題がある型であるというホモトピー タイプ セオリー（HoTT）が出てくる。型つきラムダ計算から来た流れは、この辺が最先端？
でも、これらも１つの表現方法だけど、実際のプログラムでは、項目と値によるエンティティモデルやクラス・オブジェクトで表現したりする。
さらには、AIの世界だと、特徴ベクトルという形で状態を表現し、その特徴ベクトルの演算を考えるようになってきた（Word2Vec)この辺が、先端かしら・・・
ということで、意味論の分野は、論理（命題）、型、特徴ベクトル、項目と値を、どんな感じで「まぜまぜ」するのかが話題。 ＜ いまここ。
【ちゃぶ台返しの量子コンピュータ】
ここで、ちゃぶ台返しが起こる。量子コンピューターは、これらの流れと全く違った計算方法をする。いわく、ブラとケットがでてきてブラケット・・・わけわからん。
そのうえ、もっとわけわからんことが起こってる。いわく
・答えは、「これ」と求まらない。確率的に求まる（は、はい？？）
・アルゴリズムがないと、計算できない
そのアルゴリズムで、素因数分解するものは、ある。ショアのが。
で、これでパスワードが無効になるとか言われて話題になっている（サイエンスZEROでも再放送してた）。
もう一つ、行列式は解ける。このアルゴリズムがある。
で、さっきの意味論に戻ってくる。特徴ベクトルは行列で表してるけど、それなら、量子コンピューターでも扱える？
この辺っていうか、量子コンピューター全体が先端
【量子コンピューターとAI：不確かさ】
量子コンピューターは確率的に答えが求まるけど、AIの機械学習も確率的に求める。
いままでのバチンと答えが求まるものと違う。
このような確率的、不確かななかで、どう計算するのかというのが先端の話題。
不確かさの中でのAIのテストとか、不確かさの中での形式仕様PATとか
不確かさについて扱うのが、今先端。
今後は、確率論的ということで、ベイズが入ってくるか？入ってくるならどんな感じで？
なんかが、近未来的な話なのでしょうか・・・
【で・・・】
こんな話、おもしろいですか？
おもしろいなら、プログラムを学ぶことを目的にすることもアリだと思うけど、
（将来、量子コンピューターの方向に進むなら、いままでの勉強は無駄になっちゃうけど・・・）
たぶん、こういうことをやりたい人はごくわずかで、プログラムを「作る」のが楽しいんではなくて？
https://blog.goo.ne.jp/xmldtp/e/761fd2136761fed4867a9e5de22ee1a4
で「２．２プログラムを学びたい場合、計算論とかの話になる。これは別エントリで」と書いた。
それについて
つまり、プログラムを書くとは？というのを突き詰めていくと、どうなるのか？
→サブテーマとして、プログラムは作成可能なのか？その根拠は論理的に説明できるのか？
→説明できないとしたら、どこかに論理のジャンプが起こることになり、
論理的にプログラムは書けない＝プログラムで論理性を養うというのはおかしい
ことになる。
あんまり詳しくないので、
ロリポおじさん程度の不正確さで書くので、まあ、大目に見てやってください
（書いてあること、信じないでね！）
【プログラム→計算可能まで】
プログラムを書くとはどういうことかを調べるのは、まずはいくつかのプログラミング言語で書いてみたり、調べたりすることになる。
そうすると、プログラムは大きく２種類の箇所に分かれていることが分かる
・意味的には各言語共通で表記方法が違う
：足し算、引き算などの四則演算など
・各言語ごとに特徴があり、目的に応じて使う
：Java等のクラス、Cのメモリアクセス（＝ポインタ）
ここで、目的の話はしないことなので、上のほうをつきつめる。
表記法はさておき、意味的に考えて、コンピューターはなんでも計算できるのか？
これは、計算可能性という話で、計算論という学問分野になる。
大きく２つの方法で議論できる
・１つは、チューリングマシン
・もう一つは、ラムダ計算。この分野には教科書的な本が昔あり（高橋正子「計算論 計算可能性とラムダ計算」）そこに出てくるけど、一般的に計算を定義して、どのようなものが計算可能か定義する（これは資源を考えない。資源を考えると計算複雑性という話になる）
この２つは、チャーチ・チューリングのテーゼによって、同じこと言っているということになる。
【ラムダ計算→型つきラムダ計算】
ところが、ラムダ計算で「正しさ」を議論していくと、不完全性定理のコンピューター版みたいな話（一階述語論理の決定可能性問題）になる。つまり、「正しいかどうかは停止しない限り判断できない」
そこで「正しい」ということが証明できないとこまるので、「強く正規化する」（つまり停止する）ものが求められた。そこでカリー・ハワード対応、型つきラムダ計算が出てきて（ただし、型つきラムダ計算の中には、強く正規化しないものもあるようだ）。この型つきラムダ計算は、Javaで出てくる多態性（ポリモーフィズム）なんかを議論したり、圏論へと広がっていく。また、型の話は、型と命題の関係にいく。ここから先の話は後述の「では、仕様をどう表現するか：意味論」へつづく。
一方、「正しい」ことを証明する話は、「形式仕様」という議論の場に移っていく。この形式仕様では、仕様を論理的に記述して正しいことを示す「形式仕様言語」(Z,B,Event Bなど）と、正しいかどうかは証明できないけど、正しくない場合には検出する「モデル検査」(SPINなど）が出てきた。形式仕様言語の場合、正しいことを証明するには停止しないといけないが、そもそも、組み込みのプログラムは停止しないから、証明できなくなってしまう（なので、組み込みは、モデル検査やシミュレーションをよく使う）。証明は大変なので、自動定理証明が出てきたり、証明支援が出てきたり（coqなど）・・・っていう広がりを見ている。
【要求仕様をプログラムに実装できるか】
今までの話は、どんなもの（WHAT)が計算可能かという話だった。これとは別に、どうやって（HOW)要求仕様から設計プログラミングに落とし込めるかという話が「別に」ある。実務上では、要求仕様→設計→プログラミングといくが、ここに一貫性があるのか、完全性を保ちながら要求仕様からプログラミングまでの変換は可能であるかという話だ。「ない」となったら、「トレーサビリティマトリックス」とか作っている私たちの立場は？ってことになる。
実際、「一貫性はない」という意見があった。
要求仕様は「WHAT」を定義していて、設計は「HOW」を定義している。WHATはHOWに”とらわれてはいけない”（要求分析者は設計方法に左右されずに要求を出さないといけない）。だからこの間には断層がある。これが佐藤正美氏の提唱する「SDLCの断層」だった。この論理はウォーターフォールではまあいいんだけど、アジャイルになると、設計と要求定義は混在化してくる。そうすると、あちらこちらに断層ができて、一貫化したプログラムは作れない！という話になる。
一貫性がないなら、一つの視点で表現することができない。結果として、ふるまいの部分はアクティビティ図、構造はクラス図など、様々な図を使って仕様を表すUMLが広まった。が、これらの図は、何がどうつながっているのかが分かりにくい・一貫性が見えない・完全性は大丈夫なのかわからない事態を生みだした。
しかし、Lamsweerdeがゴールという概念を用いてKAOSという手法を提唱することにより、この断層はなくなった。そして、UMLの各図はKAOSから導きだせることが、1冊の本(Requirements Engineering: From System Goals to UML Models to Software Specifications)で示された。
KAOSの考え方は、様相論理を用いる。システム化に成功するということは、「現状Pから、システム化に成功した状態（要求を満たした状態）Qへ、いつかは状態遷移すること」である（P→□Q）と考える。そしてこのP→□Qをゴール（一番初めに定義するゴールをトップゴール）とよぶ。そうすると、ゴールの状態Qを表現すること（WHAT）が要求定義であり、設計とは現状Pから状態Qに状態遷移させる方法を考えること（P→□Qの→に相当）である。となる。つまり、２つの行為は１つのゴールで表現できる。
そしてこのゴールP→□Qを「何らかの手法で」分割し（詳細化・洗練という）、さらにそのゴールを分割して・・・と分割していったとき、すべてのゴールは、ある人によって実現可能なプロセスを実行することによって達成されるならば、全プロセスが実行されたときにゴールは達成すると考える。
（なお、ここでは達成ゴールを紹介した。ゴールにはほかに、回避ゴール、維持ゴールなどあるけど、詳細な説明は省略。似た話だから）
これにより、どうやって（HOW)要求仕様から設計プログラミングに落とし込めるかという話は、システムのトップゴールP→□Qから、どうやって詳細化を行って、実行可能な末端ゴールに一貫性（完全性）を保ちながら分解できるかという話に帰着した。この完全性を保ちながら分解する方法は、What部分を分解する要素分解と、状態遷移を分解するマイルストーン分解を行えば可能でありそうということを直感的に言っている人もいるが、数学的にはまだ証明されていない。ここが最前線。
なお、(Requirements Engineering: From System Goals to UML Models to Software Specifications)の表紙には、バベルの塔が書かれている。システムをUMLの様々な図というか言語（UMLのLは言語のL)で表した混乱を、この本で終止符を打つということでしょうか？日本はともかく、世界的にこの本は要求仕様の教科書となっている。
【では、仕様をどう表現するか：意味論】
ただ、ここではP→□Qの状態PやQの表現方法については議論していない。なので、次は「状態はどのように表現できるか。単なる記号ではなく、意味を持った形で表現できるのか？」ということが議論の対象になる。
現状は、この状態（要求仕様）を自然言語で書いているが、それだとあいまいになる。そこで、論理式で書くことになる（そもそも、様相論理なので、論理式だよね）。記号を論理式で書く・・・この方向は、記号論理学の話から、ミニマリストプログラム、CCG(Combibatory Categorial Grammars)、DisCoCatへとつながっていく。ここら辺が最新なの？
また命題と型とが結びついて、すべての命題がある型であるというホモトピー タイプ セオリー（HoTT）が出てくる。型つきラムダ計算から来た流れは、この辺が最先端？
でも、これらも１つの表現方法だけど、実際のプログラムでは、項目と値によるエンティティモデルやクラス・オブジェクトで表現したりする。
さらには、AIの世界だと、特徴ベクトルという形で状態を表現し、その特徴ベクトルの演算を考えるようになってきた（Word2Vec)この辺が、先端かしら・・・
ということで、意味論の分野は、論理（命題）、型、特徴ベクトル、項目と値を、どんな感じで「まぜまぜ」するのかが話題。 ＜ いまここ。
【ちゃぶ台返しの量子コンピュータ】
ここで、ちゃぶ台返しが起こる。量子コンピューターは、これらの流れと全く違った計算方法をする。いわく、ブラとケットがでてきてブラケット・・・わけわからん。
そのうえ、もっとわけわからんことが起こってる。いわく
・答えは、「これ」と求まらない。確率的に求まる（は、はい？？）
・アルゴリズムがないと、計算できない
そのアルゴリズムで、素因数分解するものは、ある。ショアのが。
で、これでパスワードが無効になるとか言われて話題になっている（サイエンスZEROでも再放送してた）。
もう一つ、行列式は解ける。このアルゴリズムがある。
で、さっきの意味論に戻ってくる。特徴ベクトルは行列で表してるけど、それなら、量子コンピューターでも扱える？
この辺っていうか、量子コンピューター全体が先端
【量子コンピューターとAI：不確かさ】
量子コンピューターは確率的に答えが求まるけど、AIの機械学習も確率的に求める。
いままでのバチンと答えが求まるものと違う。
このような確率的、不確かななかで、どう計算するのかというのが先端の話題。
不確かさの中でのAIのテストとか、不確かさの中での形式仕様PATとか
不確かさについて扱うのが、今先端。
今後は、確率論的ということで、ベイズが入ってくるか？入ってくるならどんな感じで？
なんかが、近未来的な話なのでしょうか・・・
【で・・・】
こんな話、おもしろいですか？
おもしろいなら、プログラムを学ぶことを目的にすることもアリだと思うけど、
（将来、量子コンピューターの方向に進むなら、いままでの勉強は無駄になっちゃうけど・・・）
たぶん、こういうことをやりたい人はごくわずかで、プログラムを「作る」のが楽しいんではなくて？
アクセス
トータル
ランキング
