Skip to content

Instantly share code, notes, and snippets.

@jeffque

jeffque/peano.hs

Created August 29, 2024 01:40
Show Gist options
  • Save jeffque/04fcd2d19030d8461edd10f0c3a35543 to your computer and use it in GitHub Desktop.
Save jeffque/04fcd2d19030d8461edd10f0c3a35543 to your computer and use it in GitHub Desktop.
Download ZIP
Aritmética de Peano
Raw
peano.hs
data Nat = Zero | Suc Nat
inc :: Nat -> Nat
inc x = Suc x
showNat :: Nat -> String
showNat Zero = "Zero"
showNat (Suc v) = "Suc " ++ (show v)
type BinNat = (Nat -> Nat -> Nat)
addNat :: BinNat
addNat Zero x = x
addNat x Zero = x
addNat x (Suc y) = addNat (Suc x) y
multNat :: BinNat
multNat Zero x = Zero
multNat x Zero = Zero
multNat (Suc x) y = addNat y (multNat x y)
ltNat :: Nat -> Nat -> Bool
ltNat Zero Zero = False
ltNat Zero (Suc _) = True
ltNat (Suc _) Zero = False
ltNat (Suc x) (Suc y) = ltNat x y
diffNat :: BinNat
diffNat x Zero = x
diffNat Zero _ = Zero
diffNat (Suc x) (Suc y) = diffNat x y
modNat :: BinNat
modNat x Zero = Zero
modNat x y = if (ltNat x y) then x else modNat (diffNat x y) y
divNat :: BinNat
divNat x Zero = Zero
divNat x y = if (ltNat x y) then Zero else Suc (divNat (diffNat x y) y)
ackPeter :: BinNat
ackPeter Zero n = inc n
ackPeter (Suc m) Zero = ackPeter m (Suc Zero)
ackPeter (Suc m) (Suc n) = ackPeter m (ackPeter (inc m) n)
instance Show Nat where
show = showNat
main :: IO ()
main = do
let dois = (inc (inc Zero))
let quatro = addNat dois dois
print dois
print quatro
print (ackPeter dois quatro)
--print (inc (inc Zero))
--print (multNat (inc (Suc Zero)) (inc (inc (inc Zero))))
--print (ltNat (inc (Suc Zero)) (inc (inc (inc Zero))))
--print (diffNat (multNat (inc (Suc Zero)) (inc (inc (inc Zero)))) (inc (inc (inc (inc Zero)))))
--print (modNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (inc (inc (Suc (Suc Zero)))) )
--print (divNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (inc (inc (Suc (Suc Zero)))) )
--print (divNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (Suc (Suc Zero)) )
--print (modNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (Suc (Suc Zero)) )
--print (ackPeter Zero Zero)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment