【学術】型理論
1 ：非決定性名無しさん：
龍田真『型理論』
読んでもわからん。つーか、読めない。
読んでもわからん。つーか、読めない。
|
|
|
2 ：非決定性名無しさん：02/04/25 12:01
それは、論文へのポインタじゃないの？
漏れも読めない（Ｔ__Ｔ）
漏れも読めない（Ｔ__Ｔ）
「レクチャーノート ソフトウェア学〈1〉型理論」(著)龍田 真
http://www.amazon.co.jp/exec/obidos/ASIN/476490201X/qid=1019705722/sr=1-78/ref=sr_1_2_78/250-2535033-0511438
内容（「MARC」データベースより）
日本ソフトウェア科学会の学会誌コンピュータソフトウェアに掲載された解説記事を一つにまとめ、本の形にした。
型理論を概説した書。
＃しまっちゃってて、今手元にない...。
http://www.amazon.co.jp/exec/obidos/ASIN/476490201X/qid=1019705722/sr=1-78/ref=sr_1_2_78/250-2535033-0511438
内容（「MARC」データベースより）
日本ソフトウェア科学会の学会誌コンピュータソフトウェアに掲載された解説記事を一つにまとめ、本の形にした。
型理論を概説した書。
＃しまっちゃってて、今手元にない...。
4 ：非決定性名無しさん：02/04/28 12:49
整数論とはまた違うものなの？
5 ：非決定性名無しさん：02/04/29 00:31
整数論と型理論って関係あるんですか？
確かにゲーデルは不完全性定理の証明に型の体系を用いていますが、
それと自然数論とはまた別物のような気がするのですが。。自信なし
確かにゲーデルは不完全性定理の証明に型の体系を用いていますが、
それと自然数論とはまた別物のような気がするのですが。。自信なし
6 ：非決定性名無しさん：02/04/29 01:09
ラッセルの？
7 ：非決定性名無しさん：02/04/29 01:11
型推論マンセー
8 ：非決定性名無しさん：02/04/29 03:21
>7
type theoryのtypeとプログラミング言語での（型推論にみられるような）typeは相当違うぞ、おぃ。
type theoryのtypeとプログラミング言語での（型推論にみられるような）typeは相当違うぞ、おぃ。
9 ：非決定性名無しさん：02/04/29 03:27
>>8
煽りじゃなくて純粋な疑問なんだけど、どう違うの？
煽りじゃなくて純粋な疑問なんだけど、どう違うの？
10 ：非決定性名無しさん：02/04/29 14:57
どう違うのか知りたいage
11 ：非決定性名無しさん：02/04/30 23:50
教えてくれage
12 ：非決定性名無しさん：02/04/30 23:57
実は俺も木になる
13 ：非決定性名無しさん：02/05/01 13:08
煽りっぽくなってきたがまだまだ知りたいage
14 ：非決定性名無しさん：02/05/01 18:18
type theoryのtypeって集合のネストの深さみたいな話じゃなかったか？
15 ：8：02/05/06 20:14
う、確かに型理論はもともとプログラミングの型の理論だ。スマソ。
でもさ、structureや型を代数論上に載せるときには、
普通typeという言葉は避けてsortという用語を使うよね。
それに今のtype theoryの話って、プログラミング言語上の話は少ないじゃん。
応用としてはML方面とかいろいろあるけど。今現在、騙り論とかtype theoryとかいう
言葉を聞いたなら、直観論理との対応とか、マーチンロフ以降の証明と型との対応とか、
そっち方面を思い浮かべるほうが多いんじゃない？かなあ...弱い言い訳か。
でもさ、structureや型を代数論上に載せるときには、
普通typeという言葉は避けてsortという用語を使うよね。
それに今のtype theoryの話って、プログラミング言語上の話は少ないじゃん。
応用としてはML方面とかいろいろあるけど。今現在、騙り論とかtype theoryとかいう
言葉を聞いたなら、直観論理との対応とか、マーチンロフ以降の証明と型との対応とか、
そっち方面を思い浮かべるほうが多いんじゃない？かなあ...弱い言い訳か。
何故にずれたカキコするの
17 ：非決定性名無しさん：02/08/28 23:15
オブジェクト指向と型理論との関係ってどうよ。
アフォな漏れに教えてください。
アフォな漏れに教えてください。
18 ：非決定性名無しさん：02/10/24 02:50
ラッセルの型理論ってなんですか？
19 ：非決定性名無しさん：03/02/27 23:36
普段この板は見ないのでずいぶん亀レスですが
>>15
sortを使うのは1st-orderの場合．
higher-orderではプログラミング言語でもtypeというのが普通．
というか80年代後半から90年代にかけて
型理論はむしろコンピュータサイエンスの一環として大きく発展した．
いまは基礎理論はおおむね様子がわかったので応用に向かっている感じ．
分野はプログラミング言語，セキュリティ，コンパイラ，
検証システム，自然言語処理，知識処理，といったところですかね．
やっぱりInternetやWeb絡みの応用が多いかな．
>>15
sortを使うのは1st-orderの場合．
higher-orderではプログラミング言語でもtypeというのが普通．
というか80年代後半から90年代にかけて
型理論はむしろコンピュータサイエンスの一環として大きく発展した．
いまは基礎理論はおおむね様子がわかったので応用に向かっている感じ．
分野はプログラミング言語，セキュリティ，コンパイラ，
検証システム，自然言語処理，知識処理，といったところですかね．
やっぱりInternetやWeb絡みの応用が多いかな．
20 ：非決定性名無しさん：03/05/20 00:15
で、この本はどうなのよ？
あげ厨は苦しみもがいて死んでください。
あぼーん
23 ：非決定性名無しさん：03/08/31 21:16
char int short long float double byte ......
24 ：非決定性名無しさん：03/09/02 04:07
それは、論文へのポインタじゃないの？
漏れも読めない（Ｔ__Ｔ）
漏れも読めない（Ｔ__Ｔ）
25 ：非決定性名無しさん：03/12/10 21:40
学術スレage
26 ：非決定性名無しさん：04/01/01 22:11
学術スレage
27 ：非決定性名無しさん：04/01/02 20:06
学術スレage
28 ：非決定性名無しさん：04/01/03 22:58
学術ｽﾚage
そんなしょうもないageなんてどーでもいい。
それより、はしのえみ好きだろ？
それより、はしのえみ好きだろ？
30 ：非決定性名無しさん：04/01/04 09:13
はしのえみ好き
どのスレも
スレタイに【学術】がはいっている。
スレが、２００２年４月頃に建てられている。
スレタイに【学術】がはいっている。
スレが、２００２年４月頃に建てられている。
32 ：非決定性名無しさん：04/01/07 22:55
学問あげ
33 ：非決定性名無しさん：04/01/09 00:04
学問あげ
34 ：非決定性名無しさん：04/01/27 05:44
35 ：非決定性名無しさん：04/01/27 06:33
学術あげ
36 ：非決定性名無しさん：04/01/27 06:33
学術あげ
37 ：非決定性名無しさん：04/01/27 06:33
学術あげ
38 ：非決定性名無しさん：04/01/27 06:34
学術あげ
39 ：非決定性名無しさん：04/01/27 06:34
学術あげ
40 ：非決定性名無しさん：04/01/27 06:35
学術あげ
41 ：非決定性名無しさん：04/05/17 01:36
学術AGE
学問揚げ
44 ：非決定性名無しさん：04/05/25 06:11
氏にます
45 ：非決定性名無しさん：04/06/11 18:35
生㎞
46 ：非決定性名無しさん：04/06/24 08:41
学術揚げ
47 ：非決定性名無しさん：
久々に学問上げ