Язык диофантовых предикатов

В продолжение темы про характеризацию вычислимости через диофантовы уравнения, мне бы хотелось рассказать об одном интересном формальном языке. Идею этого языка наверняка возникала у множества разных людей, очень уж он естественнен становится, если знать о теореме Робинсон-Дэвиса-Путнама-Матиясевича, однако название впервые встречается в замечательной статье Hilbert's Tenth Problem is Unsolvable (Martin Davis, 1973). Кстати, эта статья это первое официальное и притом отлично написанное изложения RDPM-теоремы, там всё дельно объясняется, даются конкретные примеры, как выражаются диофантовыми уравнениями числа Фибоначчи, экспоненциальная функция, любые примитивно-рекурсивные и любые μ-рекурсивные функции.

Язык этот не содержит логических символов, символа равенства и кванторов: высказывания это просто многочлены P(x, a, b, c, ..) от произвольного числа переменных и выделенной переменной x, интерпретируемые как ∀x.∃a, b,..,c. P(x, a, b,.., c) = 0, где переменные принимают целые положительные значения, а квантор всеобщности понимается в слабом смысле “верность выражения сохраняется при наложении на x дополнительных ограничений диофентовыми уравнениями”.

Это очень сильный язык:
– любое перечислимое множество, любая вычислимая функция, любое вычислимое соотношение можно закодировать диофантовым уравнением;
– можно написать такой P, что P(x, a, b,.., c) тогда и только тогда, когда программа закодированная числом x завершается;
– то, что программа, выполняющая, скажем, cut-elimination, завершается для любого поданного на вход доказательства x в теории T эквивалентно высказыванию “T непротиворечива”.

Теперь детали.( Read more... )

Хочу машину с DCT-трансмиссией на базе Zeroshift-сцепления!

Я очень привык к велосипедному режиму переключения передач: есть два рычажка на руле: поднять передачу и опустить передачу. На автомобиле мне бы хотелось точно таких же двух рычажков, и чтобы для переключения передачи не нужно было отвлекаться: ни педаль сцепления нажимать, ни руку с руля уводить. И чтобы скорость переключалась очень быстро и без периода свободного пробега, когда чуть теряешь скорость из-за нажатого сцепления. При этом педаль сцепления я считаю нужной (иногда удобно чтобы машина просто свободно “покатилась”) и ручное управление скоростями тоже мне по-душе. Вот как я люблю чтобы в операционных системах была консоль и из неё всё можно было сделать, так мне по-душе, чтобы если трансмиссия была, то можно было ею управлять вручную.

Полагаясь на всё вышесказанное, наиболее удобная мне система — DCT: dual-clutch transmission. Идея такой системы состоит в том, что из коробки передач в сторону колёс выходит не один вал, а два. Чётные передачи выводятся на один вал, нечётные на другой. Т.к. переключение передач всегда происходит с чётной на нечётную
(кроме как в случае перехода на нейтралку, передачи должны переключаться последовательно), переключение всегда можно осуществлять просто перключением колёс с одного выходного вала на другой, а это можно делать моментально. Т.е. нажал я на руле рычажок “вниз” или “вверх”, на свободном валу передача переключилось, и сразу переключаем вал. Чтобы переключение происходило максимально быстро, свободный вал обычно всё время держат включенным на передаче более высокой, чем включенная. Таким образом переключение вверх происходит за считанные миллисекунды. Вниз чуть дольше, но всё-равно заметить это невозможно.

Сейчас в большинстве DCT-систем используются два фрикционных аппарата сцепления, но фрикционное сцепление это вообще штука такая.. Спорная. Диски изнашиваются и греются, подшипник сцепления изнашивается, устройство довольно тонкое, да и переключение получается чуть замедленное. В общем, гораздо более прогрессивный подход — сцепление системы Zeroshift, специально разработанное для DCT: http://youtu.be/HJHjiUheod8.
Оно состоит из двух шестерней на валу (на одну подаётся вращение с одной скоростью, на другую с другой, те самые два выхода DCT-коробки передач), а между шестерёнками устройство, осуществляющее их сцепление с валом. Это устройство может пребывать в трёх состояниях: свободное вращение (отжатое сцепление), сцеплена левая шестерёнка, сцеплена правая шестерёнка. При помощи управляющих колец на устройство можно подать три команды:
– немедленно снять сцепление
– в ближайший удобный момент перейти на правую шестерню
– в ближайший удобный момент перейти на левую шестерню

Удобные моменты наступают часто: каждую 1/6 полного вращения соответствующей шестерёнки. А передача происходит непрерывно, т.е. ни в какой момент вал не оказывается свободным, постоянно на него подаётся некоторый крутящий момент. Очень классная система, простая, предельно энергоэффективная и с очень большим ресурсом.

Но она создаёт новую проблему: без фрикционного сцепления нужно что-то делать с рывком при переключении передач, иначе будет жутко изнашиваться коробка. К счастью, эта проблема очень просто решается: между валом, выходящим из нашего аппарата сцепления, и валом, который уже подаёт крутящий момент на колёса, устанавливается дифференциал на вращательной пружине. Т.е. между валами допускается разница в скорости вращения, она будет скомпенсирована тем, что будет вращаться сам дифференциал. Однако по мере вращения дифференциала, будет накручиваться пружина и этому вращению противодействововать. Соответственно сразу после переключения передач, рывок будет смягчён за счёт накручивания этой пружины, а потом вся энергия, накопленная в пружине, очень быстро вернётся назад во ускорение вращения колёс, 99% этой энергии менее чем за секунду после переключения передач. Пружину можно считать гармонической, т.е. никакой лишней диссипации энергии, вся мощность на дорогу. Опять же пружину можно отъюстировать на большее или меньшее смягчение рывка, получая спортивный и семейный варианты трансмиссии.

В плане эффективности набора скорости, в плане плавности хода и в плане энергоэффективности Zeroshift-коробка заметно опережает вообще все другие виды трансмиссии, которые мне удалось найти. Хочу.