数学@ふたば
[ホーム]

[掲示板に戻る]
レス送信モード
おなまえ
E-mail
題  名
コメント
添付File []
削除キー(記事の削除用。英数字で8文字以内)

画像ファイル名:1624743823237.png-(12818 B)
12818 B無題Name名無し21/06/27(日)06:43:43No.115402そうだねx1 1月08日頃消えます
型ってなに?
集合とは違うの?
1無題Name名無し 21/06/27(日)10:35:52No.115403+
コンピュータは通常、整数しか扱えない。その整数もどれだけの大きさの整数を扱うかでメモリーを使う量が変わる。

その形式は色々考えられるが、形式ごとに変数が表せる範囲や、精度が変わるってこと。
その形式のことを型とか言うわけだ。
2無題Name名無し 21/06/27(日)12:49:40No.115405+
もっと数学的に
More mathematically
3無題Name名無し 21/06/27(日)15:23:23No.115406+
例えば、同じ整数型でも0か1の組み合わせ(ビット)の数で型が分けられている。

int16 なら16ビット符号あり整数。
int32 なら32ビット符号あり整数。
int64 なら64ビット符号あり整数。

それぞれ扱える整数の範囲が違い、ビット数が多くなれば扱える範囲が広がるが、メモリーを食う。
今のCPUは64ビットか32ビット。32ビットマシンで64ビット整数を扱うにはちょっとした工夫が必要となる。

unsigned int という型もあり、これは正の数だけを扱うことにした整数型。これを使うと扱える数の範囲が2倍になるが負数は扱えない。

float , double というのは、数を実数部×指数部という2つの数に分け小数を扱えるようにしたもの。doubleはfloatの2倍の容量を使い、2倍の精度で計算できる。

ちなみに、実際にはどのようなビット構成になっているかは機種ごとに違っているが…今は IEEE754 の構成になっているはず。これが結構複雑というか、なんでこう定義したのかーというか。まあ、今は機械で計算させるんだけどね。
4無題Name名無し 21/06/27(日)16:07:59No.115407+
    1624777679014.jpg-(149284 B)
149284 B
いやそういう実装上の話では無くて型の公理と集合の公理の違いが知りたい
そもそも型理論にZF公理みたいなのってあるの?
5無題Name名無し 21/06/27(日)18:26:23No.115408+
型なんてコンピュータの実装上の都合じゃないの?
チューリングのいうマシンに型なんて概念ないでしょ
深くは調べてないけど
6無題Name名無し 21/06/27(日)19:20:34No.115409+
いや型自体はコンピュータの前からあるよ
プログラミングに応用されてるってだけでコンピュータ特有の概念じゃない
7無題Name名無し 21/06/27(日)21:44:16No.115410+
でも、コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。桁あふれとか、切り捨て・四捨五入とかあるし。
そんなんでZF公理系と言っても…
8無題Name名無し 21/06/27(日)22:45:21No.115411+
とりあえずコンピュータの話は忘れてもらって…
9無題Name名無し 21/06/27(日)22:45:38No.115412+
スレ画が良くなかったのかもしれない
10無題Name名無し 21/06/28(月)00:14:10No.115413+
>コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。
そもそも加法は全単射じゃないのでは
11無題Name名無し 21/06/28(月)00:17:45No.115414+
型は集合とだいたい同じなんじゃないの
だから部分型とか直和とか直積とか型の関数とか型の型とかを考えることができる
12無題Name名無し 21/06/28(月)00:24:14No.115415+
集合を包含してる感じだろうけど型にあって集合に無いのってなんだろ
13無題Name名無し 21/06/28(月)01:00:31No.115416+
コンピュータの実装なしの型の定義って…わからんw

型の型?コンピュータだと、機械語のその型へのポインターみたいなヤツ?w
型の関数?指定した型を返す関数?
数学だとどうなるんだ?

実数や整数だと加法の関数を定義すると、全単射なんじゃ?
14無題Name名無し 21/06/28(月)03:07:30No.115417そうだねx1
1+3も2+2も4になるのにどこが全単射なんじゃ……
15無題Name名無し 21/06/28(月)06:19:17No.115418+
>型の型?コンピュータだと、機械語のその型へのポインターみたいなヤツ?w
例えば 123 : Int だけど Int : Number みたいなのがあっても良いって事かと
プログラミングで言うと型クラスに相当する感じかな?
16無題Name名無し 21/06/28(月)06:56:37No.115419+
どっちかと言うとカインドのことなのかな?
17無題Name名無し 21/06/28(月)07:03:40No.115420+
>型の関数?指定した型を返す関数?
これはここに乗ってる奴かな?
https://qiita.com/HirotoShioi/items/39fc492401e4dcbc8cba
Zero型とSucc Zero型, Succ(Succ Zero)型, ... と作って行って型で"自然数"を作ったり出来るらしい
で更にその"自然数"同士を足すAdd型族というのが定義できるとか
18無題Name名無し 21/06/29(火)19:12:26No.115424+
俺の理解が間違ってるのかもしれんが
「集合の集合」のことじゃなかったっけ
「全ての集合の集まり」をふつうの集合のように扱うと矛盾するとRussellが証明して
当のRussellが「集合の集合」「集合の集合の集合」以下略を使いまくれば
これを解決できるのではないかと対策案として提示したやつ
応用上いろいろと便利な方法ではあったが
「全ての集合の集まり」対策としては失敗したとか何とか
その後Quineの系譜がこの路線で(原子的元urelementsを追加して)
「全ての集合の集まり」対策に成功したZFC公理系とほぼ遜色なく
数学諸概念を構成できるNFU公理系を作ったとか何とか(詳しくねえ)
19無題Name名無し 21/06/29(火)23:22:21No.115425+
>「集合の集合」のことじゃなかったっけ
これは真のクラスって奴だと思う
んでパラドックス発見したのはカントールじゃなかったかな
ラッセルのパラドックスはR={x| x∉x}に関する奴
型は何か値の右側に注釈として付いてる感じのイメージ
123 : 自然数
みたいな
この"自然数"が型
20無題Name名無し 21/06/30(水)06:14:24No.115426+
>これは真のクラスって奴だと思う
>んでパラドックス発見したのはカントールじゃなかったかな
>ラッセルのパラドックスはR={x| xx}に関する奴
あっしまった
独学だとこういうところがうろ覚えになっちゃう
>型は何か値の右側に注釈として付いてる感じのイメージ
>123 : 自然数
>みたいな
>この"自然数"が型
確かにそういう使われ方してるね
「これらはこれの型の例であり他の型の例ではない」
「この型とはこれこれの条件を満たす集合である
(条件のない単なるラベルの貼り付けられた集合のこともある)」
こうか?
21無題Name名無し 21/06/30(水)06:59:44No.115427+
『圏論の歩き方』という教科書というよりも大学講義のカタログみたいな本あるけど
第4章『プログラム意味論と圏論』の要約を発掘したら
「Curry-Howard対応というやつで型は命題のようなものと見なせる」という記述があった
別のプログラム系の人の書いた名前の通り『型理論』って本だと
変数や変数の(ラムダ計算の)式としての「項」は「型」を「持ち」
実際には型とはまた別の変数や変数の右結合で出来ている
(例えば整数型や二値真理値型や「整数型(の項)を入力したら二値真理値型(の項)を出力するなんか型」等)
ということで集合というよりは式と関係のある命題として考えた方がいいのだそうな
どういう関係かはちょっと分からない(部分集合とは考えにくいから順序対か対応だと思う)
22無題Name名無し 21/06/30(水)07:09:22No.115428+
だから>>18はナシ
書いといて何だがごめんなさい
23無題Name名無し 21/06/30(水)07:34:48No.115429+
Curry-Howard対応ってのは例えば型付き計算の
「x : double, f : double -> int と言うデータから f(x) : int を計算するプログラムが作れます」
と言う事実の型の部分だけ見ると,
「double, double -> int から int が計算できます」
となって, これが論理学の
「A, A -> B を仮定すると B が導かれる」
(モーダス・ポネンス)
となんか似てるねってなる奴だね
すごく抽象的な関係だから型(ここで言うdouble, int)と命題(A, B)が同じですよって言われても「?」ってなるだけな気もする
集合{1,2,3}と{りんご,みかん,バナナ}が同型ですよって言われても1=りんご,3=バナナだったんだ!とはならないのと同じ感じで
24無題Name名無し 21/06/30(水)07:46:12No.115430+
ただ集合には結構似てる気がして, 例えば
x : double, f: double -> int
っていうのも,
x ∈ double, f ∈ Map(double, int)
(Map(A,B)は集合Aから集合Bへの関数の集合)
と言い換えて違和感ないし
25無題Name名無し 21/07/02(金)06:09:19No.115431+
命題は真偽値が付かなきゃいけないという制約付きだけど型と集合はそういうのないのが大きな違いか
26無題Name名無し 21/07/04(日)10:44:05No.115450+
    1625363045529.png-(245054 B)
245054 B
なんかほぼ答えみたいなの見つけた
型が何なのかは色々解釈の余地があるらしい
と言うか型ってそれだけ色々なものに共通した性質(形式?)だったってことか
>第二部:「型の理論入門」
>ページ 169
https://www.marulabo.net/docs/type-theory-2/
27無題Name名無し 21/07/04(日)14:26:28No.115451+
    1625376388879.png-(86614 B)
86614 B
>なんかほぼ答えみたいなの見つけた
メチャクチャアツイなこれとその前のプレゼン資料
型とは素朴にはまず「要素や写像に伴っている何らかの性質の集合」だったが
それは「階層構造を持っており自分の型の下位でない型には写像を使う事が禁じられているもの」であった
その縛りは「それら要素を証明に見立てて型を命題に見立てたら
結論となる命題が関係ないもの同士の証明同士を関連付けても
その関連付けた写像はどっちの結論にも行きつく訳ないから居場所ないじゃん」とか
あるいは「それら要素を点に見立てて型を空間に見立てたら
空間が関係ないもの同士の点同士の間の線がどっちかの空間に入ってる訳ないじゃん」とか
直感的にはそういう意味合いになるのだと解釈したよ
たぶんこの画像のような感じではなかろうか(きたねー手書きで申し訳ないが)
28無題Name名無し 21/07/04(日)20:17:32No.115452+
うーん難しいな
モーダスポネンスと関数適用が何故似てるか?って話の理屈がそうなってるって話かな?それとも
>No.115424
の集合、集合の集合、集合の集合の集合、…って階層が型には備わってるって話の方か?
29無題Name名無し 21/07/04(日)20:42:36No.115453+
>モーダスポネンスと関数適用が何故似てるか?って話の理屈がそうなってるって話かな?
こっちに近い話かな
「要素aが集合Aに所属する&要素bが集合Bに所属するとき
それらの間の写像はAにもBにも所属してない
これは論理式でも点でも同じである
この「違う集合同士の要素同士の写像はどちらの集合にも所属していない」ことを強調すると
「違う型同士の要素同士の写像はどちらの型でも扱えない」ということと要は同じ意味なので
つまりやはり型とは集合のことなのでは?」ということを言いたい図だった
30無題Name名無し 21/07/04(日)20:44:33No.115454+
>集合、集合の集合、集合の集合の集合、…って階層が型には備わってるって話の方か?
こっちはさっきの図では描けなかったが
型Aの部分集合として下位階層の型Sを考えて
Sの中の要素a'を想定したら当然それは型Aの要素でもあるので
aとa'の写像は型Aの中で問題なく扱えるし前述の通り型Aの外にまたぐと扱えなくなる
これならやはりさっき言った通り「型=集合」という認識でよさそう
(集合の集合云々だから「大きくなる」と思いきや
部分集合云々の「小さくなる」話になっているのは自分でも引っかかるが)
31無題Name名無し 21/07/04(日)22:08:21No.115455+
階層があるって話はx∈xみたいなのを避けるために
(x : A) ∈ (y : B), (BはAより上位の型)
みたいな感じで両辺違う型にしようっていう話だったと思う
部分集合とはまたちょっと違う気がする
32無題Name名無し 21/07/06(火)02:47:28No.115457+
https://proc-cpuinfo.fixstars.com/2017/05/division-operation-optimization/
グロタンディーク構成

負の数の補数表現

ディラックの海
33無題Name名無し 21/07/06(火)08:05:53No.115458+
グロタンディーク構成って要素の圏の一般的な奴らしいけど型と何か関係あるの?
34無題Name名無し 21/07/10(土)02:20:14No.115470+
5時から男
35無題Name名無し 21/07/10(土)10:25:42No.115471+
古めかしいが単純明快で懇切丁寧な論理学の教科書である
前原昭二『記号論理入門』の第8章§1を読んでいたら

>∀Fとか∃Fのような<述語に関する限定作用素>をも合わせ考える論理を2階の述語論理といいます。
><述語の述語>に関する限定作用素を許す3階の述語論理というように、高階の述語論理-あるいは型の理論ともよばれる-というものを一般に考えることもできます。

ってあったのよ
この本の第1版は1967年10月15日なんで
当時「高階の述語論理≒型理論」という認識があったということが読み取れる

またこの本では第1章§5で述語と性質と概念と条件と命題関数と(内包で書ける)集合を同一視するので
つまりは型=述語の述語=(内包で書ける)集合のさらなる(内包で書ける)集合であると考えられる
これだと今までの議論と整合的な見解でもある
36無題Name名無し 21/07/10(土)18:18:13No.115476+
歴史的にはラッセルが集合論のパラドクスを回避するために導入したのが型(タイプ)だけど、ラッセル(とホワイトヘッド)はさらに意味論的パラドクスというのを回避するために階(オーダー)というのも導入した。
でもこれらは定義によっては同じになるので前原先生なんかは同一視して教科書を書きがち。

命題と型を同一視するのは、自然演繹の証明と型付けの導出体系が同型になるからというだけでなく、命題の意味をその証明の集まりと同一視する(BHK解釈)と型っぽくなるという背景もある。

プログラムの表示的意味論というのを与えるとプログラムの型を数学的な集合と対応づけられるようになるよ。
37無題Name名無し 21/08/17(火)07:14:03No.115757+
>歴史的にはラッセルが集合論のパラドクスを回避するために導入したのが型(タイプ)だけど、ラッセル(とホワイトヘッド)はさらに意味論的パラドクスというのを回避するために階(オーダー)というのも導入した。
>でもこれらは定義によっては同じになるので前原先生なんかは同一視して教科書を書きがち。
今気づいたけど別物なんですか! 混同してた…

- GazouBBS + futaba-