Верификация частными случаями

Буду говорить в контексте программирования, но соображения можно распространить шире.

Когда мы описываем алгоритм: программу, доказательство теоремы или решение математической задачи — мы строим его описание в рамках некоторой формальной модели. В рамках соглашений и ограничений, которые мы явно или неявно принимаем.

Описать алгоритм вне формальной модели невозможно. Хотя бы потому, что любой язык — уже формализация. 

Отсюда вытекает интересная проблема.

Читать далее

Тарантога: второй блин

Потоки данных во второй версии прототипа Тарантоги. Кликните, чтобы увеличить.

Продолжаю эксперименты. Как видно из заголовка, вторая попытка тоже не удалась, хотя выглядит симпатичнее.

Реализация ушла довольно далеко от описанного в посте о первом блине. В частности, GraphQL не подошёл.

Как всегда, работа породила сторонние результаты. Я подумал об уменьшении сложности работы с данными, вынес в отдельную библиотеку логику работы с предикатами.

Вторую версию концепции я считаю жизнеспособной, но сильно затратной для развития в одного разработчика. Вот если бы меня было несколько, или проект уже существовал в рабочем виде, и надо было только дописывать новых агентов. 

Но мы имеем, что имеем, поэтому буду думать дальше. Скорее всего попробую сделать в лоб: минималистично, стандартными подходами без интеллектуальных извращений. Всё-таки представление об инструменте уже несколько раз в голове перекрутил и оно значительно упростилось.

А пока расскажу что получилось на этот раз.

Читать далее

Pydicates: предикаты для Python

Опубликовал небольшую библиотеку для работы с предикатами в Python: github, pypi. Как всегда, под BSD-3.

Позволяет конструировать функции для отложенных вычислений. Например, описывать такие условия: (OwnedBy('alex') | OwnedBy('alice')) & HasTag('game-design').

Делал для себя, так как уже несколько раз в пет-проектах писал костыли для этого дела. Решил сделать один раз правильно и больше не тратить на это время.

Минимальный пример:

from pydicates import Predicate, common


def HasTag(tag):
    return Predicate('has_tag', tag)


def has_tag(context, tag, document):
    return tag in document['tags']


common.register('has_tag', has_tag)

document = {'tags': ('a', 'b', 'c', 'd')}

assert common(HasTag('a') & HasTag('c'), document)
assert not common(HasTag('a') & HasTag('e'), document)
assert common(HasTag('a') & ~HasTag('e'), document)
assert common(HasTag('a') & (HasTag('e') | HasTag('d')), document)

Больше примеров можно найти в репозитории ./examples

API описано чуть подробнее в ./examples/documents_check.py

Больше примеров можно найти в тестах.

Концепт-документ игры Сказания

Источник изображения: MTG Fetch Lands: What Are They and How to Get Them for Cheap

Ещё один концепт, на этот раз довольно старый. Не думаю, что такую игру будет просто привести к успеху, но идея мне нравится.

Читать далее

Python 3 Types in the Wild

Вышла статья с исследованием состояния статической типизации в Python. Я её наискосок просмотрел, всё примерно так, как я и рассказывал в эссе:

Далее несколько интересных цитат.

Читать далее