Stack Overflow
Stack Overflow

Questions tagged [peano-numbers]

Peano numbers are a simple way of representing the natural numbers using only a zero value and a successor function.

Peano numbers are a simple way of representing the natural numbers using only a zero value and a successor function. In it is easy to create a type of Peano number values, but since unary representation is inefficient, they are more often used to do type arithmetic due to their simplicity.

25 questions
7
votes
2 answers

Haskell Peano Numbers

I'm trying to write a function toPeano :: Int -> Nat toPeano n = that turns an Integer into its Peano Number. I have the data: data Nat = Zero | Succ Nat deriving Show For example, toPeano 0 = Zero toPeano 1 = Succ Zero toPeano 2 = Succ…
Shabu
  • 645
  • 4
  • 11
  • 17
6
votes
1 answer

Injectivity of successor of natural numbers in Coq

I am a little confused whether the injectivity of the successor function defined on natural numbers in Coq is an axiom? According to Wikipedia/Peano axioms, it is an axiom (7). When I look at Coq.Init.Peano manual page I see the…
OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
6
votes
1 answer

Converting integers to peano numbers using the type system

This is a follow-up of a question I asked almost two years ago. I am still experimenting with the type system to write a small linear algebra library where the dimensions of vectors/matrices/tensors is encoded using the type system (with Peano…
paradigmatic
  • 40,153
  • 18
  • 88
  • 147
4
votes
1 answer

How can I add two numbers using type constraints?

Here I encode addition by 1 as wrapping in a tuple type and subtraction by 1 as extracting the second element of the tuple type: type zero = unit * unit type 'a minus1 = 'snd constraint 'a = unit * 'snd type 'a plus1 = unit * 'a So far, the…
Max Heiber
  • 14,346
  • 12
  • 59
  • 97
4
votes
1 answer

Peano numbers in Rust

I wanted to write a simple implementation of Peano numbers in Rust and it seems that I managed to get the basics working: use self::Peano::*; use std::ops::Add; #[derive(Debug, PartialEq)] enum Peano { Zero, Succ(Box) } impl Add for…
ljedrz
  • 20,316
  • 4
  • 69
  • 97
4
votes
3 answers

Is there a convenient way to construct larger type level Peano numbers using mono-traversable?

The mono-traversable package uses type level Peano numbers for MinLen. I can construct them using chained Succs: toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int]) but this quickly gets out of hand: toMinLen [1,2,3] :: Maybe (MinLen (Succ…
MaxGabriel
  • 7,617
  • 4
  • 35
  • 82
3
votes
1 answer

Why Peano numbers in OCaml not working due to scope error?

I have the following peano number written with GADTs: type z = Z of z type 'a s = Z | S of 'a type _ t = Z : z t | S : 'n t -> 'n s t module T = struct type nonrec 'a t = 'a t end type 'a nat = 'a t type e = T : 'n nat -> e The following…
David 天宇 Wong
  • 3,724
  • 4
  • 35
  • 47
2
votes
1 answer

Prolog program to enumerate all possible solution over a countable set

I am writing a prolog program with can perform Peano arithmetics. I have standard definitions for natural numbers. nat(n). nat(s(N)) :- nat(N). Because I want to enumerate all possible relation of addition between natural numbers, I defined an…
liutaowen
  • 23
  • 2
2
votes
2 answers

Tail recursive addition of Peano numbers in F# using accumulators

At Uni we were given a challenge of creating a tail recursive addition of Peano numbers using an accumulator. We aren't allowed to use any library function or other functions that we have created, but we are allowed to 'hide' the accumulator in an…
LVOL
  • 29
  • 3
2
votes
1 answer

Can't create sequence of Ints in Kotlin through succesor function. Says "Type Inference failed"

I'm trying to create a stream/sequence of natural numbers from the number 0 and a successor function S, through the generateSequence function. Here's what I've got: package core fun sequenceOfNumbers(): Sequence { return…
user1661303
  • 539
  • 1
  • 7
  • 20
2
votes
7 answers

Piano (Peano) numbers?

I was listening to the steve yegge podcast (#29, around 21:29), and in part of it, they were talking about "how to tell if the person you're talking to is smart", and they said that one way was to talk about "smart people things" (I'm paraphrasing),…
dwmackie
2
votes
1 answer

Haskell Peano Numbers and Laziness in Multiplication

I started learning Haskell recently and in my class right now, we have constructed a Peano number class and instanced it in the Num typeclass. During lecture, my professor claimed that depending on whether you viewed the successor function as S x =…
Frank Wang
  • 181
  • 9
1
vote
1 answer

Natural Number Game goals completed with error (invalid begin-end expression, comma expected)

When playing the Natural Number Game (in Lean), in Advanced Multiplication World Level 2/4, I used the following code. The last three lines seem to cause trouble. cases a at h, left, refl, cases b at h, right, refl, left, rw mul_succ at h, rw…
Benjamin Wang
  • 226
  • 1
  • 9
1
vote
2 answers

Coq theorem proving: Simple fraction law in peano arithmetic

I am learning coq and am trying to prove equalities in peano arithmetic. I got stuck on a simple fraction law. We know that (n + m) / 2 = n / 2 + m / 2 from primary school. In peano arithmetic this does only hold if n and m are even (because then…
Falco Winkler
  • 1,082
  • 1
  • 18
  • 24
1
vote
1 answer

Peano number implementation in Coq

I was going through the book Software foundations to learn Coq and I got stuck on Numbers. In this Type definition Inductive nat : Type := | O : nat | S : nat -> nat. How does O becomes 0 when we use it in definition of Definition pred (n :…
Totoro
  • 1,307
  • 12
  • 18
1
2