私はHaskellウィキブックの表示セマンティクスに関するセクションに取り組んでいますが、この演習でちょっと立ち往生しています:
から始まる不動点の反復によって得られる不動点
も最小であり、他のどの不動点よりも小さいことを証明してください。(ヒント:
は cpo の最小要素であり、g はモノトーンです)。
次のステートメントは、演習に至るまでの概念の核心を定義しています (私は思います):
ここで、f は階乗関数であり、g が連続であるとすると、g の固定小数点として示されます。
g(f) = f が示されている部分は基本的に理解していると思いますが、演習をどうすればよいかはよくわかりません。私が理解していることから、階乗関数 f は最小不動点 (演算子に基づいて最小) ですが、
関数を と比較することが (直感的に) 意味することはまったく明確ではありません。例に示されている最小不動点以外。
g(x) は単調であるため、一方が他方よりも小さい 2 つのものに適用すると、結果は依然としてこの順序に従うことを理解しています。
関数 f' を取り、 を仮定することから証明を開始すると思います
。その場合、g の単調な性質を通じて、 を示すことができます
。次に、必然的に g(f') = g(f) または f' = f であることを示すことができれば、証明は完了したと思いますが、それを示す方法がわかりません。