| dbo:abstract | - In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type and a typing environment , does there exist a -term M such that ? With an empty type environment, such an M is said to be an inhabitant of . (en)
- 型理論において 、型住性問題(type inhabitation problem)とは、型と型環境が与えられたとき、 を満足する項tが存在するか否かの判定問題である。そのような項tが存在するとき、項tは 型の住人であるといい、 型は有項であるという。 (ja)
- 在简单类型lambda演算中，类型居留（Type inhabitation）问题是如下问题：给定一个类型 ，是否存在一个 -项 M 使得对于某个类型环境 有 ？在空的类型环境中，如果回答是肯定的，则 M 被称为 的居留元（inhabitant）。 因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见 Curry-Howard 同构)，一个类型有一个居留元，当且仅当它是极小蕴涵逻辑的重言式。 证明了在简单类型λ演算中类型居留问题是 的。 (zh)
|
| dbo:wikiPageID | |
| dbo:wikiPageLength | - 1816 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID | |
| dbo:wikiPageWikiLink | |
| dbp:wikiPageUsesTemplate | |
| dcterms:subject | |
| rdfs:comment | - In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type and a typing environment , does there exist a -term M such that ? With an empty type environment, such an M is said to be an inhabitant of . (en)
- 型理論において 、型住性問題(type inhabitation problem)とは、型と型環境が与えられたとき、 を満足する項tが存在するか否かの判定問題である。そのような項tが存在するとき、項tは 型の住人であるといい、 型は有項であるという。 (ja)
- 在简单类型lambda演算中，类型居留（Type inhabitation）问题是如下问题：给定一个类型 ，是否存在一个 -项 M 使得对于某个类型环境 有 ？在空的类型环境中，如果回答是肯定的，则 M 被称为 的居留元（inhabitant）。 因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见 Curry-Howard 同构)，一个类型有一个居留元，当且仅当它是极小蕴涵逻辑的重言式。 证明了在简单类型λ演算中类型居留问题是 的。 (zh)
|
| rdfs:label | - 住性 (型理論) (ja)
- Type inhabitation (en)
- 类型居留问题 (zh)
|
| owl:sameAs | |
| prov:wasDerivedFrom | |
| foaf:isPrimaryTopicOf | |
| isdbo:wikiPageRedirects of | |
| isdbo:wikiPageWikiLink of | |
| isfoaf:primaryTopic of | |
