Описание тега lambda-calculus
λ-исчисление - это формальная система для определения функций, их применения и рекурсии, которая составляет математическую основу функционального программирования.
2
ответа
В лямбда-исчислении, что если применить выражение к нефункциональному выражению?
Я новичок в Lambda Calculus. Я читал об определении лямбда-выражения в Википедии. Множество лямбда-выражений, Λ, может быть определено индуктивно: Если x переменная, то x ∈ Λ Если x переменная и M ∈ Λ, то (λx.M) ∈ Λ Если M, N ∈ Λ, то (M N) ∈ Λ Экзем…
02 апр '17 в 08:13
1
ответ
Как я могу оценить выражение?
Как я могу оценить выражение, учитывая список значений для переменных, которые оно содержит? eval::[(Variable,Integer)]->Expr->Integer Пример: eval[("x",2), ("y",4)](Mult(Plus(Var "x") (Const))(Var "y"))= 12
28 ноя '08 в 00:46
2
ответа
Функция рекурсивного лямбда-исчисления
Я хотел бы создать функцию лямбда-исчисления P, что (P x y z) дает ((x y)(x P)(P z)), Я пытался использовать варианты Y-комбинатор / Тьюринга комбинатор, то есть функции вида λg.(g g), так как мне нужно воспроизвести саму функцию, но я не вижу пути …
18 апр '16 в 16:19
4
ответа
Y-комбинатор в D?
Я пытаюсь лучше изучить Y-комбинатор (вроде как я это понимаю на Схеме) и внедрить его в D 2.0, и у меня довольно плохо получается: auto fact = delegate(uint delegate(uint) recurse) { return delegate(uint n) { return n > 1 ? n * recurse(n - 1) : …
04 авг '11 в 07:44
1
ответ
Невозможно понять термин F-омега
Я читаю статью о Fω и не могу понять причины этого утверждения: Типовой член типа (∀γ:*. F γ → β) показывает, что F - постоянная функция, которая всегда возвращает β. Я предполагаю, что "F γ → β" - это термин типа, т. Е. Тип стрелки. Этот тип стрелк…
29 ноя '17 в 10:19
3
ответа
Арифметика с церковными цифрами
Я работаю через SICP, и проблема 2.6 поставила меня в затруднительное положение. При работе с церковными числами концепция кодирования нуля и 1 в качестве произвольных функций, которые удовлетворяют определенным аксиомам, кажется, имеет смысл. Кроме…
12 окт '10 в 07:09
1
ответ
Каноническая форма (МБ) (МБ)
Существуют ли лямбда-члены M и B с M =/= B, чтобы MB и (MB) (MB) имели одинаковую каноническую форму? Является ли проблема, с которой я столкнулся, пока я еще новичок с лямбда-исчислением, я подошел к этому, имея M = λx.x и B = λy.y Μ Β = (λx.x) (λy…
07 сен '18 в 18:46
1
ответ
Как бы вы абстрагировали шаблон в этой паре "похожих по форме" типов данных?
Общий вопрос У меня есть пара типов данных, которые представляют собой два разных способа представления одной и той же вещи: один записывает имя переменной в String, а другой записывает имя переменной в Int. В настоящее время они оба определены. Тем…
28 янв '14 в 00:53
1
ответ
Лямбда-нотация в НЛП
Я должен сделать анализ семантики и использовать лямбда-нотацию для следующих предложений Мне нужна помощь для: Что такое лямбда-нотация для определенного и неопределенного определителя? Anna drew a red panda. За a я использовал exist x: lambda p: p…
15 ноя '15 в 00:38
3
ответа
Какое официальное название для этого синтаксиса?
Иногда в Scheme у меня есть функции, которые принимают такие аргументы add 3 4 Что вы называете такого рода "списком", где его элементы похожи a1 a2 a3? Я не думаю, что вы можете назвать это списком, потому что списки содержатся в скобках, а элемент…
27 апр '10 в 04:34
6
ответов
Этапы сокращения функции предшественника лямбда-исчисления
Я застреваю с описанием Википедии функции предшественника в лямбда-исчислении. Википедия говорит следующее: ПРЕД:= λnfx.n (λgh.h (g f)) (λu.x) (λu.u) Может кто-нибудь объяснить пошаговые процессы сокращения? Благодарю.
09 янв '12 в 14:51
0
ответов
Генерация свежих имен для безымянных лямбда-терминов
Есть ли какой-то общий метод или библиотека для генерации свежих имен при преобразовании безымянных лямбда-терминов в именованные? Это то, что я придумал (минимальный пример основан на представлении школы Haskell): {-# LANGUAGE FlexibleInstances #-}…
04 апр '16 в 20:04
3
ответа
Что требуется для того, чтобы расширить реализацию нетипизированного лямбда-исчисления, чтобы охватить просто типизированное лямбда-исчисление?
Мэтт Майт говорит о реализации интерпретатора лямбда-исчисления в 7 строках схемы: ; eval takes an expression and an environment to a value (define (eval e env) (cond ((symbol? e) (cadr (assq e env))) ((eq? (car e) 'λ) (cons e env)) (else (apply (e…
21 июн '16 в 05:14
2
ответа
Спецификация типа полиморфа
Я создал тип, который определяет (nat,bool) -> T пары: Definition pprod_nb : Set := forall T:Set, (nat -> bool -> T) -> T. Теперь я хочу специализировать pprod_nb с T = nat: (nat -> bool -> nat) -> nat Мой вопрос: как указать тип ф…
28 мар '18 в 09:22
1
ответ
Лямбда-исчисление, нормальный порядок, нормальная форма,
В лямбда-исчислении, если термин имеет нормальную форму, стратегия сокращения нормального порядка всегда будет производить его. Мне просто интересно, как строго доказать вышеприведенное утверждение?
30 янв '16 в 16:19
1
ответ
Функциональная "симултаниты"?
По этой ссылке говорится о функциональном программировании. В частности, автор говорит это: Одновременность означает, что мы предполагаем, что утверждение в лямбда-исчислении оценивается одновременно. Тривиальная функция: λf(x) ::= x f(x) определяет…
08 авг '14 в 00:00
1
ответ
Звонок по имени против обычного порядка
Я знаю, что эта тема обсуждалась несколько раз, но кое-что мне все еще неясно. Я прочитал этот вопрос о различиях между аппликативным порядком / вызовом по значению и обычным порядком / вызовом по имени, и есть кое-что, что я хотел бы уточнить раз и…
06 июл '16 в 09:03
1
ответ
Конвертировать естественный язык в логическую формулу
Я несколько дней пытался написать грамматику NLTK, чтобы преобразовать простые французские предложения в логические формулы. Моя проблема может быть похожа на английские предложения. Моя цель состоит в том, чтобы эта грамматика принимала несколько з…
05 июл '15 в 00:21
1
ответ
Пример замен во время компиляции, ухудшающих программу
Представьте себе наивный компилятор типизированного лямбда-исчисления (чтобы исключить довольно болезненную проблему нетерминации и неявной рекурсии), который использует нормализацию (включая подстановки под лямбда-выражения) в качестве "оптимизации…
16 дек '16 в 00:59
2
ответа
Предпосылки для изучения лямбда-исчисления
Может кто-нибудь сказать мне, каковы предпосылки для изучения лямбда-исчисления (если таковые имеются)?
27 дек '10 в 06:24