[Haskell-cafe] Peano axioms
Hi,
Below are two attempts to define Peano arithmetic in Haskell.
The first attempt, Peano1, consists of just a signature in the class
with the axioms in the instance. In the second attempt, Peano2, I am
trying to move the axioms into the class. The reason is, I want to put
as much specification as possible into the class. Then I would like to
include properties in the class such as commutativity something like:
infixl 5 `com`
com :: Int - Int - Int
x `com` y = (x + y)
commutative com a b = (a `com` b) == (b `com` a)
I seem to be able to include just one default equation the Peano2 attempt.
Any ideas?
I have looked at
http://www.haskell.org/haskellwiki/Peano_numbers
Regards,
Pat
-- Attempt 1
-- In this attempt the axioms are in the instance and things seem OK
module Peano1 where
infixl 6 `eq`
infixl 5 `plus`
class Peano1 n where
suc :: n - n
eq :: n - n - Bool
plus :: n - n - n
data Nat = One | Suc Nat deriving Show
instance Peano1 Nat where
suc = Suc
One `eq` One = True
(Suc m) `eq` (Suc n) = m `eq` n
_`eq`_ = False
m `plus` One = Suc m
m `plus` (Suc n) = Suc (m `plus` n)
-- Evaluation *Peano1 Suc(One) `plus` ( Suc (One))
-- Attempt 2
-- In this attempt the axioms are in the class and things are not OK.
module Peano2 where
infixl 6 `eq`
infixl 5 `plus`
class Peano2 n where
one :: n
eq :: n - n - Bool
plus :: n - n - n
suc :: n - n
suc a = a `plus` one
{-
I cannot add the remaining default axioms
one `eq` one = True
(suc m) `eq` (suc n) = m `eq` n
(suc a) `eq` (suc b) = a `eq` b
_`eq`_ = False
-}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Peano axioms
The problem is that you are using 'suc' as if it is a constructor: ((suc m)
`eq` (suc n) = m `eq` n)
You'll have to change it to something else, and it will probably require
adding an unpacking function to your class and it will probably be messy.
I'd suggest you make use of the Eq typeclass and defined the Eq instances
separately:
class (Eq n) = Peano2 n where
one :: n
plus :: n - n - n
suc :: n - n
suc a = a `plus` one
- Job
On Thu, Sep 17, 2009 at 2:36 PM, pat browne patrick.bro...@comp.dit.iewrote:
Hi,
Below are two attempts to define Peano arithmetic in Haskell.
The first attempt, Peano1, consists of just a signature in the class
with the axioms in the instance. In the second attempt, Peano2, I am
trying to move the axioms into the class. The reason is, I want to put
as much specification as possible into the class. Then I would like to
include properties in the class such as commutativity something like:
infixl 5 `com`
com :: Int - Int - Int
x `com` y = (x + y)
commutative com a b = (a `com` b) == (b `com` a)
I seem to be able to include just one default equation the Peano2 attempt.
Any ideas?
I have looked at
http://www.haskell.org/haskellwiki/Peano_numbers
Regards,
Pat
-- Attempt 1
-- In this attempt the axioms are in the instance and things seem OK
module Peano1 where
infixl 6 `eq`
infixl 5 `plus`
class Peano1 n where
suc :: n - n
eq :: n - n - Bool
plus :: n - n - n
data Nat = One | Suc Nat deriving Show
instance Peano1 Nat where
suc = Suc
One `eq` One = True
(Suc m) `eq` (Suc n) = m `eq` n
_`eq`_ = False
m `plus` One = Suc m
m `plus` (Suc n) = Suc (m `plus` n)
-- Evaluation *Peano1 Suc(One) `plus` ( Suc (One))
-- Attempt 2
-- In this attempt the axioms are in the class and things are not OK.
module Peano2 where
infixl 6 `eq`
infixl 5 `plus`
class Peano2 n where
one :: n
eq :: n - n - Bool
plus :: n - n - n
suc :: n - n
suc a = a `plus` one
{-
I cannot add the remaining default axioms
one `eq` one = True
(suc m) `eq` (suc n) = m `eq` n
(suc a) `eq` (suc b) = a `eq` b
_`eq`_ = False
-}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Peano axioms
I don't understand your goal. Isn't Peano arithmetic summarized in Haskell as: data Peano = Zero | Succ Peano deriving Eq This corresponds to a first-order logic over a signature that has equality, a constant symbol 0, and a one-place successor function symbol S. Function symbols such as and + can be introduced as defined function symbols that do not add substantive information to the theory. The only axioms you want are the ones for equality. John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
