Публикации по теме 'lambda-calculus'
Магические числа
Волшебные числа
В предыдущей статье была фраза о том, что числа тоже являются функциями и что такое 1 = () =› {} . Итак, давайте копнем немного дальше. Если один — функция, то что тогда два? Предположим, что это функция функции, например
one = () => {}
two = () => () => {}
// which means
two_ = () => one
Проще говоря, здесь цифра — это количество толстых стрелок. Так что ноль это ничто. Один — это одна нулевая глубина, два — две глубины и так далее. Если..
Непрактичные, функциональные списки (список без лямбда)
В своем первом посте я хотел сделать что-то необычное. Я не хочу утомлять вас сверхсерьезными фактами или прикрывать что-то практическое в этом отношении. Вместо этого мы займемся своего рода упражнением по программированию. Идеи в этом посте взяты из математической темы под названием Церковные кодировки и вдохновлены другой статьей Список без лямбды .
Сегодняшняя цель - восстановить функциональность языка с помощью ОЧЕНЬ ограниченного набора инструментов. Что-то вроде..
Вопросы по теме 'lambda-calculus'
Грамматика Antlr4 для применения функций
Я пытаюсь написать простую грамматику лямбда-исчисления (см. Ниже). Проблема, с которой я столкнулся, заключается в том, что приложение функции, похоже, рассматривается как правоассоциативное, а не левоассоциативное, например. «f 1 2» анализируется...
831 просмотров
schedule
23.10.2021
Как вы оцениваете возведение в степень церковных цифр?
Возведение в степень по церковным цифрам определяется как:
expt ≡ λmnsz.nmsz
Но у меня возникают проблемы с его оценкой в тех случаях, когда степень не равна 0 или 1. Рассмотрим этот пример:
expt C3 C2 ≡ [λmnsz.nmsz](λsz.s^3 z) (λsz.s^2...
1369 просмотров
schedule
27.09.2021
Простое лямбда-исчисление DSL с использованием GADT в OCaml
Как с помощью GADT определить в OCaml простой DSL, похожий на лямбда-исчисление? В частности, я не могу понять, как правильно определить средство проверки типов для преобразования нетипизированного AST в типизированный AST, а также не могу определить...
1463 просмотров
schedule
04.11.2021
Можно ли реализовать сложение набранных цифр Чёрча, используя итеративное приращение?
Я не могу найти способ определить добавление как повторяющееся приращение, несмотря на то, что это возможно на нетипизированном языке. Вот мой код:
{-# LANGUAGE RankNTypes #-}
type Church = forall a . (a -> a) -> (a -> a)
zero ::...
264 просмотров
schedule
24.09.2021
Почему необходимо введение Yкомбинатора в λ-исчисление?
Я читаю книгу по λ-исчислению «Функциональное программирование через лямбда-исчисление» (Грег Майклсон). В книге автор вводит сокращенные обозначения для определения функций. Например
def identity = λx.x
и продолжает говорить, что мы должны...
87 просмотров
schedule
16.09.2021
Как я могу доказать, что XOR true true = false в лямбда-исчислении?
Я знаю, что XOR = (a) ((b) (false) (true)) (b), но как я могу уменьшить [xor true true] и получить ложный результат из этого выражения?
191 просмотров
schedule
27.10.2021
Как применить только одну бета-редукцию к λy. (Λx.λy.yx) yz?
Я не понимаю, как получить правильный ответ, который равен λy. (Λw.wy) z
Переименование разрешено только в случае необходимости, и из ответа очевидно, что использовалось переименование.
128 просмотров
schedule
06.10.2021
η-расширение на чистом функциональном языке
В OCaml разрешено иметь в .mli :
val f : 'a -> 'a
val g : 'a -> 'a
и .ml :
let f x = x
let g = f
Однако в F# это отвергается:
eta_expand.ml(2,5): error FS0034: Module 'Eta_expand' contains
val g : ('a -> 'a)...
592 просмотров
schedule
24.02.2022
Реализация CLISP Lambda Calculus Div
Я пытаюсь реализовать функцию разделения с помощью clisp Lambda Calc. стиль
Я прочитал на этом сайте, что лямбда-выражение деления:
Y (λgqab. LT a b (PAIR q a) (g (SUCC q) (SUB a b) b)) 0
Это ИСТИНА и ЛОЖЬ
(defvar TRUE...
633 просмотров
schedule
16.03.2022
Ленивая оценка и вложенные преобразователи потребляют память
Я работаю над крошечным движком лямбда-исчисления, который я хочу, чтобы он был ленивым, как Haskell. Я пытаюсь хотя бы пока придерживаться правил Haskell, чтобы не пришлось все переосмысливать, но я не хочу делать это вслепую.
Я понимаю, что...
354 просмотров
schedule
13.03.2022
Церковные списки в Хаскелле
Мне пришлось реализовать функцию карты haskell для работы со списками церквей, которые определены следующим образом:
type Churchlist t u = (t->u->u)->u->u
В лямбда-исчислении списки кодируются следующим образом:
[] := λc. λn....
4682 просмотров
schedule
01.04.2022
Эквивалентность вызова по значению и по имени
Я работаю над курсом Coursera по функциональному программированию, и в какой-то момент они обсуждают разницу между методами оценки вызовов по значению и вызовов по имени. Они в какой-то момент меня смущают, мол:
Оба метода приводят к одним и...
89 просмотров
schedule
01.04.2022
Haskell — Как дважды написать функцию, используя (.) f g — композиция функций
Вот проблема, мне нужно написать известную дважды функцию
(twice= \x-> \x-> x)
но на этот раз с использованием функции композиции (.) , такой как (.) f g .
Я не знаю, как это решить, потому что я думал в начале сделать так:...
570 просмотров
schedule
08.05.2022
Почему лямбда-выражения Java не представляют новый уровень области видимости?
Насколько я понимаю, в таких языках, как Haskell, а также в рамках лямбда-исчисления каждое лямбда-выражение имеет свою область видимости, поэтому, если у меня есть вложенные лямбда-выражения типа: \x -> (\x -> x) , то первый параметр \x...
6465 просмотров
schedule
14.05.2022
Церковные цифры системы F в Агде
Я хотел бы протестировать некоторые определения в системе F, используя Agda в качестве средства проверки и оценки типов.
Моей первой попыткой представить натуральные числа Черча было написание
Num = forall {x} -> (x -> x) -> (x ->...
68 просмотров
schedule
20.05.2022
лямбда-исчисление: передача двух значений в один параметр без каррирования
Я не могу понять, почему в нетипизированном лямбда-исчислении разрешено следующее бета-сокращение:
(λx.x y) (u v) -> ((u v) y)
В частности, я не могу понять, как можно передать два параметра u и v одному параметру x в части λx.x ....
260 просмотров
schedule
30.05.2022
Сокращение лямбда-исчисления / оценка выражений
Я читал эти заметки по лямбда-исчислению, и у меня возникли некоторые проблемы с сокращением/вычислением одного из выражений в начале.
В частности, функция (λf.λx.f(f(x)))(λy.y^2)(5).
Как именно мне начать это? Он говорит, что ответ равен...
387 просмотров
schedule
03.06.2022
Декларативные модели вычислений в физических машинах
В последнее время я изучал модели вычислений, и у меня возник вопрос.
Кажется, что многие модели вычислений можно реализовать на физических машинах. Некоторые из них фактически основаны на физических лицах.
Например, так обстоит дело с...
122 просмотров
schedule
14.06.2022
тройное лямбда-исчисление в Python NLP
У меня есть список свойств, и мне нужно сделать логическое представление предложения, используя лямбда-исчисление, например, для свойства, «расположенного в», которое должно возвращать (x,y) | < x, located in ,y >
Я пробовал это, но это...
118 просмотров
schedule
28.06.2022
Ошибка проверки связанных переменных для комбинатора K
Недавно у меня появилась копия «Основы языков программирования», второе издание. На странице 29 в книге представлена следующая грамматика для лямбда-исчисления со вкусом схемы:
<expression> ::= <identifier>
::=...
78 просмотров
schedule
26.06.2022
