Математические основы программирования. Рубрика в журнале - Программные системы: теория и приложения
Ред. заметка
Статья продолжает публикации автора о подходе к использованию конструктивной математики и применении языка с зависимыми типами для доказуемого программирования вычислительной алгебры. Получено конструктивное выражение понятия области с разложением на простые множители для моноидa и кольца с некоторыми дополнительными свойствами. Описан способ построения машинно-проверяемых доказательств для теорем, связывающих понятия разложения на простые множители в областях различного вида. Все описываемые построения и доказательства воплощены полностью в виде программы на функциональном языке Agda
Бесплатно
Реализация высокоточных вычислений в базисе модулярно-интервальной арифметики
Статья научная
Проблема влияния ошибок округления возникает в большом количестве задач в различных областях знаний, включая вычислительную математику, математическую физику, биохимию, квантовую механику, математическое программирование. Для решения таких задач может потребоваться точность в 100-1000 десятичных цифр. В рамках данного исследования разработаны новые способы представления числовой информации - модулярно-позиционные интервально-логарифмические системы счисления, а также методы выполнения арифметических операций для повышения скорости высокоточных вычислений.
Бесплатно
Рекурсивные определения реляционных преобразований
Статья научная
В статье определяются основные конструкции и семантика языка описания действий (action description language), предназначенного для описания и вычисления преобразований отношений моделей ситуаций (реляционных преобразований). Основное отличие описываемого языка от традиционных языков описания действий (STRIPS, ADL и т.п.) заключается в использовании, кроме традиционных (STRIPS-like) правил, их теоретико-множественных композиций и рекурсии это существенно повышает выразительность языка. Описывается функция для вычисления эффектов действий, определенных рекурсивно и доказывается ее частичная корректность.
Бесплатно
Сенсорная сеть с модульной архитектурой
Статья научная
Описан новый подход к организации сенсорной сети на основе устройств с модульной архитектурой. Описываемая аппаратно-программная платформа для сенсорных сетей является своего рода конструктором, который позволит легко собирать сенсорные узлы в соответствии со специфическими нуждами пользователя и разворачивать сенсорные сети там, где это нужно. Данный подход призван значительно расширить сферу применения сенсорных сетей
Бесплатно
Слияние циклов для локализации данных
Статья научная
Для улучшения локализации данных используется слияние циклов. Слияние циклов, имеющих общие переменные, может ускорить исполнение за счёт уменьшения количества кэш-промахов. Это преобразование известно давно, но компиляторы выполняют его лишь для простейших случаев.Наши улучшенные алгоритмы используют предварительные преобразования для корректного слияния циклов, имеющих разное количество итераций и информационные зависимости.
Бесплатно
Современные тенденции в области хранения и обработки сенсорных данных
Статья научная
Содержится обзор современных тенденций в области хранения и обработки сенсорных данных, различные подходы рассматриваются с точки зрения применимости к организации масштабируемых высокопроизводительных хранилищ данных, выделены наиболее перспективные решения с учетом специфики сенсорных данных и их использования
Бесплатно
Струи как основа реализации понятия т-процесса для платформы JVM
Статья научная
Распространение и доступность современных параллельных аппаратно-программных платформ демонстрирует отставание уровня инструментов разработки параллельных приложений от нужд разработчиков программ. В ИПС РАН ведется разработка подхода к распараллеливанию программ, основанного на использовании модели вычислений «самотрансформация вычисляемой сети». В данной работе рассматриваются различные варианты подходов к реализации для платформы JVM понятия «Т- процесс» –– базового понятия данной модели вычислений. Анализируются потенциальные проблемы, связанные с реализацией понятия «Т-процесс», как на основе классических потоков ОС/JDK, так и в случае внесения поддержки легковесных потоков непосредственно в код виртуальной машины. Предлагается подход к реализации Т-процессов, основанный на использовании понятия струй, т.е. легковесных потоков, реализуемых вне ядра JVM. Приводятся результаты экспериментального сравнения подходов к реализации понятия «Т-процесс», основанных на использовании классических потоков и струй (англ. fibers). Анализируется эффект от использования струй для реализации модели вычислений «самотрансформация вычисляемой сети», используемой в разрабатываемом языке параллельного программирования ajl для платформы JVM
Бесплатно
Суперкомпьютерные технологии в решении задач биоинформатики
Статья научная
С 2001 года в ИВМиМГ СО РАН функционирует Центр коллективного пользования «Сибирский суперкомпьютерный центр» (ССКЦ) с пиковой производительностью кластеров 115 TFlops. Основные задачи центра: разработка и использование суперкомпьютерных технологий для математического моделирования различных задач, решаемых в институтах СО РАН; обеспечение работ институтов СО РАН и университетов Сибири по математическому моделированию в фундаментальных и прикладных исследованиях; обучение специалистов СО РАН и студентов университетов методам параллельных вычислений на суперкомпьютерах, методам моделирования больших задач. Одним из основных потребителей ресурсов является Центр коллективного пользования «Биоинформатика», созданный на базе Института Цитологии и Генетики СО РАН. В рамках совместных работ центров коллективного пользования были разработаны программные пакеты по наиболее актуальным научным направлениям биоинформатики. Работа посвящена обзору ресурсов ССКЦ и прикладным программным пакетам по биоинформатике. Ключевые слова и фразы: суперкомпьютеры с гибридной архитектурой, биоинформатика, компьютерная геномика, эволюция, прикладные программные пакеты
Бесплатно
Теоретико-категорный подход к проектированию вычислительных систем
Статья научная
Вычислительная система называется алгебраической, если она содержит дискретные управляемые посткремниевые узлы. Предложен теоретико-категорный подход к проектированию таких систем, нацеленный на эффективное применение математических методов отображения расчетных задач на архитектуру таких систем. Построены категории, объектами которых служат алгебраические модели вычислений узлов и систем, а морфизмами служат спецификации действий по интеграции узлов в системы. Конечные диаграммы в таких категориях представляют собой формальные архитектурные модели алгебраических вычислительных систем.
Бесплатно
Троичная виртуальная машина и троичная ДССП
Статья научная
В научно-исследовательской лаборатории троичной информатики (НИЛ ТИ) ВМК МГУ (в период с 2010 по 2013 г.) созданы троичная виртуальная машина ТВМ и кросс-система ДССП-ТВМ разработки программ для неё на языке ДССП-Т – троичном варианте языка ДССП. В статье представляются архитектура троичного процессора ТВМ и его система команд, основные черты языка ДССП-Т и возможности среды разработки ДССП-ТВМ, а также поясняются некоторые проблемные аспекты реализации имитатора ТВМ, кросс-компилятора языка ДССП-Т и диалогового интерпретатора ДССП/ТВМ для специфичной троичной машины. Ключевые слова и фразы: троичный компьютер, имитационная модель, ТВМ, ДССП, структурированное программирование, сшитый код
Бесплатно
Статья научная
В статье приводится описание разработанного автором многофункционального графического интерфейса визуального проектирования широкого спектра различных вычислительных процессов и технологических цепочек. Описание задачи формируется пользователем с помощью набора готовых функциональных блоков и редактора связей, устанавливающего каналы передачи данных. Интерфейс имеет инструменты для запуска составленных схем задач в параллельно-конвейерном режиме и отслеживания их выполнения
Бесплатно
Устойчивая алгоритмическая привязка к произвольному участку кода программы
Статья научная
При работе над задачей программист наиболее активно взаимодействует с~конечным набором фрагментов кода. Информация об их расположении важна для быстрого перемещения между ними, для других разработчиков и как разновидность документации. Интегрированные среды разработки (IDE) позволяют связывать метки с~участками кода, просматривать список меток и использовать их для быстрой навигации, однако связь между меткой и помеченным местом может теряться при редактировании кода, особенно при изменении за пределами IDE. В предыдущих работах авторами предлагается интегрируемый в~IDE инструмент, позволяющий устойчиво к~изменению кода помечать крупные синтаксические сущности программы («привязываться» к~ним). Описание помечаемого элемента строится по~абстрактному синтаксическому дереву (АСД) программы и используется для алгоритмического поиска этого элемента в~отредактированном позднее коде. Поиск осуществляется с~успешностью от 99 до 100.. Целью настоящей работы является устойчивая алгоритмическая привязка к~произвольному участку кода. Для привязки к~однострочному фрагменту кода предложены расширение модели, описывающей помечаемый фрагмент, и дополнительный алгоритм поиска. Введена необходимая формализация и предложен алгоритм встраивания в~АСД узлов, соответствующих многострочным фрагментам; показано, что в~результате такого встраивания не нарушается корректность АСД. В~коде трёх крупных проектов на~языке C. произведены привязки к~случайно выбранным строкам. Ручной проверкой результатов поиска этих строк в~отредактированном коде подтверждено, что привязка устойчива к~редактированию кода.
Бесплатно
Статья научная
Фронтальный алгоритм решения SAT задачи
Статья научная
Алгоритм вычисления семантического значения конъюнктивных формул вида $U = F(X_1, X_2,..., X_n)$ в неклассической пропозициональной логике $L_{S_{2}}$ также вычисляет множество всех решений логического уравнения $F({x_1}, {x_2},..., {x_n})= 1,$ где $F(X_1, X_2,..., X_n)$ - формула булевой алгебры множеств, составляющих дискретную диаграмму Венна. Элементы этих множеств являются неотрицательными целыми числами. На основе этого алгоритма строится новый алгоритм для решения задачи $ SAT$. Существенная разница между ним и семейством алгоритмов, основанных на $ DPLL $, и $ CDCL $, - замена булевых переменных множествами. Это позволяет эффективно проверить выполнимость не одного, а многих наборов значений логических переменных ${x_1}, {x_2},..., {x_n}$.
Бесплатно
