Код неси. Нахуй мне в твой текст вчитываться?
Аксиомы Пеано, судя по Гуглу, это что-то связанное с натуральными числами.
ОП хочет понять как вычислять арифметику? Ну наверное через аккумулятор, как в ассемблере (все языки - синтаксический сахар над ассемблером).
ОП хочет понять как вычислять арифметику? Ну наверное через аккумулятор, как в ассемблере (все языки - синтаксический сахар над ассемблером).
Вряд ли ты найдёшь тут единомышленников. Большинству похуй на этот теоретический дроч, все хотят зарабатывать деньги.
Хотя есть пруверов тред
> все языки - синтаксический сахар над ассемблером
Не юзай понятия, значение которых не понимаешь, плез.
> ОП хочет понять как вычислять арифметику?
Нет. Я и так могу построить аксиомы Пеано. Особенно просто и понятно они строятся в системах перезаписи термов/строк. Для того, чтобы построить аксиомы Пеано достаточно самого языка. Т.е их можно легко строить на чистом лямбда исчислении (числа Чёрча), или на логических предикатах.
Тут такое дело, смотри, не все так просто.
Суть в том что
Все языки программирования - это синтаксический сахар над ассемблером.
Теперь можешь что-нибудь сказать по делу и не сказать ничего.
> Все языки программирования - это синтаксический сахар над ассемблером.
Это абсолютно некорректное утверждение. Дальше что?
> Все языки программирования - это синтаксический сахар над ассемблером.
Начнем с того, что компилятор ≠ язык программирования. Так что говорить, что все языки являются синтаксическим сахаром над ассемблером не корректно.
>Все языки программирования - это синтаксический сахар над ассемблером.
Байтоговнарики не могут мыслить абстрактно. Тезис Чёрча-Тьюринга гарантирует, что программа на любом нормальном языке может быть переведена в байтодрисню и наоборот.
запили свои аксиомы на каком-нить языке - самому гуглить лень)
На Pure lang:
// Сложение
nonfix Z;
x + Z = x;
Z + x = x;
S(x) + y = x + S(y);
// Умножение
infix 2300 •;
x • S(Z) = x;
S(Z) • x = 0;
x • Z = 0;
Z • x = 0;
x • S(y) = x • y + x;
попробуй для начала переписать в префиксную форму всё подряд
5+4= -> = + 5 4
а как операция = будет работать и сможешь ли ты прувать теоремы в форте - я хз
Так как я это сделаю, если функция сложения обязательно бинарная? Я конечно знаю, что в лямбда исчислении тоже существуют только унарные функции (арность фун-ии задается через каррирование), но в лямбда кроме того и переменные есть. А как задать очевидно бинарную функцию в языке где есть только угарные функции задаваемых в поинт-фри стайле я не в курсе.
если я правильно понял - через стек, куда складируются все излишки значений
2 + 5 4 -> 4 5 попадают в стек, + подбирает 2 верхних значения, кладёт результат в стек и 2 вслед за ним, берёт 2 значения и т.д.
Звучит как-то не функционально.
есть немного - такой стек похож на не функциональное глобальное состояние, но всё же функция зависит только от входных параметров - пусть и подаются они весьма странно
Пиздец ИТТ дегенератов, в упор не понимающих о чем вообще речь.
> неебическая скорость
Это смотря с чем сравнивать. Все каноничные реализации именно медленные что пиздец, сольют JVM.
> как построить в конкатенативных языках аксимы Пеано?
Если речь про конкатенативные языке в общем, то точно так же, как и в лямбда-исчислении, только комбинаторы накидывать справа, а не слева, т.к. у тебя композиция перевернута. Конкретно forth для такого не предназначен, это тупо интерпретатор над словарем и одним или несколькими стеками, как в калькуляторе. Ты можешь попытаться эмулировать арифметику через [ и ], но это хак, т.к. все равно будешь юзать встроенные функции, только в "compile" time.
> неебическая скорость
Это смотря с чем сравнивать. Все каноничные реализации именно медленные что пиздец, сольют JVM.
> как построить в конкатенативных языках аксимы Пеано?
Если речь про конкатенативные языке в общем, то точно так же, как и в лямбда-исчислении, только комбинаторы накидывать справа, а не слева, т.к. у тебя композиция перевернута. Конкретно forth для такого не предназначен, это тупо интерпретатор над словарем и одним или несколькими стеками, как в калькуляторе. Ты можешь попытаться эмулировать арифметику через [ и ], но это хак, т.к. все равно будешь юзать встроенные функции, только в "compile" time.
> Если речь про конкатенативные языке в общем, то точно так же, как и в лямбда-исчислении
Да проблема в том, что в лямбда исчислении благодаря аргументам и каррированию я могу выражать функции любой арности (к примеру бинарную функцию [+]). А как это сделать в языке где нет явных аргументов и все функции могут быть только унарные/нульарные.
>как построить в конкатенативных языках аксимы Пеано?
Для логического вывода (т.е. для формальной системы) требуется подходящая типизация выражений. Много ты знаешь конкатенативных языков со строгой типизацией? Но в принципе это возможно.
>Особенно просто и понятно они строятся в системах перезаписи термов/строк.
Ну так операционная семантика конкатенативных языков и есть в точности система переписывания.
Короче, раскури по-нормальному комбинаторную логику и не мучайся. Нумералы Чёрча в CL спокойно так определяются (в IKS-базисе):
n ≡ (SB)n(KI)
>А как это сделать в языке где нет явных аргументов и все функции могут быть только унарные/нульарные.
Ну что ты несёшь-то? Да и не стоит поднимать этот тупой вопрос. Уже обсуждали http://arhivach.net/thread/366436/ Лучше по-нормальному в вопросе разберись.
> Для логического вывода (т.е. для формальной системы) требуется подходящая типизация выражений.
На самом деле нет. Для написания аксиом Пеано достаточно:
- Паттерн-метчинга
- Лямбды
А можно обойтись и одной только лямбдой.
Пролог, к примеру, вообще "бестиповый", однако логический вывод имеет, и вообще для него собственно и создавался.
> Ну так операционная семантика конкатенативных языков и есть в точности система переписывания.
Любую возможную формальную систему можно выразить с помощью системы переписывания очевидным образом. Однако сами конкатенативные языки не являются системами переписывания, они только изоморфичны им.
> Ну что ты несёшь-то?
Ну смотри, либо в конкатенативных языках используем комбинаторы (= встроенные функции), либо не сможем человеческим образом написать функцию принимающую больше одного значения.
Под "значениями" я подразумеваю не аргументы, а фактическую арность функции. К примеру, в JS:
let plus = ([a, b]) => a + b
Формально у функции plus один аргумент (функция принимает один array-like объект), однако фактически у этой функции два аргумента.
>А можно обойтись и одной только лямбдой.
Не знаю как в Прологе. В TRS'ах аксиомы как и все предикаты записываются в типах. Термы населяющие тип являются доказательством предиката, выраженного типом. Конструкторы типов не выражаются через другие термы, а просто по определению населяют тип - 'доказывают' аксиому.
Ты всё-таки решил поднять этот вопрос? Я про это говорить не стану.
>комбинаторы (= встроенные функции)
У тебя какое-то своё определение комбинатора? В TRS'ах комбинатор - терм без свободных переменных. Т.О. в конкатенативных языках все слова (функции) являются комбинаторами. Но это не значит, что они (как вычисления) не могут иметь несколько параметров. Самый простой пример - посмотри на стековый эффект факторовского слова + ( x y -- z ) - тут явно указана арность параметризации. Ты с базой-то разберись.
Разве JS кокатенативный?
> В TRS'ах аксиомы как и все предикаты записываются в типах
Не обязательно. Даже скажу больше, зачастую это не так. Взгляни на Pure-lang, или на TRS'ы в лиспе.
Просто вместо определения типов используют обощенный тип данных, к которому применяется паттерн-метчинг. Систему типов можно использовать, чтобы не допускать существование определённых термов в других термах, чтобы заранее оповестить программиста что он долбоеб, и что он допустил ошибку. Но это так, удобства ради.
> Разве JS кокатенативный?
Нет, я просто привел пример функции, что формально является унарной, но не фактически. Просто в вики указывается, что все функции в конкатенативных языках являются унарными, что не возможно.
Изначально, вопрос был таков: как определить такой конкатенативный язык, что не использует встроенные функции/комбинаторы? TRS к примеру нет необходимости в каких-то встроенных комбинаторах. Достаточно декларации правила.
Можно ли реализовать подобную мощь в конкатенативных языках? Дело в том, что конкенативные языки на порядок проще в реализации, чем аппликативные языки, и тем более TRS. И я хочу, чтобы этот язык был самодостаточным, и не использовал встроенные функции определенные в компиляторе (кроме IO-эффектов, с ним всё понятно, просто скинем их выполнение на компилятор, как Haskell делает).
Ну вот имеем мы список из слов. Каждое слово - функция, а сам список является композицией этих функций.
Если в у слова нет определения, то считается, что функция возвращает само это слово. Т.е число 5 это функция, которая возвращает число 5.
Слово это просто последовательность непроблельных символов. Окей, тут всё понятно.
Вопрос: как построить в конкатенативных языках аксимы Пеано? Естественно, без использования библиотечных/встроенных функций. Что-то не догоняю никак.