• Ubuntu 14.04 LTS (Trusty Tahr) доступна для скачивания!
    0
    Сейчас в 13.10 настроил так при помощи xkb, но одна раскладка работает для всех окон, это не удобно.
    Вообще, есть утилитки, которые могут сделать каждому приложению свою раскладку. Если правильно припоминаю, то сам когда-то пользовался вот этой вместе с xkb, когда xfce'шный индикатор и xxkb не понравились.
  • Как первокурсник определение Коши сократил
    0
    А почему тогда не писать «ε ∈ C ∧ (ε ∈ R ∧ ε > 0)»? Это тоже равносильно «ε ∈ R+».
    Понятия не имею. Лично я бы так не писал, потому что это потребовало бы расширения множества аксиом комплексными числами, что, наверное, совершенно не обязательно.
    Почему вместо «ε ∈ R+» должны писать «ε ∈ R ∧ ε > 0»; но при этом не пишем «m ∈ Z ∧ m > 0» вместо «m ∈ N»?
    Вы не обязаны писать «ε ∈ R ∧ ε > 0»; вы можете писать «m ∈ Z ∧ m > 0» вместо «m ∈ N». На всякий случай уточню, что я ни разу не знаток теории множеств и просто пытаюсь разобраться, а вовсе не спорю ожесточенно, если что, и не против прикоснуться к мудрости знатоков.
    Так я её так и развернул. Неинтуитивность неразвёрнутых bounded quantifiers проявляется, например, при построении отрицания.
    С неинтуитивностью отрицания ограниченных кванторов я не спорю. Я не понял, почему не надо класть положительность эпсилон в импликацию слева под квантором и почему утверждение про связанную переменную «внешнее», только и всего.
  • Как первокурсник определение Коши сократил
    0
    Знали бы вы, как выглядит ваша последняя фраза, у которого уровень знания математики на уровне 11 класс+.
    Мне не стыдно признать свою математическую безграмотность, если что, хотя я бы предпочел замечание по существу. Лично мне, да, непонятно, как с точки зрения логики можно что-то написать на стороне про связанную в формуле переменную.
  • Как первокурсник определение Коши сократил
    0
    Схема выделения тут, очевидно, ни при чём — тут даже нет «переменных-множеств».
    Вам нужны типы, чтобы" более строго" записывать ε ∈ R+, при том что это утверждение по схеме выделения равносильно ε ∈ R ∧ ε > 0. Собственно, послание было в том, что схема выделения для всех мыслимых (мной — как профан могу что-то упускать) применений квантификации по множеству обходит ограничение о неупоминании квантифицируемой переменной в терме-множестве.
    Речь идёт о том, как от матанистических «ограниченных кванторов» (на которые даже отрицания трудно навешивать) перейти к формуле с обычными логическими кванторами; это ортогонально теориям множеств.
    Интересно, каким языком вы будете определять квантификацию по множеству, если не языком теории множеств (естественно, не обязательно ZF). Вообще, не понимаю, что может быть неинтуитивного в разворачивании всеобщности в импликацию и существования — в конъюнкцию; одновременно, легальность оговаривания чего-то на стороне в окрестностях формулы непонятна мне.
  • Как первокурсник определение Коши сократил
    0
    В этом случае, если мы перепишем более строго «ε ∈ R+», то здесь «∈» понимается как в некотором смысле тип («ε: R+»).
    Вроде как схема выделения в ZF вам дана аксиоматикой — тут снова нет никакой магии.
  • Как первокурсник определение Коши сократил
    0
    ε > 0 — не надо выносить в левую часть импликации, потому что эта «область определения» не содержит вхождений других переменных, она «внешняя» по отношению к формуле.
    Квантификация по множеству разворачивается в культурный теоретико-множественный язык без всякой магии, то бишь в:
    ∀ε (ε ∈ R ∧ ε > 0 → ...)
  • Как первокурсник определение Коши сократил
    +1
    Стремление к истине похвально — продолжайте в том же духе, — но с моралью я не согласен. В ситуации, когда у вас толковый преподаватель, он бы понял, что эта формулировка равносильна, но попросил бы вас это обосновать просто чтобы убедиться, что вы не написали ответ наугад. С натяжкой победа получается.

    А еще советую не стесняться тривиальности утверждения и не брезговать пользоваться словами и даже разными буквами для разных связанных переменных — всем же лучше, когда доказательства лучше читаются.
  • Мартин Грасслин: Фанбои и тролли в сообществе СПО
    0
    Малейшее упоминание Wayland в плохом ключе — и все, автора уже называют фанбоем «иксов», Mir и вообще троллем. Что вы и делаете. Может лучше не ярлыками разбрасываться, а по существу обсуждение вести?
  • Парадокс доказательства
    0
    Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же.
    Это действительно не одно и то же, поскольку теории типов изоморфны исчислениям (изоморфизм Карри-Говарда), а не теории множеств. Впрочем, что происходит в исчислении (индуктивных) конструкций под капотом в Coq, я слабо представляю, так что разъяснение знатока не повредило бы.
  • Три задачи для программистов, которым не нужна математика
    +3
    Теорию графов не читают в курсе мат. анализа. Теорию графов читают в курсах дискретной математики (вещи, очень отвязанной и от математики, и от прикладного программирования) и в курсах алгоритмов.
    В общем-то, теорию графов могут вообще не изучать, так же как на другой специальности могут не учить численные методы решения уравнений матфизики. Это не делает, кстати, ни тот, ни другой курс отвязанным от математики.
  • Школьник об олимпиадном программировании
    +5
    Я учавствовал в Киеве, и даже занял 1-е место на уровне города (дальше не пустили по возрасту), но сейчас понимаю что ничего не решает.
    С незапамятных времен на олимпиадах не запрещено соревноваться со старшими классами, к тому же, в олимпиадах по информатике это (вроде как) можно делать постфактум, ибо задания одни и те же для всех. Что же у вас не стряслось?
    Давайте подумаем, чему нас учат задачки с Codeforces или TopCoder. Они «учат мыслить» и «писать правильный код» скажут нам труъ олимпиадники.
    Я б с удовольствием почитал бы отзыв на подобии такого, но пока что вынужден констатировать, что вы оспариваете утверждения, которые сами же и сформулировали.

    P.S. Вот чего я не могу понять, так это почему столь много людей стремятся обосновать ненужность или даже вредность олимпиад по информатике. А главное, зачем? Этим занимаются, потому что нравится, а не для легкого поступления в вуз, подготовки к собеседованию в Google или бесплатных брендированых футболок.
  • Вышел GNOME 3.8
    +2
    На видео может быть нагляднее. Имхо, как раз уведомления похожи в лучшем случае настройками, насколько могу судить по скринам третьегнома.
  • У iPhone больше уязвимостей, чем у Android, BlackBerry и Windows Phone вместе взятых
    0
    Все. Только тут желания с возможностями не совпадают. :-)
  • Частые ошибки при разработке lockfree-алгоритмов и их решения
    0
    Возможно, уместно запостить немного state of the art: комбинация техник separation logic и rely-guarantee, носящая имя RGsep, была специально заточена, чтобы сделать формальные доказательства memory safety и linearisability неблокирующих алгоритмов подъемными. В частности, если интересна теория, то по ссылке вроде как есть примеры с неблокирующим стеком, разными реализациями списков. Насколько хороша утилита, делающая это автоматически, пока не интересовался.
  • У iPhone больше уязвимостей, чем у Android, BlackBerry и Windows Phone вместе взятых
    –3
    Интересная статистика, но ведь она ничего не говорит о количестве уязвимостей, которые еще не обнаружены и могут быть использованы против пользователя, а значит пригодна только для экстраполяции, да?
  • Русский стал вторым по популярности языком Интернета
    +1
    А какой язык вы бы хотели видеть более популярным?
  • Сказ о том, как один нерадивый провинциал в MIT поступал
    0
    А много ли в ЕС англоязычных бакалавратов в принципе? У меня сложилось впечатление, что это большая редкость.
  • Магистратура в Техническом Университете Мюнхена
    0
    Другое дело, что даже эти самые лучшие университеты — середнячки по мировым меркам.
    А в чем именно TUM не блещет по мировым меркам?
  • Шумиха вокруг скорейшего краха Nokia не обоснована или о чем же недоговаривают аналитики?
    0
    Samsung запросто забила бы Nokia и ценой, и количеством. Собственно именно такую картину мы сейчас наблюдаем на рынке Android смартфонов, некогда лидеры рынка Sony и HTC терпят большие убытки и занимают мизерную долю.
    Разве сейчас модельный ряд Samsung дешевле или разнообразнее конкурентов?
  • Впечатление по работе Google Chrome OS на Acer C7 Chromebook
    0
    есть прекрасный сервис, который умеет компилировать 40 языков программирования
    Подозреваю, что речь идет об ideone.com.
  • Комментарий из публикации, перенесённой в черновики.
  • 4 принципа UX, про которые забыла Microsoft в Windows 8
    0
    А чем надо мотивировать переход на новые версии Windows (если фичи виртуализации не принципиальны)? Интересны случаи ХР => 7, XP => 8 и 7 => 8.
  • 4 принципа UX, про которые забыла Microsoft в Windows 8
    +1
    Где вы тут осуждение увидели? На лицо недостаток мотивации для покупки новой версии ОС (после чего уже могло бы и осуждение возникнуть :) ). Не все любят обновляться ради обновлений.
  • Google закрыл Карты для пользователей Windows Phone
    +1
    Насчет офиса — хороший пример.
    Было бы очень поучительно, если б Google именно этим примером в отношении MS и вдохновился.
  • Столлман назвал Ubuntu «шпионским»
    +4
    Мне кажется, что плохое здесь то, что у вас нет никаких инструментов контроля за своими личными данными. Без вашего ведома компания может как делать свой продукт лучше на основе вашей информации, так и продавать ее Министерству Любви вашего государства.
  • В энергопотреблении грядут изменения: ученые из MIT уменьшат его на половину
    +1
    К счастью, возможности «голосовать рублем» производители нас, потребителей, не лишат.
  • Комментарий из публикации, перенесённой в черновики.
  • Открыт сбор заявок на участие в бета-тестировании Steam для Linux
    +1
    сейчас установить Wine не удаётся
    Комментарии к багрепорту не читал, но осуждаю могу заметить, что летом очень даже пользовался wine на amd64. Если поломаны зависимости, может быстрее будет попробывать их самому разгрести и удалить старые пакеты, мешающие wine?
  • Обучение наоборот
    0
    Кому нужна теория — тот её быстрее освоит имея практические навыки.
    Имхо, конечно, но этот подход никак не запрещает изучать исключительно теоритические предметы при наличии хороших методических материалов (книга, преподавательский конспект лекций, и т.д.). Наоборот, это позволяет сосредоточиться на тех вещах, доказательство которых нетривиально и непонятно, а не на огромной куче определений и простых вещей, которые всегда есть в каждом курсе. К тому же, это практически не отличается от того, как это реально работает и сейчас: так или иначе, свой собственный конспект перед коллоквиумом надо разобрать и осознать самостоятельно. Разница лишь в том, по чьим материалам будешь готовиться и когда задашь интересующие вопросы: до или после колоквиума.
  • Демонстрация сбоев программы при отсутствии барьеров памяти
    0
    Как я понимаю, проверить любой код на отсутствие таких лаж невозможно.
    Это технически возможно, просто до поры до времени это не очень волновало даже самих производителей процессоров, но последние несколько лет ситация поменялась. Сейчас есть исследовательская группа в Кембридже (и сочувствующие в INRIA и прочих учреждениях), которая формализировала модели памяти SPARC, x86 и Power (раз и два). Есть люди, интересующиеся формальной верификацией поверх слабых моделей памяти (например, C++).
  • Демонстрация сбоев программы при отсутствии барьеров памяти
    +2
    > Вы ничего не перепутали? ARM и PowerPC — совершенно разные архитектуры.
    В контексте данной статьи автор мог смело писать их в одном предложении: модели памяти этих архитектур близнецы-братья.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    Могу согласиться с вами лишь частично: глюки и тормоза вылезают только там, куда прикладывает свою програмистскую руку Canonical. :-) Другими словами, если не пользоваться Unity, то Ubuntu в целом получается таким себе удобным debian testing (а это очень стабильно и здорово).
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    +1
    > переключателя полноэкранности не предусмотрено
    На самом деле, когда вы находитель в dash, кнопки закрыть/развернуть/свернуть в левом верхнем углу управляют именно им. Другими словами, есть там разворачивание меню на весь экран.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    Если не секрет, как ставили? Из jockey?
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    > панель не показывается обратно, если настроить автоскрытие
    Очень похоже на баг Unity времен до 12.04. Собственно, из-за кривых рук разработчиков этого бага, ЕМНИП, вырезали режим «умного скрытия» панели, когда она не показывается только при перекрытии каким-то окном.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    +1
    > Но в основную версию их включать не планировали (гениальное решение).
    Вообще-то, планировали и даже писали об этом в рассылке. Не знаю, все ли получилось, впрочем, ибо интересовался только lvm.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    IconTasks (ранее были другие плазмоиды, вдохновленные виндовым superbar) стремится поддерживать фичи Unity, так что тут однозначное да.

    > Мне ни KDE, ни xfce категорически не понравились: первая для инопланетян, во второй я как раз таки нужного функционала в панели и не нашёл.
    Привет вам, землянин! :)
    В XFCE это в настройках апплета таскбара (не панели), в которых довольно трудно заблудиться.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    Хотел же сразу дописать, что везде, кроме KDE (и, судя по вашей просьбе, Unity) два трея сделать проблематично. :-)
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    +1
    Извините, по памяти точно не подскажу (все-таки в ccsm черт ногу сломит) — компиза у меня сейчас нет. Раньше соответствующий плагин назывался как-то вроде «Session management», кажется.
  • Ubuntu 12.10 Quantal Quetzal (Квантовый Кетцаль/Квезаль)
    0
    > Там нет апплета, который был в старом гноме — dockbarx.
    И что этот апплет делал? Если речь о таскбаре без названий приложений, то в KDE IconTasks даже включили в стандартную поставку плазмоидов, а xfce’шная панель и сама по себе это умела всегда.