Популярная реализация функции в _|_ - незавершающееся вычисление.
Осмыслять этот код стоит с т.з. логики. В булевой логике любое утверждение либо истинно, либо ложно, его можно просто заменить одной из этих двух констант. В конструктивной логике жизнь разнообразней. Есть разница между true и irrefutable. Утверждение истинно, когда у меня есть его конструктивное доказательство в виде конкретного объекта, программы. Пока такое доказательство не получено, утверждение не истинно, но и не ложно, оно просто еще не решено. Ложно оно тогда, когда у меня опять же есть конкретная программа, которая из предполагаемого док-ва этого утверждения производит _|_, виснет. Ложные утверждения - это типы плохих, негодных, виснущих программ. Наконец, irrefutable оно, когда его отрицание ложно. Т.е. у нас нет конструктивного доказательства данного утверждения, мы не называем его истинным, но у нас есть конструктивное доказательство, что предположение о его ложности ведет к абсурду, т.е. его отрицание ложно. В посте как раз такое.
В принципе, есть определенная процедура, позволяющая конвертировать классические доказательства в конструктивные, но не один в один, а ценой замены для некоторых утверждений истинности на бесспорность (так по русски irrefutable?). Если конкретнее, в импликациях перед следствиями появляются двойные отрицания.
no subject
Осмыслять этот код стоит с т.з. логики. В булевой логике любое утверждение либо истинно, либо ложно, его можно просто заменить одной из этих двух констант. В конструктивной логике жизнь разнообразней. Есть разница между true и irrefutable. Утверждение истинно, когда у меня есть его конструктивное доказательство в виде конкретного объекта, программы. Пока такое доказательство не получено, утверждение не истинно, но и не ложно, оно просто еще не решено. Ложно оно тогда, когда у меня опять же есть конкретная программа, которая из предполагаемого док-ва этого утверждения производит _|_, виснет. Ложные утверждения - это типы плохих, негодных, виснущих программ. Наконец, irrefutable оно, когда его отрицание ложно. Т.е. у нас нет конструктивного доказательства данного утверждения, мы не называем его истинным, но у нас есть конструктивное доказательство, что предположение о его ложности ведет к абсурду, т.е. его отрицание ложно. В посте как раз такое.
В принципе, есть определенная процедура, позволяющая конвертировать классические доказательства в конструктивные, но не один в один, а ценой замены для некоторых утверждений истинности на бесспорность (так по русски irrefutable?). Если конкретнее, в импликациях перед следствиями появляются двойные отрицания.