住性 (型理論)とは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > 百科事典 > 住性 (型理論)の意味・解説 

住性 (型理論)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2025/07/03 03:52 UTC 版)

型理論において 、型住性問題(type inhabitation problem)とは、型型環境が与えられたとき、 を満足する項tが存在するか否かの判定問題である。そのような項tが存在するとき、項tは 型の住人であるといい、 型は有項であるという。


論理との関係

単純型付きラムダ計算においては、型が有項であることとminimal implicative logicにおいてその型と対応する命題が恒真であることは同値である。同様に、System F の型が有項であることと二階述語論理においてその型と対応する命題が恒真であることは同値である。

Formal properties

多くの計算体系において、型住性問題は大変困難である。単純型付きラムダ計算においては型住性問題はPSPACE完全であることが Richard Statmanにより示されている。System Fにおいては決定不能である。

参考文献




英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  
  •  住性 (型理論)のページへのリンク

辞書ショートカット

すべての辞書の索引

「住性 (型理論)」の関連用語

1
住性 (型理論) 百科事典
16% |||||

住性 (型理論)のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



住性 (型理論)のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの住性 (型理論) (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。

©2025 GRAS Group, Inc.RSS