13/08/04 10:09:51.11
>>76
URLﾘﾝｸ(researchmap.jp)
> 定義 2.13 型理論の言語 L^T は以下の要素を持つ
・・・
> * 任意の項τに対し、ある n が存在して項σが type n であり、項τが type n+1 を持つ時
> のみ論理式 σ∈τ は有意味な論理式となる。
x∪{x} = {y | y∈x or y∈{x}}
変数ｙのtypeは何になるかね？
13/08/04 10:09:51.11
>>76
URLﾘﾝｸ(researchmap.jp)
> 定義 2.13 型理論の言語 L^T は以下の要素を持つ
・・・
> * 任意の項τに対し、ある n が存在して項σが type n であり、項τが type n+1 を持つ時
> のみ論理式 σ∈τ は有意味な論理式となる。
x∪{x} = {y | y∈x or y∈{x}}
変数ｙのtypeは何になるかね？