Аппликативный порядок: всегда полностью оценивайте аргументы функции перед оценкой самой функции, например: (λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x....
Функциональное программирование имеет очень элегантное Lambda Calculus и его варианты в качестве теории резервного копирования. Есть ли такая вещь для ООП? Что такое абстракция для объектно-ориентированной...
Я думаю, что я довольно озадачен тем, что называется исчислением и тем, что называется языком программирования. Я склонен думать и, возможно, мне сказали, что исчисление - это формальная система рассуждений об эквивалентности программ. Программы имеют операционную семантику, указанную машиной,...
Я хотел бы привести пример квин в чистом лямбда-исчислении . Я был довольно удивлен, что я не мог найти один, прибегая к помощи. На странице квин есть списки квин для многих «настоящих» языков, но не для лямбда-исчисления. Конечно, это означает определение того, что я имею в виду под квинем в...
Я задал похожий вопрос на cstheory.SE . Согласно этому ответу на Stackoverflow существует алгоритм, который на не ленивом чисто функциональном языке программирования имеет сложность , тогда как тот же алгоритм в императивном программировании - Ω ( n ) . Добавление ленивости к языку FP сделало бы...
Выражение комбинатора (скажем, в основе SK) можно рассматривать как функцию, которая отображает выражения исчисления комбинатора в выражения исчисления комбинатора. То есть выражение как функцию , где - множество всех синтаксически допустимых выражений комбинатора в базисе SK. Это отображение...
Во-первых, я хотел бы сказать, что мой текст ниже может содержать ошибки, поэтому не стесняйтесь указывать на любые ошибки в моей формулировке вопроса. Рассмотрим нетипизированное лямбда-исчисление с логическими значениями и операторами if, термины которых задаются этим синтаксисом: t ::= v | t t |...
Я пытаюсь понять контекстно-зависимые грамматики. Я понимаю, почему языки как { w w ∣ w ∈ A*}{ww∣w∈A∗}\{ww \mid w \in A^*\} {anbncn∣n∈N}{anbncn∣n∈N}\{a^n b^n c^n \mid n\in\mathbb{N}\} не являются контекстно-свободными, но я хотел бы знать, чувствителен ли контекстный язык, похожий на...
В настоящее время я изучаю лямбда-исчисление, и мне было интересно узнать о двух разных видах написания лямбда-термина. λxy.xyλxy.xy\lambda xy.xy λx.λy.xyλx.λy.xy\lambda x.\lambda y.xy Есть ли разница в значении или способе применения бета-сокращения, или это просто два способа выразить одно и то...
Мне стало известно, что стоимость вывода типа в функциональном языке, таком как OCaml, может быть очень высокой. Утверждение состоит в том, что существует последовательность выражений, такая, что для каждого выражения длина соответствующего типа экспоненциально зависит от длины выражения. Я...
Я изо всех сил пытаюсь понять цель универсального и экзистенциального количественного определения типов. Я играю с написанием игрушечного языка, основанного на исчислении конструкций . Я читал о Морте и Хенке, чтобы помочь мне лучше понять. Я не понимаю, почему у CoC есть и лямбда, и полная...
Я смотрю на исчисление конструкций и его место в лямбда-кубе . Если я правильно понимаю, каждая ось куба может рассматриваться как добавление еще одной операции, связанной с типами, к простому типу исчисления, λ→λ→\lambda_\to . Первая ось добавляет операторы типа к термину, вторые операторы типа к...
Self Types - это расширение исчисления конструкций [1], которое позволяет языку выражать алгебраические типы данных, закодированные с помощью кодировки Скотта. Кодирование Скотта предоставляет возможность сопоставления с образцом O(1), что является одним из основных мотиваторов для включения...
По словам Питера Селинджера , Лямбда-исчисление алгебраическое (PDF). В начале этой статьи он говорит: Известно, что комбинаторная интерпретация лямбда-исчисления несовершенна, поскольку она не удовлетворяет правилу: при интерпретации не подразумевает (Barendregt, 1984).ξξξM=NM=NM =...
Сегодня я узнал, что алгоритм анализа отличается в зависимости от вычислительной модели. Это то, о чем я никогда не думал и не слышал. Пример, данный мне, который проиллюстрировал это далее, пользователем @chi был: Например, рассмотрим задачу: дано вернуть . В оперативной памяти это может быть...
Пусть → β→β\to_\beta - β-β\beta редукция в λ-λ\lambda вычислении. Определить β-β\beta расширение ← β←β\leftarrow_\beta по t ′ ← β t⟺t → β t ′t′←βt⟺t→βt′t'\leftarrow_\beta t \iff t\to_\beta t' . ← β←β\leftarrow_\beta является слитым ? Другими словами, имеем ли мы это для любого l , d , rl,d,rl,d,r ,...
Что такое анонимные (лямбда) функции? Каково формальное определение анонимной функции в функциональном языке программирования? Проще говоря, когда я программирую на схеме / lisp, я бы сказал, что анонимная (лямбда) функция - это функция, которая не связана с идентификатором. Это все, что вы можете...
Я не знаю, где еще задать этот вопрос, я надеюсь, что это хорошее место. Мне просто любопытно узнать, возможно ли создать генератор лямбда-исчисления; по сути, цикл, который при заданном бесконечном времени будет производить все возможные функции лямбда-исчисления. (как в виде строки). Так как...
Я работаю над небольшим компилятором лямбда-исчисления, который имеет работающую систему логического вывода типа Хиндли-Милнера, а теперь также поддерживает рекурсивный метод давайте (не в связанном коде), который, как я понимаю, должно быть достаточно для завершения Тьюринга . Проблема сейчас в...
Я понимаю, что церковная цифра выглядит как λ s . λ z . s (... n раз ...) . Это означает не что иное, как «функция примененная раз к функции ».сNcnc_nλ s . λ z, sλs.λz.s\lambda s. \lambda z. ss n zsZszs\;zsssNnnZzz Возможное определение функции следующее: . Глядя на тело, я понимаю логику функции....