Здравствуйте, kochetkov.vladimir.

Для чистой (и не очень) функциональщины есть ряд "машин" (по аналогии с МТ), реализующих их семантику, и на базе которых и построены реализации ФЯ. Ключевые слова для гугления:
SECD machine, "The Zinc Experiment", STG machine, term graph rewriting. Из трех последних выросли OCaml, Haskell и Clean соответственно.

Не очень понятно что такое конфигурация. Предположу, для лямбда-исчисления — это "состояние" между последовательными применениями аппликаций-абстракций-редукций. Похоже на алгорифмы маркова.

Не спец.

В процессе подготовки к вебинару (см. подпись) возник вопрос... Для машины Тьюринга (МТ) конфигурация (рантайм-снэпшот процесса вычисления) определяется как текущее состояние, в котором находится МТ, содержимое ее ленты и позиция на этой ленте. Конфигурация позволяет сделать срез по конкретной МТ, проанализировать его и продолжить вычисление. Это важнейшее понятие с т.з. анализа данной модели и исследования тех или иных нетривиальных свойств частично-рекурсивной функции (ЧРФ), которую реализует МТ. Например, понятие уязвимости конкретной ЧРФ, вычисляемой на МТ, может быть выражено, как достижимая конфигурация, при которой нарушается любое из свойств защищенности (конфиденциальность, доступность, целостность, аутентифицированность, авторизованность, неотказуемость) потоков данных, принадлежащих области ее определения или области значений. Например, в http://www.slideshare.net/kochetkov.vladimir/hdswasm-russianproofreaded/26 я рассматриваю пример МТ, уязвимой сразу в двух конфигурациях, достижимых в случае, если входные данные будут начинаться с пустого символа (тогда МТ перейдет в неопределенное состояние) или будут содержать управляющий символ # (тогда удаление символов "А" из подстроки после него осуществляться не будет). В первом случае, нарушается доступность исходной МТ и (в зависимости от конкретной реализации УМТ, которая ее выполняет), нарушение целостности программы исходной МТ. Во втором — нарушение целостности выходного потока данных (обход фильтрации символов "А"). Соответственно, в первом случае уязвимостью является конфигурация, наступающая при обработке первого символа, если этот символ пустой, а во втором — при первом срабатывании любой из функций перехода, связанных с символом #.

Стало интересно, а что является конфигурацией в эквивалентых моделях вычислений (конкретно: в λ-исчислении и нормальных алгоритмах Маркова)? Или, хотя бы, какую характеристику процесса вычисления в этих моделях можно взять за основу, чтобы дать аналогичное определение уязвимости и в них?

Для марковских алгоритмов все вроде бы достаточно просто — конфигурацией там является текущее значение слова к которому применяются формулы подстановки. Соответственно, уязвимостью в них является достижимое значение преобразуемого слова, при котором нарушается любое из свойств его защищенности. Например, если марковской алгоритм обрабатывает слово, изначально содержащее символ, который используется алгоритмом в качестве управляющего (как в случае с #), то уязвимостью в нем будет являться то состояние исходного слова, при котором впервые произойдет применение формулы подстановки, основанной на вхождении этого символа.

В λ-исчислении все как-то слегка сложнее. Насколько я понимаю, текущее состояние вычислительного процесса там можно выразить через своеобразный стек вычислений — упорядоченное множество троек (F, A, C), где F — функция, A — множество значений ее аргументов, с которыми она вычисляется и C — множество значений всех свободных переменных, на которые она ссылается (пустое для чистых функций). Следовательно, в примере с #, уязвимостью будет являться последняя в последовательности вычислений функция, область значений которой зависит от появления символа # в ее аргументах или свободных переменных.

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

Здравствуйте, kochetkov.vladimir, Вы писали:

KV>В λ-исчислении все как-то слегка сложнее. Насколько я понимаю, текущее состояние вычислительного процесса там можно выразить через своеобразный стек вычислений — упорядоченное множество троек (F, A, C), где F — функция, A — множество значений ее аргументов, с которыми она вычисляется и C — множество значений всех свободных переменных, на которые она ссылается (пустое для чистых функций). Следовательно, в примере с #, уязвимостью будет являться последняя в последовательности вычислений функция, область значений которой зависит от появления символа # в ее аргументах или свободных переменных.

Я не так чтоб сильно настоящий сварщик, но мне интересно, что за "грязные" функции в чистом λ-исчислении и какое отношение к этому имеют свободные переменные?

Здравствуйте, Курилка, Вы писали:

К>Я не так чтоб сильно настоящий сварщик, но мне интересно, что за "грязные" функции в чистом λ-исчислении

Ну и бред же я написал Думая о λ-исчислении, я параллельно прикидывал подходы к динамическому анализу реального функционального кода, вот и... Поскольку входные и выходные данные в λ-исчислении кодируются при помощи λ-термов, а процесс непосредственно вычисления представляет собой последовательное применение правил редукции к ним, то аналогом конфигурации здесь будет промежуточное значение "недоредуцированного" выражения, как уже написал fin_81. И, следовательно, уязвимостью здесь будет достижимое значение выражения, последующая редукция которого приводит к нарушению свойств защищенности потока данных. Похоже, что так =/

К>какое отношение к этому имеют свободные переменные?

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

Здравствуйте, fin_81, Вы писали:

_>Не очень понятно что такое конфигурация.

Я же дал определение:

текущее состояние, в котором находится МТ, содержимое ее ленты и позиция на этой ленте

более обще — это набор данных, необходимый и достаточный для того, чтобы "сериализовать" конкретный процесс вычисления и, передав их в другой экземпляр вычислителя, возобновить в нем сериализованный процесс с того же места. Фактически — это состояние процесса вычисления, но поскольку в МТ этот термин уже был забит, его решили назвать конфигурацией))

_>Предположу, для лямбда-исчисления — это "состояние" между последовательными применениями аппликаций-абстракций-редукций. Похоже на алгорифмы маркова.

Да, похоже на то.

Здравствуйте, kochetkov.vladimir, Вы писали:

KV>Здравствуйте, Курилка, Вы писали:

К>>какое отношение к этому имеют свободные переменные?

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

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

Здравствуйте, Курилка, Вы писали:

К>Ты поясни для начала, что такое "грязное λ-исчисление", ну и "грязные λ-функции" как его проявление.

Я не употреблял таких терминов, но, как сказал выше: думал об одном, а написал другое. Замени в том абзаце "λ-исчисление" на "функциональная модель вычислений" и получится примерно то, что я хотел сказать.

Здравствуйте, kochetkov.vladimir, Вы писали:

KV>А разве можно считать чистой функцию, ссылающуюся на свободные переменные?
Её и функцией то считать нельзя.

Здравствуйте, D. Mon, Вы писали:

DM>Для чистой (и не очень) функциональщины есть ряд "машин" (по аналогии с МТ), реализующих их семантику, и на базе которых и построены реализации ФЯ.
Непосредственно в терминах λ-выражений формулируется гораздо проще.

Здравствуйте, Трурль, Вы писали:

DM>>Для чистой (и не очень) функциональщины есть ряд "машин" (по аналогии с МТ), реализующих их семантику, и на базе которых и построены реализации ФЯ.
Т>Непосредственно в терминах λ-выражений формулируется гораздо проще.

В них не кодируется стратегия вычислений (normal/applicative/...), надо задавать отдельно. И не очень понятно, как описывать sharing, например.