0001デフォルトの名無しさん2019/04/09(火) 20:31:43.12ID:KZ504O8A
依存型の有意性について語るスレッドです。
数学に詳しい方々の知識を教えてください。
0004デフォルトの名無しさん2019/05/01(水) 19:59:53.75ID:blvpCat5
数学に詳しくはないが、
Agdaについては、オレゴンサマースクールのDan. Licata氏とIan Voysey氏の講義が面白かった。
2013年の公式HPで見える。また見たくなってきた。
証明支援系ってゲームっぽいよね。動画の最後でCoqが○○でAgdaは□□みたいな話が出てきてた。
multicore ocamlは分かりやすいのでしょうか？
0007デフォルトの名無しさん2019/05/25(土) 20:26:31.13ID:3c9sJ6MS
Coq：Calculus of Construction ではなく Calculus of Inductive Construction
Agda：Martin-Loef Type Theory
どう違うのかはわからん
でもCoCのが単純そう
0008デフォルトの名無しさん2020/02/15(土) 00:25:03.50ID:igxgvzDX
age
依存型は証明に大いに役に立つ
「証明: 命題」命題が証明の型になるCurry-Howard同型対応を使うとプログラムを書く＝証明するになる
命題は証明の型、つまり型だ
例えば「すべての整数nに対して、n=nである」という命題は、「∀n:Int. n==n」というふうな型として表せる。
こういう∀付きの型はnに適当な整数を代入すると1==1や2==2のように個々の整数の型が得られる
つまり、値をパラメータに取る型ということだ
値をパラメータに取る型＝依存型だ
それだけではなく、数学的な計算例えばAIでよく使われる行列の計算にも役に立つ
3×4の行列matAとm×2の行列matBがあったとき、「matA * matB」という計算は、
もしmが4でない場合にはエラーを出して教えてほしいところだ
こういう場合には行列の型自体が行数と列数を持っていれば話はカンタンになる
もっとも実世界で使うためには存在型という工夫が必要になるが
0009デフォルトの名無しさん2020/02/15(土) 00:26:40.07ID:igxgvzDX
あ、少し言い間違えた感
1==1というのは整数の型ではなく、「1は1と等しい」という命題を表す型
Coqではeq_refl x: x == xというふうな感じで実装されている
命題1==1が証明出来るってことが
1==1型の値が存在するってことに対応するわけでしょ
0011デフォルトの名無しさん2021/03/06(土) 13:52:33.80ID:CZ4Qrc8C
idrisの本読み始めたは
めっちゃロマンある😁
Haskellのservantとかこれで書けばスッキリしそう
StrInt : Bool -> Type
StrInt True = Int
StrInt False = String
eval : (x : Bool) -> StrInt x -> String
eval x si = case x of
True = cast si
False = si
eval True 123 ⇨ 123
eval False "abc" ⇨ "abc"
eval True "abc" ⇨ 型が合わないエラー
0012デフォルトの名無しさん2021/03/06(土) 13:54:16.98ID:CZ4Qrc8C
最後は"123"やな
しつれい
0013デフォルトの名無しさん2021/03/07(日) 06:00:39.42ID:wLDkdLSw
NGワード：Haskell