Да, дело-то именно в том, к какому нужнику мы идем. И, stretching the metaphor, лучше, по-моему, индивидуальный нужник в каждом огороде, чем один трехэтажный нужник сияющего мрамора на деревню, до которого от моей халупы четыре версты продираться по полям, поросшими дикими функторами.
То есть, о чем я говорю. Есть модель комбинаторной логики, лично мне она неинтересна по призванию, но может быть интересна другим людям, что само по себе весьма прельстиво. Но зачем *в этой модели* доказывать давно известные факты этой самой комбинаторной логики?! Если показать, что наша конструкция - это именно модель КЛ, то все факты КЛ в ней верны автоматически, из замшелых манускриптов. То есть, после Definition 1 должно идти не Functional Completeness, а доказательство того, что TCA моделирует КЛ и т. д., откуда все остальное вытекает само собою. Модульность же!
И вот именно этого я и не понимаю. Опять-таки, то что я не понимаю, какой тут профит, не значит, что его нет, - именно поэтому я и задал вопрос выше.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2015-05-19 04:42 pm (UTC)То есть, о чем я говорю. Есть модель комбинаторной логики, лично мне она неинтересна по призванию, но может быть интересна другим людям, что само по себе весьма прельстиво. Но зачем *в этой модели* доказывать давно известные факты этой самой комбинаторной логики?! Если показать, что наша конструкция - это именно модель КЛ, то все факты КЛ в ней верны автоматически, из замшелых манускриптов. То есть, после Definition 1 должно идти не Functional Completeness, а доказательство того, что TCA моделирует КЛ и т. д., откуда все остальное вытекает само собою. Модульность же!
И вот именно этого я и не понимаю. Опять-таки, то что я не понимаю, какой тут профит, не значит, что его нет, - именно поэтому я и задал вопрос выше.