この質問には、いくつかの深いコンピュータサイエンスとプログラミングの概念が含まれています。具体的には、「強く正規化された言語」、「チューリング完全性」、および「停止問題」に関するものです。それぞれを簡潔に説明してから、全体的な意味を解説します。
強く正規化された言語: 強く正規化されたプログラミング言語では、すべての有効なプログラムが必ず終了します。無限ループや再帰が不可能な場合が多いです。
チューリング完全性: 言語やシステムがチューリング完全であるとは、それが任意のアルゴリズムや計算をシミュレートする能力を持っていることを意味します。これは一般に、言語が非常に強力であることを示しています。
停止問題: アラン・チューリングによって未解決であることが示された問題です。具体的には、ある特定の入力に対して与えられたプログラムが終了するかどうかを判定するアルゴリズムが存在しないことが示されました。
これらの概念を組み合わせて考えると、強く正規化された関数型プログラミング言語は、プログラムが必ず終了するため、チューリング完全ではないと言えます。なぜなら、チューリング完全な言語は停止しないプログラム(無限ループなど)を表現できる必要があるからです。
さらに、強く正規化された言語がチューリング完全であると仮定すると、プログラムが型チェックに通るかどうかによって、そのプログラムが停止するかどうかを判断することができる。しかし、これは停止問題が解決できてしまうことを意味するため、このような言語が存在することはあり得ません。
要するに、強く正規化された関数型プログラミング言語がチューリング完全であると仮定すると、停止問題を解く方法が存在することになってしまうため、そのような言語は存在しない、というのがこの文の意味です。