История изменений

Ты что-то не так запомнил.

Скотт сам первый (с точки зрения построения модели, так-то есть теорема Чёрча-Розера) и доказал непротиворечивость нетипизированного лямбда-исчисления. Более ранние результаты Клини и Розера говорят о противоречивости нетипизированного варианта как логической системы — функтора из категории ULC в логически «хорошую» категорию нет, но как теория ULC непротиворечива — равенства различимы как теоремы и у теории есть модель в которых они реализуются.

Типизированные варианты тем более непротиворечивы, уже в т.ч. и логически — функтор есть, известен как изоморфизм Карри-Говарда.

http://en.wikipedia.org/wiki/Lambda_calculus#Lambda_calculus_in_history_of_ma...

http://plato.stanford.edu/entries/lambda-calculus/#ConLCal

http://plato.stanford.edu/entries/lambda-calculus/#SemLCal

http://arxiv.org/abs/0904.4756

http://mathoverflow.net/q/16752

http://turing100.acm.org/lambda_calculus_timeline.pdf

http://en.wikipedia.org/wiki/Model_theory#Using_the_compactness_and_completen...

http://en.wikipedia.org/wiki/Curry–Howard_correspondence

Ты что-то не так запомнил.

Скотт сам первый и доказал непротиворечивость нетипизированного лямбда-исчисления. Более ранние результаты Клини и Розера говорят о противоречивости нетипизированного варианта как логической системы — функтора из категории ULC в логически «хорошую» категорию нет, но как теория ULC непротиворечива — равенства различимы как теоремы и у теории есть модель в которых они реализуются.

Типизированные варианты тем более непротиворечивы, уже в т.ч. и логически — функтор есть, известен как изоморфизм Карри-Говарда.

http://en.wikipedia.org/wiki/Lambda_calculus#Lambda_calculus_in_history_of_ma...

http://plato.stanford.edu/entries/lambda-calculus/#ConLCal

http://plato.stanford.edu/entries/lambda-calculus/#SemLCal

http://arxiv.org/abs/0904.4756

http://mathoverflow.net/q/16752

http://turing100.acm.org/lambda_calculus_timeline.pdf

http://en.wikipedia.org/wiki/Model_theory#Using_the_compactness_and_completen...

http://en.wikipedia.org/wiki/Curry–Howard_correspondence