Я изучаю теорему SMN, и концепция напомнила мне о карри.
Из википедии статьи о теореме SMN :
теорема утверждает, что для данного языка программирования и целые положительные числа т и п, существует определенный алгоритм, который принимает в качестве входных данных исходный код программы с т + п свободных переменных, вместе с т значений. Этот алгоритм генерирует исходный код, который эффективно подставляет значения для первых m свободных переменных, оставляя остальные переменные свободными.
Из статьи о карри :
Интуитивно, карри говорит: «Если вы исправите некоторые аргументы, вы получите функцию от оставшихся аргументов»
Похоже, та же идея для меня. Единственная причина, по которой я не уверен, состоит в том, что в материалах, с которыми я столкнулся на smn, не упоминается карри (и наоборот), поэтому я хотел проконсультироваться с ним, чтобы убедиться, что я действительно его получаю.
источник
Ответы:
Да, это то же самое.
Карринг - это понятие из -calculus. Это преобразование между и . Думайте об этом как «если у нас есть функция двух аргументов типов и , то мы можем исправить первый аргумент (типа ), и мы получим функцию от оставшегося аргумента (типа )». Фактически это преобразование является изоморфизмом. Это сделано математически точным с помощью математических моделей (типизированных) -calculus, которые являются декартовыми замкнутыми категориями .A × B → C A → ( B → C ) A B A B λλ × B → C A → ( B → C) A В A В λ
Существует категория пронумерованных наборов. Нумерованный набор - это пара где - набор, а - частичная выборка, т. Карта из чисел на , которая также может быть неопределенной. Если , то мы говорим , что является кодом из . В теории вычислимости есть много примеров. Всякий раз, когда мы кодируем некоторую информацию числом, мы получаем пронумерованный набор. Например, существует стандартная нумерация частично вычислимых функций, так что - это число, вычисляемое частичной вычислимой функцией, закодированнойA ν A : N → A A ν A ( n ) = x n x φ φ n ( k ) n k( A , νA) A νA: N → A A νA( n ) = x N Икс φ φN( к ) N применительно к . (Результат может быть неопределенным.)К
Морфизм нумерованных множеств - это реализованное отображение , что означает, что существует такое, что для всех в области . Это выглядит сложно, но все, что он говорит, это то, что делает с кодами то, что делает с элементами. Это математический способ сказать, что «программа реализует функцию ».п ∈ N F ( ν ( к ) ) = N , B ( ф п ( K ) ) K v , A ф п ф ф п пе: ( A , νA) → ( B , νВ) n ∈ N е( νA( k ) ) = νВ( φN( к ) ) К νA φN е φN е
Вот изюминка: категория пронумерованных множеств является декартовой замкнутой. Поэтому мы можем интерпретировать в нем напечатанный -calulus и спросить, какая программа реализует операцию каррирования. Ответ: программа, заданная теоремой smn.λ
источник