【F*】依存型っていいの？【Coq】

**デフォルトの名無しさん** · 2019/04/09(火) 20:31:43.12

依存型の有意性について語るスレッドです。
数学に詳しい方々の知識を教えてください。

**デフォルトの名無しさん** · 2019/04/10(水) 14:11:26.65

Idrisは分かりやすいよ

**デフォルトの名無しさん** · 2019/04/11(木) 10:14:06.35

この動画で、依存型の基本的な使い方を解説をしているよ。Agdaです。
https://www.youtube.com/watch?v=uxSPJLrYyak

**デフォルトの名無しさん** · 2019/05/01(水) 19:59:53.75

数学に詳しくはないが、
Agdaについては、オレゴンサマースクールのDan. Licata氏とIan Voysey氏の講義が面白かった。
2013年の公式HPで見える。また見たくなってきた。

証明支援系ってゲームっぽいよね。動画の最後でCoqが○○でAgdaは□□みたいな話が出てきてた。

**デフォルトの名無しさん** · 2019/05/07(火) 16:33:30.27

multicore ocamlは分かりやすいのでしょうか？

**デフォルトの名無しさん** · 2019/05/09(木) 19:05:05.55

CoqがチンコでAgdaはマンコ？

**デフォルトの名無しさん** · 2019/05/25(土) 20:26:31.13

Coq：Calculus of Construction ではなく Calculus of Inductive Construction
Agda：Martin-Loef Type Theory
どう違うのかはわからん
でもCoCのが単純そう

**デフォルトの名無しさん** · 2020/02/15(土) 00:25:03.50

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でない場合にはエラーを出して教えてほしいところだ
こういう場合には行列の型自体が行数と列数を持っていれば話はカンタンになる
もっとも実世界で使うためには存在型という工夫が必要になるが

**デフォルトの名無しさん** · 2020/02/15(土) 00:26:40.07

あ、少し言い間違えた感
1==1というのは整数の型ではなく、「1は1と等しい」という命題を表す型

Coqではeq_refl x: x == xというふうな感じで実装されている

**デフォルトの名無しさん** · 2020/02/15(土) 12:30:08.84

命題1==1が証明出来るってことが
1==1型の値が存在するってことに対応するわけでしょ

**デフォルトの名無しさん** · 2021/03/06(土) 13:52:33.80

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" ⇨ 型が合わないエラー

**デフォルトの名無しさん** · 2021/03/06(土) 13:54:16.98

最後は"123"やな
しつれい

**デフォルトの名無しさん** · 2021/03/07(日) 06:00:39.42

NGワード：Haskell

**デフォルトの名無しさん** · 2023/01/03(火) 08:49:48.69

制限解除記念かきこ