Category: наука

Category was added automatically. Read all entries about "наука".

иероглифы

coq + imperative algorithm proving

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.
Collapse )

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.




Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
Collapse )

По итогу -- впечатления смешанные.
трололо

MapM

Abstract:
В данной статье я расскажу вам про отображающие функции вида map, включающие в себя сайд-эффекты. Тем, кому известен хаскель, эти функции известны как mapM и подобные.
Далее, будет показано, что хаскель, будучи самым распространённым языком из тех, где используются монады (ну, кроме C#/linq и Scala), является непрактичным из-за отсутствия сайд-эффектов. Раньше мне без сайд-эффектов было всего лишь просто неудобно использовать хаскель (требовалось городить лишний код), теперь же я понимаю, что есть некоторые вещи, где с чистотой не получится клёво использовать монады в одном из их применений.
Также будет показано, что тайпклассы -- это не гибко, потому что у одного тайпкласса и у одной функции (например, "функция sequence в монаде IO") может быть только одна реализация, и будет показано, где именно это не гибко.

Collapse )

Кроме того, видел сегодня клёвую статью Modules Matter Most. Она тут упомянута потому, что в ней тоже необоснованно гонят на хаскель, но сама статья хорошая и правильная.

Как показал наш спектральный анализ...

Встала задачка определения частоты звука. Точнее, две задачи. На входе — дискретизированный звук a0+∑ansin(nωt+φn) (n ∈ N, n ≥ 1), слегка приправленный белым шумом.

Первая задача: приблизительно определить основную частоту. Про преобразование Фурье знаю, но у меня случай сильно проще, и для него требуется всего лишь вычислять Σ|x[0] - x[0-k]| (с затуханием), основная частота определяется по первому минимуму суммы. (недостаток — необходимость игнорировать первый минимум для малых k, когда сигнал совпадает или почти совпадает сам с собой.) На практике для частоты дискретизации 44100Гц хватает k≤221 для быстрого определения частот от 200Гц и выше.

Для простых случаев это лучше, чем тащить библиотеку, реализующую FFT. Однако, если не будет хватать, то возьму fftw.

Вторая задача: имея приближенную частоту, определить частоту с большей точностью. Тут Фурье неприменим: нужна точность ±0.5Гц, что означает необходимость иметь 2 секунды собранных данных. Частота у меня иногда меняется, а нужно фиксировать частоту максимум через 0.5с после её установления (а лучше — 0.2с) и с хорошей точностью. Так как сигнал имеет гораздо более простой вид, нежели "полный спектр", то и тут должен быть подходящий мне метод.

Создаём 2..6 "сумматоров" вида S(ω) = ∑x[0]·(cos(ωt) + i·sin(ωt)) (тоже с затуханием), равномерно распределенных около приблизительно известной частоты так, чтобы отношение их частот было постоянным. Далее, на каждый цикл (когда ωt переходит границу 2πn) определяем аргумент комплексной суммы S(ω), вычитаем из неё аргумент, определенный на предыдущем переходе, получая d(ω). Если сигнал был чистый и частота недалеко от ω, то сдвиг фазы будет небольшим. В идеальном случае (интегрирование вместо суммирования, отсутствие шума, отсутствие гармоник, отсутствие дискретизации) сдвиг был бы постоянным и был бы связан с реальной частотой сигнала нехитрым выражением (если не ошибаюсь, этим: ωреальная = ω · (1 + d(ω)/π) для сдвига на частоте ω, равного d(ω) радиан на каждый цикл).

Проверял на чистом звуке флейты, с помощью указанной формулы определял частоту. ν≈280Гц, 4 "сумматора", отстоящих друг от друга примерно на 3Гц. Получившиеся частоты лежат очень близко друг к другу, отклонение ±0.05Гц от среднего, и это всего на трёх "переходах" ωt через 2πn, что соответствует 0.01с звучания.

Однако зависимость d(ω) не всегда линейная, поэтому, не сильно теряя в точности, можно спокойно забить на формулу для ωреальная, и с помощью интерполяции многочленом по 3-4 близлежащим точкам решить уравнение d(ω)=0. Благо, d(ω) вполне гладкая и даже d'(ω)≈0.

Осталось только доделать интерполяцию и решение уравнения с её помощью, проверить приемлемость метода для других тембров (на всякий случай, а вдруг), определиться с конечным языком реализации (так и оставлять на окамле или переписать на Ц), и "тюнер" готов к использованию. Из внешних зависимостей будет только sox. Да и то, если научиться брать звук напрямую, то и его не будет.