Type inhabitation problem
- Type inhabitation problem
In simply typed lambda calculus, the type inhabitation problem is the following problem: given a type , does there exist a -term M such that for some type environment ? If the answer is positive, M is said to be an inhabitant of .
Since types in simply typed lambda calculus correspond to formulae of minimal implicative logic (see Curry-Howard isomorphism), a type has an inhabitant if and only if it is a tautology of minimal implicative logic.
Richard Statman proved that the type inhabitation problem is PSPACE-complete.
Wikimedia Foundation.
2010.
Look at other dictionaries:
Curry–Howard correspondence — A proof written as a functional program: the proof of commutativity of addition on natural numbers in the proof assistant Coq. nat ind stands for mathematical induction, eq ind for substitution of equals and f equal for taking the same function… … Wikipedia
List of mathematics articles (T) — NOTOC T T duality T group T group (mathematics) T integration T norm T norm fuzzy logics T schema T square (fractal) T symmetry T table T theory T.C. Mits T1 space Table of bases Table of Clebsch Gordan coefficients Table of divisors Table of Lie … Wikipedia
List of PSPACE-complete problems — Here are some of the more commonly known problems that are PSPACE complete when expressed as decision problems. This list is in no way comprehensive. Games and puzzles Generalized versions of: Amazons· Atomix· Geography· Gomoku· Hex· Reversi·… … Wikipedia
Richard Statman — Infobox Scientist image width = 150px name = Richard Statman box width = birth date = Sept 6, 1946 birth place = death date = death place = residence = citizenship = nationality = ethnicity = field = computer science work institutions = Carnegie… … Wikipedia
Anthropology and Archaeology — ▪ 2009 Introduction Anthropology Among the key developments in 2008 in the field of physical anthropology was the discovery by a large interdisciplinary team of Spanish and American scientists in northern Spain of a partial mandible (lower… … Universalium
Afterlife — For other uses, see Afterlife (disambiguation). After death , Life after death , and Hereafter redirect here. For other uses, see After death (disambiguation), Life after death (disambiguation), and Hereafter (disambiguation). Ancient Egyptian… … Wikipedia
Sangaria, India — Infobox Indian Jurisdiction native name = Sangaria | type = city | latd = 29.48| longd = 74.27 state name = Rajasthan district = Hanumangarh leader title = leader name = altitude = population as of = 2001 population total = 34,541| population… … Wikipedia
North American river otter — Conservation status Least Concern … Wikipedia
Sudan, The — officially Republic of the Sudan Country, North Africa. Area: 966,757 sq mi (2,503,890 sq km). Population (2002 est.): 37,090,000. Capital: Khartoum. Muslim Arab ethnic groups live in the northern and central two thirds of the country, while… … Universalium
Origin of the Romanians — History of Romania This article is part of a series Prehistory … Wikipedia
