7

タイプチェッカーで、特定の計算が終了することが保証されているかどうかを指定できる関数型言語はありますか? あるいは、Haskellだけでこれを行うことはできますか?

Haskellに関して、この回答では、ポスターは次のように述べています

これについての通常の考え方は、すべての Haskell 型が「リフト」されているというものです。これには ⊥ が含まれています。つまり、 だけではなくにBool対応します。これは、Haskell プログラムが終了することが保証されておらず、例外が発生する可能性があるという事実を表しています。{⊥, True, False}{True, False}

一方、アグダに関するこの論文は、次のように述べています。

正しい Agda プログラムとは、型チェックと終了チェックの両方に合格するプログラムです。

つまり、すべての Agda プログラムが終了し、BoolAgda の a は正確に に対応します{True, False}。

たとえば、Haskell では type の値を持つことができますIO a。これは、問題の値を計算するために IO が必要であることをタイプチェッカーに伝えます。Lifted a問題の計算が終了しない可能性があると主張する型を用意できますか? つまり、非終了を許可しますが、型システムで分離します。(明らかに、Agda のように、値を「確実に終了する」と「終了しない可能性がある」にのみ分けることができます) そうでない場合、これを行う言語はありますか?

4

1 に答える 1

4

あなたは確かにできます。しかし、それは完璧ではありません。定義により、終了する一部の計算は に存在する必要がありますLifted。これを停止問題と呼びます。

この考えをあきらめる前に、これは音ほど悪くはありません。Coq、Agda、およびその他の多くは、終了をチェックするためのヒューリスティックで問題なく動作します。

これが実際に問題になる言語は、定理を証明しようとしている Coq や Agda などの言語です。たとえば、型があるとしましょう

 Definition falsy := exists n, n > 0 /\ 0 > n.
 -- Read this as, 
 --   "The type of a proof that for some number n, n > 0 and n < 0"

Coq 構文。/\とを意味します。Coq や Agda でそのようなプロパティを証明するには、次のように書く必要があります。

Definition out_proof : falsy = ____.
-- Read this as
--   "A proof that there exists a number n < 0 and n > 0"

ある数、および____に対する証明はどこにありますか。まあ、これは間違っているので、これは非常に難しいです。明らかに、0 より小さい数と 0 より大きい数は存在しません。nn > 00 > nfalsy

しかし、無制限の再帰で非終了を許可すると、

 Definition bottom_proof : falsy = bottom_proof.

このタイプはチェックしますが、明らかに一貫性がありません! 何か間違っていることが証明されました！したがって、定理証明アシスタントは何らかの形式の終了チェックを強制します。

実用的になりたい場合は、この持ち上げられた型を使用して、基本的にタイプチェッカーに「バックオフ、これが終了しない可能性があることはわかっていますが、それで問題ありません」と伝えることができます。これは、ウェブサーバーなど、「永久に」実行したい場所など、現実世界のものを書くのに役立ちます。

本質的に、あなたは言語の分割を提案しています.一方では、物事を安全に証明できる「検証済みのコード」があり、もう一方では、永遠にループする可能性のある「安全でないコード」があります. との比較は正しいですIO。これは Haskell の副作用の分割とまったく同じ考え方です。

編集：コアカーシブデータ

コアカーシブ データについて言及しましたが、これはあなたが望むものではありません。アイデアは、永遠にループするということですが、「生産的に」そうします。本質的に、再帰で終了を確認する最も簡単な方法は、現在持っているものよりも厳密に小さい項で常に再帰することです。

Fixpoint factorial n := match n with
  | 0 => 1
  | S n' => n * factorial n'

コアカーションを使用すると、結果の用語は入力よりも「大きく」なければなりません。

Cofixpoint stream := Cons 1 stream

繰り返しますが、これは許可されていません

 Cofixpoint stream := stream
于 2013-10-18T18:04:34.557 に答える