Переменная
    Переменные обозначаются одиночными символами, неделимы, означают что-то.
    Запись переменной в виде символа считается/признаётся термом.
    что если количество необходимых переменных превзойдёт количество символов в алфавите?
    тогда получится, что нужно создать другой язык, в котором переменные смогут обозначаться по-другому,
    например несколькими символами, а разделять их будут не границы символов,
    а дополнительно вставленные пробелы.
Функция
    для λ-исчисления важно то, что f трактуется как алгоритм,
    вычисляющий результат по заданному входному значению.
    f - это имя функции
    запись
    f a - это запись "вызова" функции с аргументом а (см. "Аппликация")
λ-абстракция
    λ-абстракция "строит"/"создаёт" функции по заданным выражениям (выражения и термы очень похожи, см. "Терм")
    запись λ x . t,
    где t - это терм, а x - это переменная
    обозначает, что мы определили функцию без имени (λ функция от аргумента x),
    значение которой равно значению выражения t ≡ t [x] (выражения и термы очень похожи, см. "Терм")
    (построили над выражением t функцию)
    λ-абстракция коротко может называться "Абстракция".
    λ-абстракция это операция в лямбда-исчислении (см. "λ-исчисление")
Терм λ-исчисления
    кусок текста на языке λ-исчисления. Текст на языке λ-исчисления может рассматриваться как выполняемый код (алгоритм), тогда
    терм - это кусок кода(алгоритма) записанный на языке λ-исчисления

    Термы λ-исчисления называют так же λ-термами,
    Термы λ-исчисления называют также объектами («обами»)

    1) термами являются переменные
    2) термом является запись операции "λ-абстракция"
    (λ x.M) это терм, если x переменная, а M - терм
    3) термом является запись (M N)
    (M N) это терм, если M и N - это термы
    Существует возможность, что при склейке термов
    возникнет возможность применения операции "Аппликация"

    т.е. терм это некая последовательность переменных и функций
    может так оказаться что можно все функции вычислить и получится цепочка переменных
    а может быть переменных нет, и функции не все с параметрами, тогда получится функция
    а может оказаться и просто некая последовательность из переменных и функций
    (кусок текста/кода на языке λ-исчисления)
Аппликация
    Аппликация это вызов функции с аргументом .
    аппликация f к a может рассматриваться двояко:
    - как результат (применения f к a), или же (вопрос, а что такое "Результат"? это терм (см. "Терм"))
    - как процесс вычисления f a.

    Аппликация может так же называться "применение".
    Аппликацию обычно обозначают f a, где f — функция, а a — аргумент.
    Запись f a соответствует общепринятой в математике записи f(a),
    которая тоже иногда используется (см. "Функция").
    для λ-исчисления важно то, что f трактуется как алгоритм,
    вычисляющий результат по заданному входному значению.

    интерпретация аппликации как процесса связана с понятием β-редукции (см. β-редукция).
    Аппликация это операция в лямбда-исчислении (см. "λ-исчисление")
β-редукция
    β-редукция является единственной «существенной» аксиомой λ-исчисления
    с β-редукций λ-исчисление обладает свойством полноты по Тьюрингу

    для вычисления выражения
    (λx.t) a
    в которое входят и абстракция и аппликация
    необходимо выполнить подстановку терма "а" в выражение "t" вместо переменной "x"
    (λx.t) a = t [x := a]
    (см. "Подстановка" ?).

    Выражение вида
    (λx.t) a
    т.е. применение абстракции к некому терму, называется редексом (redex).
λ-исчисление
    https://ru.wikipedia.org/wiki/Лямбда-исчисление
    опирается на понятие "Термы λ-исчисления" (см. "Терм λ-исчисления")
    опирается на понятие "β-редукция" (см. "β-редукция")
    λ-исчисление включает в себя операции "Аппликация" и "λ-абстракция"
    операции "Аппликация" и "λ-абстракция" положены в основу λ-исчисления.
    операции "Аппликация" и "λ-абстракция" называют "Фундаментальные операции λ-исчисления"
η-преобразование
    выражает идею, что две функции являются идентичными тогда и только тогда, когда,
    будучи применёнными к любому аргументу, дают одинаковые результаты.
    f = (λx.f) x
    если x не имеет свободных вхождений в f, иначе
    свободная переменная x после преобразования станет связанной внешней абстракцией или наоборот
    способ дать функции имя?
    Можно ввести в синтаксис языка новый сахар: "описание функции через знак равенства" и
    f = (λx.f)
    "описание разных функций на разных строках"
    Возникнут, правда, проблемы с тем, что переменные станут разными, некоторые - просто переменные, которые что-то там значат, а некоторые - функции, которые надо поискать "в разных строках".
    Если в языке нет типов (то есть, существует единственный тип), и имена переменных хранят функции, то этот единственный тип должен быть типом "функция", т.е. все переменные в языке - это функции, только некоторые определены, а некоторые - нет.

Если рецепт - это алгоритм, то опишите приготовление манной каши при помощи λ-исчисления (юзерстори изложена в документе 1938, Николай Носов, "Мишкина каша").

Отредактировано Лис (2021-12-26 12:16:25)