Name名無し21/06/27(日)06:43:43No.115402そうだねx1
1月11日頃消えます 型ってなに？
集合とは違うの？

…No.115403+コンピュータは通常、整数しか扱えない。その整数もどれだけの大きさの整数を扱うかでメモリーを使う量が変わる。 その形式は色々考えられるが、形式ごとに変数が表せる範囲や、精度が変わるってこと。 その形式のことを型とか言うわけだ。

…No.115405+もっと数学的に More mathematically

…No.115406+例えば、同じ整数型でも0か1の組み合わせ（ビット）の数で型が分けられている。 int16 なら16ビット符号あり整数。 int32 なら32ビット符号あり整数。 int64 なら64ビット符号あり整数。 それぞれ扱える整数の範囲が違い、ビット数が多くなれば扱える範囲が広がるが、メモリーを食う。 今のCPUは64ビットか32ビット。32ビットマシンで64ビット整数を扱うにはちょっとした工夫が必要となる。 unsigned int という型もあり、これは正の数だけを扱うことにした整数型。これを使うと扱える数の範囲が２倍になるが負数は扱えない。 float , double というのは、数を実数部×指数部という２つの数に分け小数を扱えるようにしたもの。doubleはfloatの２倍の容量を使い、２倍の精度で計算できる。 ちなみに、実際にはどのようなビット構成になっているかは機種ごとに違っているが…今は IEEE754 の構成になっているはず。これが結構複雑というか、なんでこう定義したのかーというか。まあ、今は機械で計算させるんだけどね。

…No.115407+ いやそういう実装上の話では無くて型の公理と集合の公理の違いが知りたい そもそも型理論にZF公理みたいなのってあるの？

…No.115408+型なんてコンピュータの実装上の都合じゃないの？ チューリングのいうマシンに型なんて概念ないでしょ 深くは調べてないけど

…No.115409+いや型自体はコンピュータの前からあるよ プログラミングに応用されてるってだけでコンピュータ特有の概念じゃない

…No.115410+でも、コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。桁あふれとか、切り捨て・四捨五入とかあるし。 そんなんでZF公理系と言っても…

…No.115411+とりあえずコンピュータの話は忘れてもらって…

…No.115412+スレ画が良くなかったのかもしれない

…No.115413+>コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。 そもそも加法は全単射じゃないのでは

…No.115414+型は集合とだいたい同じなんじゃないの だから部分型とか直和とか直積とか型の関数とか型の型とかを考えることができる

…No.115415+集合を包含してる感じだろうけど型にあって集合に無いのってなんだろ

…No.115416+コンピュータの実装なしの型の定義って…わからんｗ 型の型？コンピュータだと、機械語のその型へのポインターみたいなヤツ？ｗ 型の関数？指定した型を返す関数？ 数学だとどうなるんだ？ 実数や整数だと加法の関数を定義すると、全単射なんじゃ？

…No.115417そうだねx11+3も2+2も4になるのにどこが全単射なんじゃ……

…No.115418+>型の型？コンピュータだと、機械語のその型へのポインターみたいなヤツ？ｗ 例えば 123 : Int だけど Int : Number みたいなのがあっても良いって事かと プログラミングで言うと型クラスに相当する感じかな？

…No.115419+どっちかと言うとカインドのことなのかな？

…No.115420+>型の関数？指定した型を返す関数？ これはここに乗ってる奴かな？ https://qiita.com/HirotoShioi/items/39fc492401e4dcbc8cba Zero型とSucc Zero型, Succ(Succ Zero)型, ... と作って行って型で"自然数"を作ったり出来るらしい で更にその"自然数"同士を足すAdd型族というのが定義できるとか

…No.115424+俺の理解が間違ってるのかもしれんが 「集合の集合」のことじゃなかったっけ 「全ての集合の集まり」をふつうの集合のように扱うと矛盾するとRussellが証明して 当のRussellが「集合の集合」「集合の集合の集合」以下略を使いまくれば これを解決できるのではないかと対策案として提示したやつ 応用上いろいろと便利な方法ではあったが 「全ての集合の集まり」対策としては失敗したとか何とか その後Quineの系譜がこの路線で（原子的元urelementsを追加して） 「全ての集合の集まり」対策に成功したZFC公理系とほぼ遜色なく 数学諸概念を構成できるNFU公理系を作ったとか何とか（詳しくねえ）

…No.115425+>「集合の集合」のことじゃなかったっけ これは真のクラスって奴だと思う んでパラドックス発見したのはカントールじゃなかったかな ラッセルのパラドックスはR={x| x∉x}に関する奴 型は何か値の右側に注釈として付いてる感じのイメージ 123 : 自然数 みたいな この"自然数"が型

…No.115426+>これは真のクラスって奴だと思う >んでパラドックス発見したのはカントールじゃなかったかな >ラッセルのパラドックスはR={x| x��x}に関する奴 あっしまった 独学だとこういうところがうろ覚えになっちゃう >型は何か値の右側に注釈として付いてる感じのイメージ >123 : 自然数 >みたいな >この"自然数"が型 確かにそういう使われ方してるね 「これらはこれの型の例であり他の型の例ではない」 「この型とはこれこれの条件を満たす集合である （条件のない単なるラベルの貼り付けられた集合のこともある）」 こうか？

…No.115427+『圏論の歩き方』という教科書というよりも大学講義のカタログみたいな本あるけど 第4章『プログラム意味論と圏論』の要約を発掘したら 「Curry-Howard対応というやつで型は命題のようなものと見なせる」という記述があった 別のプログラム系の人の書いた名前の通り『型理論』って本だと 変数や変数の（ラムダ計算の）式としての「項」は「型」を「持ち」 実際には型とはまた別の変数や変数の右結合で出来ている （例えば整数型や二値真理値型や「整数型（の項）を入力したら二値真理値型（の項）を出力するなんか型」等） ということで集合というよりは式と関係のある命題として考えた方がいいのだそうな どういう関係かはちょっと分からない（部分集合とは考えにくいから順序対か対応だと思う）

…No.115428+だから>>18はナシ 書いといて何だがごめんなさい

…No.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=バナナだったんだ！とはならないのと同じ感じで

…No.115430+ただ集合には結構似てる気がして, 例えば x : double, f: double -> int っていうのも, x ∈ double, f ∈ Map(double, int) （Map(A,B)は集合Aから集合Bへの関数の集合） と言い換えて違和感ないし

…No.115431+命題は真偽値が付かなきゃいけないという制約付きだけど型と集合はそういうのないのが大きな違いか

…No.115450+ なんかほぼ答えみたいなの見つけた 型が何なのかは色々解釈の余地があるらしいと言うか型ってそれだけ色々なものに共通した性質（形式？）だったってことか>第二部：「型の理論入門」>ページ 169https://www.marulabo.net/docs/type-theory-2/

…No.115451+ >なんかほぼ答えみたいなの見つけた メチャクチャアツイなこれとその前のプレゼン資料型とは素朴にはまず「要素や写像に伴っている何らかの性質の集合」だったがそれは「階層構造を持っており自分の型の下位でない型には写像を使う事が禁じられているもの」であったその縛りは「それら要素を証明に見立てて型を命題に見立てたら結論となる命題が関係ないもの同士の証明同士を関連付けてもその関連付けた写像はどっちの結論にも行きつく訳ないから居場所ないじゃん」とかあるいは「それら要素を点に見立てて型を空間に見立てたら空間が関係ないもの同士の点同士の間の線がどっちかの空間に入ってる訳ないじゃん」とか直感的にはそういう意味合いになるのだと解釈したよたぶんこの画像のような感じではなかろうか（きたねー手書きで申し訳ないが）

…No.115452+うーん難しいな モーダスポネンスと関数適用が何故似てるか？って話の理屈がそうなってるって話かな？それとも >No.115424 の集合、集合の集合、集合の集合の集合、…って階層が型には備わってるって話の方か？

…No.115453+>モーダスポネンスと関数適用が何故似てるか？って話の理屈がそうなってるって話かな？ こっちに近い話かな 「要素aが集合Aに所属する&要素bが集合Bに所属するとき それらの間の写像はAにもBにも所属してない これは論理式でも点でも同じである この「違う集合同士の要素同士の写像はどちらの集合にも所属していない」ことを強調すると 「違う型同士の要素同士の写像はどちらの型でも扱えない」ということと要は同じ意味なので つまりやはり型とは集合のことなのでは？」ということを言いたい図だった

…No.115454+>集合、集合の集合、集合の集合の集合、…って階層が型には備わってるって話の方か？ こっちはさっきの図では描けなかったが 型Aの部分集合として下位階層の型Sを考えて Sの中の要素a'を想定したら当然それは型Aの要素でもあるので aとa'の写像は型Aの中で問題なく扱えるし前述の通り型Aの外にまたぐと扱えなくなる これならやはりさっき言った通り「型=集合」という認識でよさそう （集合の集合云々だから「大きくなる」と思いきや 部分集合云々の「小さくなる」話になっているのは自分でも引っかかるが）

…No.115455+階層があるって話はx∈xみたいなのを避けるために (x : A) ∈ (y : B), (BはAより上位の型) みたいな感じで両辺違う型にしようっていう話だったと思う 部分集合とはまたちょっと違う気がする

…No.115457+https://proc-cpuinfo.fixstars.com/2017/05/division-operation-optimization/ グロタンディーク構成 と 負の数の補数表現 と ディラックの海

…No.115458+グロタンディーク構成って要素の圏の一般的な奴らしいけど型と何か関係あるの？

…No.115470+５時から男

…No.115471+古めかしいが単純明快で懇切丁寧な論理学の教科書である 前原昭二『記号論理入門』の第8章§1を読んでいたら >∀Fとか∃Fのような<述語に関する限定作用素>をも合わせ考える論理を2階の述語論理といいます。 ><述語の述語>に関する限定作用素を許す3階の述語論理というように、高階の述語論理-あるいは型の理論ともよばれる-というものを一般に考えることもできます。 ってあったのよ この本の第1版は1967年10月15日なんで 当時「高階の述語論理≒型理論」という認識があったということが読み取れる またこの本では第1章§5で述語と性質と概念と条件と命題関数と（内包で書ける）集合を同一視するので つまりは型＝述語の述語＝（内包で書ける）集合のさらなる（内包で書ける）集合であると考えられる これだと今までの議論と整合的な見解でもある

…No.115476+歴史的にはラッセルが集合論のパラドクスを回避するために導入したのが型(タイプ)だけど、ラッセル(とホワイトヘッド)はさらに意味論的パラドクスというのを回避するために階(オーダー)というのも導入した。 でもこれらは定義によっては同じになるので前原先生なんかは同一視して教科書を書きがち。 命題と型を同一視するのは、自然演繹の証明と型付けの導出体系が同型になるからというだけでなく、命題の意味をその証明の集まりと同一視する(BHK解釈)と型っぽくなるという背景もある。 プログラムの表示的意味論というのを与えるとプログラムの型を数学的な集合と対応づけられるようになるよ。

…No.115757+>歴史的にはラッセルが集合論のパラドクスを回避するために導入したのが型(タイプ)だけど、ラッセル(とホワイトヘッド)はさらに意味論的パラドクスというのを回避するために階(オーダー)というのも導入した。 >でもこれらは定義によっては同じになるので前原先生なんかは同一視して教科書を書きがち。 今気づいたけど別物なんですか！　混同してた…

…No.116049そうだねx1PM（プリンキピア・マテマティカ）では上でいわれてるように別概念として型と階を導入したけど，同時代のゲーデルらによってより簡便に再定義される．そちらは型と階を実質区別しなくていい． 一応，ゲーデルの定義でも階は論理式の階層のような概念なので型とは違うけれど，内包公理と同様の原理によって集合の一種である型と論理式の性質である階を対応付けている． >型ってなに？ ほぼ集合論で言うところのクラス（類）と同じ． でもラッセルのパラドクスのようなものを文法的に排除するために，対象の帰属関係の階層（順序）のようなものを付与して，ひとつ上の階層からの帰属にしか文法的に言及できないように制限した理論を作った． そういう構造付きクラスのことを，あるいはそのクラスに割り振られた階層を見分けるラベルのことを型とよんだ． 階はゲーデル的な型に対応した定義なのか，量化の強さで定義するのかなどでも若干導入が違うし，orderとsortedの用語が歴史的にルーズに使われている． これについては，2階述語論理の標準解釈と非標準解釈やこれに伴うヘンキンの仕事に，そのあたりのモヤモヤを晴らす糸口がある．