Сейчас в 13.10 настроил так при помощи xkb, но одна раскладка работает для всех окон, это не удобно.
Вообще, есть утилитки, которые могут сделать каждому приложению свою раскладку. Если правильно припоминаю, то сам когда-то пользовался вот этой вместе с xkb, когда xfce'шный индикатор и xxkb не понравились.
А почему тогда не писать «ε ∈ C ∧ (ε ∈ R ∧ ε > 0)»? Это тоже равносильно «ε ∈ R+».
Понятия не имею. Лично я бы так не писал, потому что это потребовало бы расширения множества аксиом комплексными числами, что, наверное, совершенно не обязательно.
Почему вместо «ε ∈ R+» должны писать «ε ∈ R ∧ ε > 0»; но при этом не пишем «m ∈ Z ∧ m > 0» вместо «m ∈ N»?
Вы не обязаны писать «ε ∈ R ∧ ε > 0»; вы можете писать «m ∈ Z ∧ m > 0» вместо «m ∈ N». На всякий случай уточню, что я ни разу не знаток теории множеств и просто пытаюсь разобраться, а вовсе не спорю ожесточенно, если что, и не против прикоснуться к мудрости знатоков.
Так я её так и развернул. Неинтуитивность неразвёрнутых bounded quantifiers проявляется, например, при построении отрицания.
С неинтуитивностью отрицания ограниченных кванторов я не спорю. Я не понял, почему не надо класть положительность эпсилон в импликацию слева под квантором и почему утверждение про связанную переменную «внешнее», только и всего.
Знали бы вы, как выглядит ваша последняя фраза, у которого уровень знания математики на уровне 11 класс+.
Мне не стыдно признать свою математическую безграмотность, если что, хотя я бы предпочел замечание по существу. Лично мне, да, непонятно, как с точки зрения логики можно что-то написать на стороне про связанную в формуле переменную.
Схема выделения тут, очевидно, ни при чём — тут даже нет «переменных-множеств».
Вам нужны типы, чтобы" более строго" записывать ε ∈ R+, при том что это утверждение по схеме выделения равносильно ε ∈ R ∧ ε > 0. Собственно, послание было в том, что схема выделения для всех мыслимых (мной — как профан могу что-то упускать) применений квантификации по множеству обходит ограничение о неупоминании квантифицируемой переменной в терме-множестве.
Речь идёт о том, как от матанистических «ограниченных кванторов» (на которые даже отрицания трудно навешивать) перейти к формуле с обычными логическими кванторами; это ортогонально теориям множеств.
Интересно, каким языком вы будете определять квантификацию по множеству, если не языком теории множеств (естественно, не обязательно ZF). Вообще, не понимаю, что может быть неинтуитивного в разворачивании всеобщности в импликацию и существования — в конъюнкцию; одновременно, легальность оговаривания чего-то на стороне в окрестностях формулы непонятна мне.
ε > 0 — не надо выносить в левую часть импликации, потому что эта «область определения» не содержит вхождений других переменных, она «внешняя» по отношению к формуле.
Квантификация по множеству разворачивается в культурный теоретико-множественный язык без всякой магии, то бишь в:
∀ε (ε ∈ R ∧ ε > 0 → ...)
Стремление к истине похвально — продолжайте в том же духе, — но с моралью я не согласен. В ситуации, когда у вас толковый преподаватель, он бы понял, что эта формулировка равносильна, но попросил бы вас это обосновать просто чтобы убедиться, что вы не написали ответ наугад. С натяжкой победа получается.
А еще советую не стесняться тривиальности утверждения и не брезговать пользоваться словами и даже разными буквами для разных связанных переменных — всем же лучше, когда доказательства лучше читаются.
Насколько я понимаю, находясь в путешествии в различных странах не слишком подолгу, он, по сути, не является резидентом ни одной страны мира.
Сам я совершенно не в теме всех этих формальностей, но в моем понимании визы с правом на работу и контракт или договор подряда, который вы заключаете с работадателем, должны бы требовать, чтоб вы были налоговым резидентом. Однако, это все явно не случай описанного в посте, а даже если бы речь шла о стихийной работе, то вообще говоря образ жизни автора позволяет предположить о непревышенном необлагаемого налогами минимуме доходов, ежели такой имеется в посещенных автором странах.
P.S. Интересно, до каких еще подробностей будней автора можно спуститься, чтобы навязать другим свои взгляды на жизнь. :-)
Извините, но я не могу подобрать другого слова, когда видеоплейер начинает заикаться, если одновременно с воспроизведением видео запустить какое-нибудь копирование из каталога в каталог на том же самом диске.
А разве для линуксоидов число 12309 уже потеряло смысл? Например, у меня полно аналогичных впечатлений при копировании гигабайтов файлов под Linux.
Малейшее упоминание Wayland в плохом ключе — и все, автора уже называют фанбоем «иксов», Mir и вообще троллем. Что вы и делаете. Может лучше не ярлыками разбрасываться, а по существу обсуждение вести?
Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же.
Это действительно не одно и то же, поскольку теории типов изоморфны исчислениям (изоморфизм Карри-Говарда), а не теории множеств. Впрочем, что происходит в исчислении (индуктивных) конструкций под капотом в Coq, я слабо представляю, так что разъяснение знатока не повредило бы.
Теорию графов не читают в курсе мат. анализа. Теорию графов читают в курсах дискретной математики (вещи, очень отвязанной и от математики, и от прикладного программирования) и в курсах алгоритмов.
В общем-то, теорию графов могут вообще не изучать, так же как на другой специальности могут не учить численные методы решения уравнений матфизики. Это не делает, кстати, ни тот, ни другой курс отвязанным от математики.
Но Windows Phone уже занял стабильное третье место и, судя по всему, не останавливается, конечно может и не так быстро как хотелось бы, но все же.
Как будто бы уверенное третье место среди десктопных ОС побудило Microsoft портировать много своих приложений на GNU/Linux. Спасибо, что Skype еще поддерживается.
P.S. Оценивать правоту корпораций — занятие сомнительное. Они же не за справедливость борются.
Я учавствовал в Киеве, и даже занял 1-е место на уровне города (дальше не пустили по возрасту), но сейчас понимаю что ничего не решает.
С незапамятных времен на олимпиадах не запрещено соревноваться со старшими классами, к тому же, в олимпиадах по информатике это (вроде как) можно делать постфактум, ибо задания одни и те же для всех. Что же у вас не стряслось?
Давайте подумаем, чему нас учат задачки с Codeforces или TopCoder. Они «учат мыслить» и «писать правильный код» скажут нам труъ олимпиадники.
Я б с удовольствием почитал бы отзыв на подобии такого, но пока что вынужден констатировать, что вы оспариваете утверждения, которые сами же и сформулировали.
P.S. Вот чего я не могу понять, так это почему столь много людей стремятся обосновать ненужность или даже вредность олимпиад по информатике. А главное, зачем? Этим занимаются, потому что нравится, а не для легкого поступления в вуз, подготовки к собеседованию в Google или бесплатных брендированых футболок.
Возможно, уместно запостить немного state of the art: комбинация техник separation logic и rely-guarantee, носящая имя RGsep, была специально заточена, чтобы сделать формальные доказательства memory safety и linearisability неблокирующих алгоритмов подъемными. В частности, если интересна теория, то по ссылке вроде как есть примеры с неблокирующим стеком, разными реализациями списков. Насколько хороша утилита, делающая это автоматически, пока не интересовался.
Интересная статистика, но ведь она ничего не говорит о количестве уязвимостей, которые еще не обнаружены и могут быть использованы против пользователя, а значит пригодна только для экстраполяции, да?
Вы не обязаны писать «ε ∈ R ∧ ε > 0»; вы можете писать «m ∈ Z ∧ m > 0» вместо «m ∈ N». На всякий случай уточню, что я ни разу не знаток теории множеств и просто пытаюсь разобраться, а вовсе не спорю ожесточенно, если что, и не против прикоснуться к мудрости знатоков.
С неинтуитивностью отрицания ограниченных кванторов я не спорю. Я не понял, почему не надо класть положительность эпсилон в импликацию слева под квантором и почему утверждение про связанную переменную «внешнее», только и всего.
Интересно, каким языком вы будете определять квантификацию по множеству, если не языком теории множеств (естественно, не обязательно ZF). Вообще, не понимаю, что может быть неинтуитивного в разворачивании всеобщности в импликацию и существования — в конъюнкцию; одновременно, легальность оговаривания чего-то на стороне в окрестностях формулы непонятна мне.
∀ε (ε ∈ R ∧ ε > 0 → ...)
А еще советую не стесняться тривиальности утверждения и не брезговать пользоваться словами и даже разными буквами для разных связанных переменных — всем же лучше, когда доказательства лучше читаются.
P.S. Интересно, до каких еще подробностей будней автора можно спуститься, чтобы навязать другим свои взгляды на жизнь. :-)
P.S. Оценивать правоту корпораций — занятие сомнительное. Они же не за справедливость борются.
Я б с удовольствием почитал бы отзыв на подобии такого, но пока что вынужден констатировать, что вы оспариваете утверждения, которые сами же и сформулировали.
P.S. Вот чего я не могу понять, так это почему столь много людей стремятся обосновать ненужность или даже вредность олимпиад по информатике. А главное, зачем? Этим занимаются, потому что нравится, а не для легкого поступления в вуз, подготовки к собеседованию в Google или бесплатных брендированых футболок.