Студопедия Главная Случайная страница Обратная связь

Разделы: Автомобили Астрономия Биология География Дом и сад Другие языки Другое Информатика История Культура Литература Логика Математика Медицина Металлургия Механика Образование Охрана труда Педагогика Политика Право Психология Религия Риторика Социология Спорт Строительство Технология Туризм Физика Философия Финансы Химия Черчение Экология Экономика Электроника

Canonicality





Associated with every kind K is a full interpretation function [], read as “canonical”. Given a kind (instance) it returns the canonical form of that kind (instance). The canonical form of a canonical form is itself. If we have a term of the form [k] = l we call the asset l the canonical kind of k. Likewise, for instances,

we use the term canonical instance. When we do not distinguish kind or instance, we say canonical realization or canonical asset.

Canonicality preserves all structure of its domain and, since the codomain is generative (it is constructed entirely by the canonicality operation), then it can have no new structure. This means that it is possible to define a full interpretation between any two canonically equivalent assets, but not necessary that such

interpretations exist.

Thus, canonicality induces an equivalence relation; interpretations do not.

Rewriting logic embedded in a type system are used in [18] to define and compute canonical forms of kinds and instances. All operations within kind theory but for resolution are deterministic due to the fact that that their operational semantics are Church-Rosser. Resolution is defined in general rewriting logic and

is both undecidable and NP-hard, but in all the common cases that we have explored in the actual use of resolution in practice are tractable and decidable1







Дата добавления: 2015-09-07; просмотров: 492. Нарушение авторских прав; Мы поможем в написании вашей работы!




Обзор компонентов Multisim Компоненты – это основа любой схемы, это все элементы, из которых она состоит. Multisim оперирует с двумя категориями...


Композиция из абстрактных геометрических фигур Данная композиция состоит из линий, штриховки, абстрактных геометрических форм...


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


ТЕОРЕТИЧЕСКАЯ МЕХАНИКА Статика является частью теоретической механики, изучающей условия, при ко­торых тело находится под действием заданной системы сил...

Определение трудоемкости работ и затрат машинного времени На основании ведомости объемов работ по объекту и норм времени ГЭСН составляется ведомость подсчёта трудоёмкости, затрат машинного времени, потребности в конструкциях, изделиях и материалах (табл...

Гидравлический расчёт трубопроводов Пример 3.4. Вентиляционная труба d=0,1м (100 мм) имеет длину l=100 м. Определить давление, которое должен развивать вентилятор, если расход воздуха, подаваемый по трубе, . Давление на выходе . Местных сопротивлений по пути не имеется. Температура...

Огоньки» в основной период В основной период смены могут проводиться три вида «огоньков»: «огонек-анализ», тематический «огонек» и «конфликтный» огонек...

Методика обучения письму и письменной речи на иностранном языке в средней школе. Различают письмо и письменную речь. Письмо – объект овладения графической и орфографической системами иностранного языка для фиксации языкового и речевого материала...

Классификация холодных блюд и закусок. Урок №2 Тема: Холодные блюда и закуски. Значение холодных блюд и закусок. Классификация холодных блюд и закусок. Кулинарная обработка продуктов...

ТЕРМОДИНАМИКА БИОЛОГИЧЕСКИХ СИСТЕМ. 1. Особенности термодинамического метода изучения биологических систем. Основные понятия термодинамики. Термодинамикой называется раздел физики...

Studopedia.info - Студопедия - 2014-2025 год . (0.01 сек.) русская версия | украинская версия