Карты (замены) с бесконечными доменами - PullRequest
Новая
       17

Карты (замены) с бесконечными доменами

3 голосов
/ 11 октября 2011

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

  • σ | e (x n ) = если x n ∈ FV (e), то σ (x n ) иначе х п

Поскольку операция ограничения применяется к всем переменным в возможно бесконечном наборе, тип данных, такой как конечная карта, не может "смотреть вперед", чтобы предвидеть ограничение при добавлении новых привязок. И, конечно же, использование конечных отображений с бесконечными областями приводит к нетерминации. Есть ли способ имитировать такие операции, как ограничение, с использованием конечных отображений или другого представления подстановок, который позволил бы легко записывать такие операции, как ограничение над ними? Мне кажется, я упускаю очевидное решение - например, пользуюсь ленивой оценкой или функциональными заменами.

редактирование:

Для справки, вот наивное решение с использованием конечных карт. Каждый раз, когда операция ограничения применяется к подстановке σ и выражению e, найдите множество FV ( e ) свободных переменных, равное e . Для каждой переменной x n в области σ, если x n ∈ FV ( e ), тогда установите σ '(x n ) = x n . Вернуть σ '. Предположим, что σ '(x n ) = x n , если x n dom (σ').

edit: Это очевидное решение, которое я упустил.

1 Ответ

4 голосов
/ 11 октября 2011

Ну, самая прямая модель замещения - это просто сама функция. 

newtype Subst = Subst { apply :: Var -> Expr }

singleton :: Var -> Expr -> Subst
singleton v e = Subst (\v' -> if v == v' then e else Var v')
-- etc.

Для первого прохода при реализации языка, это, вероятно, то, что я использовал бы, как только сломались конечные карты. Это не быстро (потребует O (n) времени, когда n - размер домена), но это просто. Держите его в капсуле, чтобы вы могли заменить его позже.

Если вы начнете получать удар в течение времени O (n), тогда вы можете переключиться на три. data-inttrie было специально написано, чтобы вести себя так же, как функция на целых числах, но разрешать эффективные модификации в отдельных точках (как хотелось бы с помощью функции подстановки). Если ваши переменные однозначно идентифицируются целыми числами, вы можете использовать их напрямую, в противном случае вы можете эмулировать стиль для строк или для всего, что вы используете.

Но мне также кажется странным, что вам нужно "смотреть вперед". Я никогда не нуждался в этом в моих языковых реализациях; если вы добавляете новую привязку в ограниченную замену, ограничение не применяется к новым привязкам (в противном случае семантика будет неправильной). Конечные карты сделали свое дело во всех случаях, когда я не делаю что-то нелепо странное (а те обычно не работают).

...