2
Czy istnieje typowany rachunek lambda, który jest spójny i kompletny Turinga?
Czy istnieje typowany rachunek lambda, w którym odpowiednia logika w korespondencji Curry-Howarda jest spójna i gdzie istnieją możliwe do wpisania wyrażenia lambda dla każdej funkcji obliczeniowej? Jest to wprawdzie pytanie nieprecyzyjne, pozbawione precyzyjnej definicji „typowanego rachunku lambda”. Zastanawiam się, czy istnieją (a) znane przykłady tego, lub (b) znane dowody niemożności …