В исчислении MCLL допустимо правило подстановки: если z ∈ Var и MCLL → Γ,то MCLL → Подстановка →Γ[z := A] (где z ∈ Var∪{1}) определяется следующим образом: если z = pi,то вместо каждого вхождения pi в → Γ подставляется A, а вместо каждого вхождения ¯ pi подставляется A⊥;если Γ[z := A]. понимается как →A⊥ Лемма 3. <...> Если MCLL→Γ[pi := ¯ 2 A⊥ Мы также будем использовать двусторонние MCLL-секвенции: запись A1A2 . <...> В исчислении MCLL допустимо правило эквивалентной замены: если B ↔ C и MCLL → Γ[z := B],то MCLL → Γ[z := C]. <...> Имеет место эквивалентность (1⊗⊥)(¯ Две формулы A и B называются эквивалентными (обозначение A ↔ B), если MCLL A → B 1 B1 . <...> Bm. pi, 1 1, Определим стандартный перевод из типов и секвенций L∗(\,1) в формулы и секвенции MCLL: pi секвенции Π→C с типами из Tp(\,1). <...> Получится выводимая в MCLL секвенция, причем, так как q не входит в секвенция эквивалентной замены получаем MCLL (q \ q) \(pi \ q)]. <...> Подставим в эту секвенцию Π → C, это будет C, замечания. <...> Работа поддержана РФФИ (грант № 08–01–00399), программой “Ведущие научные школы” (грант НШ–65648.2010.1) и программой сотрудничества междуШвейцарией и Россией в области науки и техники (STCP–CH–RU). <...> Equivalent types in Lambek calculus and linear logic. <...> Поступила в редакцию 01.12.2010 УДК 519.718 ЛЕГКОТЕСТИРУЕМЫЕ СХЕМЫ ДЛЯ ЛИНЕЙНЫХ ФУНКЦИЙ C.Р. <...> Беджанова1 В работе установлено, что линейную булеву функцию от n переменных можно реализовать неизбыточной схемой из функциональных элементов в базисе {&,∨, ¯}, которая в случае инверсных неисправностей на выходах элементов допускает единичный диагностический тест длины ] log(n−1)[ +2. <...> 1Беджанова Светлана Руслановна — асп. каф. дискретной математики мех.-мат. ф-та МГУ, e-mail: azjunja@mail.ru. <...> В смысле этого перевода MCLL Π → C для любой pi. <...> №4 Ключевые слова: схемы из функциональных элементов, инверсные неисправности, диагностические тесты, длина теста. <...> Пусть в схемах в неисправное состояние может перейти выход ровно одного из элементов и эта неисправность инверсная. <...> Это означает, что если в исправном состоянии элемент <...>