私の理解では、静的に型付けされた言語で書かれたプログラムに特定の（小さな）欠陥のサブセットがないことを正式に証明するプログラムを書くことができる可能性があるということです。
これに関する私の問題は次のとおりです。
AとBの2つのチューリング完全言語があると仮定します。Aは「タイプセーフ」であると推定され、「B」はそうではないと推定されます。Aで書かれたプログラムの正しさをチェックするためにプログラムLが与えられたとしましょう。Lを適用してBで書かれたプログラムをAに翻訳するのを防ぐにはどうすればよいですか。PがAからBに翻訳される場合、なぜPLaではないのですか。 Bで書かれたプログラムの有効な型チェッカー？
私は代数の訓練を受けており、CSの勉強を始めたばかりなので、これが機能しない明らかな理由があるかもしれませんが、私は非常に知りたいです。この「型安全性」全体は、しばらくの間私にとって魚臭いものでした。
すべてのB'（Bで記述されたプログラム）を同等のA'（B'が正しい場合は正しい）に変換できる場合、言語Bは言語Aと同じくらいの「型安全性」を享受します（理論的な意味では、もちろん;-)-基本的にこれは、Bが完全な型推論を実行できるようなものであることを意味します。しかし、それは動的言語では非常に制限されています-たとえば、次のことを考慮してください。
if userinput() = 'bah':
thefun(23)
else:
thefun('gotcha')
ここでthefun（仮定しましょう）はint引数に対してはタイプセーフですが、str引数に対してはタイプセーフではありません。さて、そもそもこれをどのように言語Aに翻訳しますか...？
Aを静的に型付けされることになっているチューリング完全言語とし、A'を型チェックを削除したときにAから取得する言語とします（ただし、他の目的にも役立つため、型注釈は使用しません）。Aの受け入れられたプログラムは、A'の受け入れられたプログラムのサブセットになります。したがって、特に、A'もチューリング完全になります。
翻訳者PがBからAに（およびその逆に）与えられます。それは何をすることになっていますか？次の2つのいずれかを実行できます。
まず、BのすべてのプログラムyをAのプログラムに変換できます。この場合、Aのプログラムは定義上正しく入力されているため、LPyは常にTrueを返します。
第二に、PはBのすべてのプログラムyをA'のプログラムに変換できます。この場合、LPyはPyがAのプログラムである場合はTrueを返し、そうでない場合はFalseを返します。
最初のケースでは興味深いものは何も得られないので、2番目のケースに固執しましょう。これはおそらくあなたが言っていることです。Bのプログラムで定義された関数LPは、Bのプログラムについて何か面白いことを教えてくれますか？Pの変化の下で不変ではないので、私はノーと言います。Aはチューリング完全であるため、2番目の場合でも、そのイメージがたまたまAにあるようにPを選択できます。LPは常にTrueになります。一方、Pは、一部のプログラムがA'のAの補集合にマップされるように選択できます。この場合、LPはBの一部の（おそらくすべての）プログラムに対してFalseを吐き出します。ご覧のとおり、yのみに依存するものは何も得られません。
私はそれをより数学的に次のように言うこともできます：オブジェクトがプログラミング言語であり、射が1つのプログラミング言語から別のプログラミング言語への翻訳者であるプログラミング言語のカテゴリーCがあります。特に、射P：X-> Yがある場合、Yは少なくともXと同じくらい表現力があります。チューリング完全言語の各ペアの間には、両方向に射があります。CのオブジェクトXごとに（つまり、プログラミング言語ごとに）、Xのプログラムによって計算できる部分的に定義された関数の{X}（悪い表記、私は知っています）などの関連するセットがあります。各射P：X- > Yは、セットの包含{X}->{Y}を誘導します。アイデンティティ{X}->{Y}を誘発するすべての射P：X->Yを正式に反転させましょう。結果のカテゴリを呼び出します（数学的には、C'によるC）のローカリゼーション。ここで、包含A->A'はC'の射です。ただし、A'の自己同型では保存されません。つまり、射A->A'はC'のA'の不変量ではありません。言い換えると、この抽象的な観点から、「静的に型付けされた」属性は定義できず、言語に任意に付加できます。
私の主張をより明確にするために、C'は、たとえば、射としてのユークリッド運動とともに、3次元空間の幾何学的形状のカテゴリーと考えることもできます。その場合、A'とBは2つの幾何学的形状であり、PとQはBをA'に、またはその逆にもたらすユークリッド運動です。たとえば、A'とBは2つの球である可能性があります。ここで、A'のサブセットAを表すA'上の点を修正しましょう。この点を「静的型付け」と呼びましょう。Bのポイントが静的に型付けされているかどうかを知りたいです。したがって、そのような点yを取り、Pを介してA'にマッピングし、それがA'上のマークされた点であるかどうかをテストします。簡単にわかるように、これは選択したマップPに依存します。言い換えると、球上のマークされた点は、その球の自己同型（球をそれ自体にマップするユークリッド運動）によって保持されません。
これまでと同じことを指摘する別の方法は、あなたの質問が次のいずれかの矛盾による証拠を構成するということです。
または両方。私の直感によれば、後者がおそらくこだわりのポイントです。その型安全性はメタ言語的特性です。
それについて「怪しい」ものは何もありません。;）
自明でない[ 1 ]型システムTに関して型安全であるチューリング完全言語のセットは、チューリング完全言語の厳密なサブセットです。そのため、一般的なケースでは、 BからAへのトランスレータP -1は存在しません。したがって、translator- cum -type-checkerLP- 1もありません。
この種の主張に対するひざまずく反応は次のようになります。ナンセンス！AとBはどちらもチューリング完全なので、どちらの言語でも計算可能な関数を表現できます。そして、確かに、これは正しいです-あなたはどちらの言語でも計算可能な関数を表現することができます。ただし、かなり頻繁に、かなり多くを表現することもできます。特に、文字列「foo」と「bar」の算術和を喜んで取得しようとする式など、表示的意味論が明確に定義されていない式を作成できます（これがチャブスダッド アレックスマルテッリの答え）。これらの種類の表現は言語Bの「中に」あるかもしれませんが、表示的意味論が定義されていないため、言語Aで単に表現できない可能性があり、したがってそれらを翻訳する賢明な方法はありません。
これは静的型付けの大きな強みの1つです。型システムがコンパイル時に、前述の関数が任意のパラメーターを受け取ることを証明できない場合、算術加算演算子の結果が明確に定義されているパラメーターを受け取ることができます。不正なタイプとして拒否されます。
上記は静的型システムのメリットを説明するために与えられた通常の種類の例ですが、おそらく控えめすぎることに注意してください。一般に、静的型システムは、パラメーターの型の正確さを強制するだけに限定される必要はありませんが、実際には、コンパイル時に証明できるプログラムの任意の望ましいプロパティを表現できます。たとえば、取得したのと同じスコープ内でファイルシステムハンドル（データベース、ファイル、ネットワークソケットなど）を解放するという制約を適用する型システムを構築することができます。明らかに、これは、生命維持システムなどの分野で非常に価値があります。システムのできるだけ多くのパラメータの正確さは絶対に不可欠です。静的型システムを満足すれば、これらの種類の証明を無料で入手できます。
[ 1 ]自明ではないということは、すべての可能な表現が適切に型付けされているわけではないという意味です。
私の理解では、これはコンパイル時と実行時の関係に関係しています。静的に型付けされた言語では、型チェックの大部分はコンパイル時に実行されます。動的に型付けされた言語では、型チェックの大部分は実行時に実行されます。
これを逆に答えさせてください：
「動的」計画法には2つの異なるタイプがあります。
1つは「動的型付け」です。つまり、PythonのIDLEシェルのように、シェルに定義を入力してプログラムできるシェルがあります。
もう1つのタイプの動的計画法は、より理論的なものです。動的プログラムは、独自のソースを変更できるプログラムです。ある程度の取り入れが必要で、マイクロコントローラのプログラムメモリを変更するためによく使用されます。数値計算用のルックアップテーブルを生成することは、動的計画法と呼ばれることがあります。