История изменений
Исправление Manhunt, (текущая версия) :
Ты забываешь, наверное, что LC ,был изначально вычислительным формализмом, он не имел отношения к реальным машинам.
Ну так он и есть формализм.
Автор упустил из виду, что нужен еще кто-то, кто будет производить подстановки.
Почему обязательно нужен? Технически нам ничто не мешает рассматривать системы аксиом, не имеющие сколько-нибудь похожих воплощений в физическом мире. Другое дело, что практического смысла в этом обычно очень мало, так что мы редко и мало этим занимаемся.
А что мешает изобрести того, кто будет сразу вычислять выражения?
Технически - ничто не мешает. Это будет другая система аксиом, в ней будут доказуемы другие теоремы. Вот только какая от этого польза?
Исходная версия Manhunt, :
Ты забываешь, наверное, что LC ,был изначально вычислительным формализмом, он не имел отношения к реальным машинам.
Ну так он и есть формализм.
Автор упустил из виду, что нужен еще кто-то, кто будет производить подстановки.
Почему обязательно должен? Технически нам ничто не мешает рассматривать системы аксиом, не имеющие сколько-нибудь похожих воплощений в физическом мире. Другое дело, что практического смысла в этом обычно очень мало, так что мы редко и мало этим занимаемся.
А что мешает изобрести того, кто будет сразу вычислять выражения?
Технически - ничто не мешает. Это будет другая система аксиом, в ней будут доказуемы другие теоремы. Вот только какая от этого польза?