Описание тега peano-numbers

Числа Пеано - это простой способ представления натуральных чисел с использованием только нулевого значения и функции-преемника.
3 ответа

Есть ли удобный способ для построения чисел Пеано большего уровня типа с использованием монопересекающихся?

В монопереходном пакете используются числа Пеано уровня типа для MinLen, Я могу построить их, используя цепочку Succs: toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int]) но это быстро выходит из-под контроля toMinLen [1,2,3] :: Maybe (MinLe…
14 фев '15 в 05:15
1 ответ

Преемник Арифметическая функция Prolog Mod

Как написать функцию mod/3 для арифметики-преемника (числа Пеано) в прологе?
17 окт '16 в 04:58
5 ответов

Преобразовать число Пеано s(N) в целое число в прологе

Я наткнулся на эту оценку натуральных чисел логических чисел в учебнике, и это доставляло мне некоторую головную боль: natural_number(0). natural_number(s(N)) :- natural_number(N). Правило примерно гласит, что: если N является 0 это естественно, есл…
2 ответа

Как проверить числа Пеано

Я прохожу курс " Принципы функционального программирования" в Scala на Coursera. Вот пример реализации чисел Пеано, который выглядит так: abstract class Nat { def isZero: Boolean def predecessor: Nat def successor: Nat = new Succ(this) def +(that: N…
15 май '17 в 12:35
2 ответа

Хаскелл Пеано Числа

Я пытаюсь написать функцию toPeano :: Int -> Nat toPeano n = который превращает целое число в его число Пеано. У меня есть данные: data Nat = Zero | Succ Nat deriving Show Например, toPeano 0 = Zero toPeano 1 = Succ Zero toPeano 2 = Succ (Succ Ze…
06 окт '11 в 02:02
1 ответ

Пеано цифры в Русте

Я хотел написать простую реализацию чисел Пеано в Rust, и, похоже, мне удалось заставить работать основы: use self::Peano::*; use std::ops::Add; #[derive(Debug, PartialEq)] enum Peano { Zero, Succ(Box<Peano>) } impl Add for Peano { type Output…
03 сен '16 в 17:19
1 ответ

Преобразование целых чисел в числа Пеано с использованием системы типов

Это продолжение вопроса, который я задал почти два года назад. Я все еще экспериментирую с системой типов, чтобы написать небольшую библиотеку линейной алгебры, в которой размеры векторов / матриц / тензоров кодируются с использованием системы типов…
07 янв '13 в 09:25
7 ответов

Пианино (Пеано) номера?

Я слушал подкаст Стива Йегге (№29, около 21:29), и в какой-то части они говорили о том, "как определить, умный ли человек, с которым вы разговариваете", и сказали, что это один из способов. должен был говорить о "вещах умных людей" (я перефразирую),…
08 дек '08 в 15:43
1 ответ

Что такое определение типа для определения Nat в бесформенном?

Это определение Nat в упаковке shapeless: trait Nat { type N <: Nat } case class Succ[P <: Nat]() extends Nat { type N = Succ[P] } class _0 extends Nat with Serializable { type N = _0 } Каковы type декларации для? После удаления мне кажется, ч…
22 окт '15 в 13:14
1 ответ

Инъективность наследника натуральных чисел в Coq

Меня немного смущает, является ли инъективность функции-преемника, определенной на натуральных числах, Coq такое аксиома? Согласно аксиомам Википедии / Пеано, это аксиома (7). Когда я смотрю на страницу руководства Coq.Init.Peano, я вижу следующее: …
16 янв '19 в 09:58
1 ответ

Реализация числа Пеано в Coq

Я изучал основы программного обеспечения, чтобы изучить Coq, и застрял в Numbers. В этом определении типа Inductive nat : Type := | O : nat | S : nat -> nat. Как O становится 0 когда мы используем его в определении Definition pred (n : nat) : nat…
23 май '17 в 14:59
1 ответ

Невозможно создать последовательность Ints в Kotlin через функцию succesor. Говорит "Ошибка вывода типа"

Я пытаюсь создать поток / последовательность натуральных чисел из числа 0 и функции-преемника S через функцию generateSequence. Вот что у меня есть: package core fun sequenceOfNumbers(): Sequence<Int> { return generateSequence(0){x -> S(x)}…
21 янв '18 в 19:00
0 ответов

Дополнение к числам Пеано на уровне типа

Я определил типы для чисел Пеано class Plus (n :: T) (m :: T) (r :: T) | r n -> m instance Plus 'Zero m m instance Plus n m r => Plus ('Succ n) m ('Succ r) Теперь у меня есть два ограничения Plus a b c а также Plus c d e, Как я могу определить…
23 май '18 в 08:21
1 ответ

Есть ли в этом учебнике ошибка об арифметике Пеано?

Я столкнулся с этим сомнением в открытом вводном курсе по интро-логике, предложенном Stanford Uni. В разделе 9.4 этого учебника здесь: http://logic.stanford.edu/intrologic/secondary/notes/chapter_09.html Это говорит: Аксиомы, показанные здесь, опред…
22 июл '16 в 02:23
1 ответ

Попытка написать предикат высоты дерева - мне нужны натуральные числа в стиле Пеано?

В качестве основного упражнения на Прологе я поставил перед собой задачу написать предикат высоты двоичного дерева, который будет работать вперед и назад, то есть, помимо определения высоты известного двоичного дерева, он должен быть в состоянии най…
3 ответа

Эта Java-программа преобразует натуральное число в теоретико-множественное кодирование, используя итерацию. Запросить помощь / стратегии для рекурсивного решения?

Я пытаюсь лучше понять теорию множеств ZFC, в частности, как компьютерная программа может моделировать аксиому бесконечности, чтобы "построить" натуральные числа. Типичные символы, которые я видел, использовали для построения натуральных чисел: "{",…
1 ответ

Числа Хаскеля Пеано и лень в умножении

Я начал изучать Haskell недавно, и прямо сейчас в моем классе мы создали класс чисел Peano и создали его в классе типов Num. Во время лекции мой профессор утверждал, что в зависимости от того, рассматривали ли вы функцию преемника как S x = x + 1 ил…
2 ответа

Доказательство теорем Кок: простой закон дробей в арифметике Пеано

Я изучаю coq и пытаюсь доказать равенства в арифметике пеано. Я застрял на простом законе дробей. Мы знаем, что (n + m) / 2 = n / 2 + m / 2 из начальной школы. В арифметике пеано это справедливо, только если n и m четны (потому что тогда деление дае…
30 ноя '19 в 23:41
1 ответ

вычислить s-число для натурального числа с помощью Prolog

Я новичок в Prolog и все еще привыкаю к ​​его логике. У меня есть задача создать функции, которые превращают натуральное число в "S-число" и наоборот. Итак, номер 0 будет 0.Номер 1 был быs(0).Номер 2 был быs(s(0)).И так далее. nat(0). nat(s(0)):- na…
10 апр '20 в 20:55
1 ответ

Предикаты Times, Quotient и Remainder в Прологе

Как я могу сделать следующее. Мне нужно было определить предикат shownumber (X,N), что верно, когда символ X соответствует натуральному числу N. Например, shownumber(s(zero),1)правда. Хорошо, теперь у меня есть предикат: shownumber(zero, 0). shownum…
01 июн '20 в 15:55