Как реализовать индукцию по математике на Haskell

Question

data Nat = Zero | Succ Nat 
type Predicate = (Nat -> Bool) 

-- forAllNat p = (p n) for every finite defined n :: Nat 

implies :: Bool -> Bool -> Bool 
implies p q = (not p) || q 

basecase :: Predicate -> Bool 
basecase p = p Zero 

jump :: Predicate -> Predicate 
jump p n = implies (p n) (p (Succ n)) 

indstep :: Predicate -> Bool 
indstep p = forallnat (jump p) 

Вопрос:

Докажите, что если basecase p и indstep p, то forAllNat p

То, что я не понимаю, что если basecase p и indstep p, так forAllNat p должны быть True, конечно.

Я думаю basecase p говорит, что P(0) верно, и indstep p говорит, что P(Succ n) что P(n+1) истинно И мы должны доказать P(n) верно. Я прав? Любое предложение о том, как это сделать?

Answer 1

Как указывает Бенджамин Ходжсон, вы не можете доказать это в Haskell. Однако вы можете доказать утверждение с несколько более сильными предпосылками. Я также проигнорирую ненужную сложность Bool.

{-# LANGUAGE GADTs, KindSignatures, DataKinds, RankNTypes, ScopedTypeVariables #-} 

data Nat = Z | S Nat 

data Natty :: Nat -> * where 
    Zy :: Natty 'Z 
    Sy :: Natty n -> Natty ('S n) 

type Base (p :: Nat -> *) = p 'Z 
type Step (p :: Nat -> *) = forall (n :: Nat) . p n -> p ('S n) 

induction :: forall (p :: Nat -> *) (n :: Nat) . 
      Base p -> Step p -> Natty n -> p n 
induction b _ Zy = b 
induction b s (Sy n) = s (induction b s n) 

Answer 2

Вы не можете доказать это в Haskell. (Turns out you can.) Язык не зависит от типизации. Это язык программирования, а не помощник доказательства. Я думаю, что назначение, вероятно, ожидает, что вы докажете это на карандаше и бумаге.

Вы можете сделать это в Агда.

data Nat : Set where 
    zero : Nat 
    suc : Nat -> Nat 

Pred : Set -> Set1 
Pred A = A -> Set 

Universal : {A : Set} -> Pred A -> Set 
Universal {A} P = (x : A) -> P x 

Base : Pred Nat -> Set 
Base P = P zero 
Step : Pred Nat -> Set 
Step P = (n : Nat) -> P n -> P (suc n) 

induction-principle : (P : Pred Nat) -> Base P -> Step P -> Universal P 
induction-principle P b s zero = b 
induction-principle P b s (suc n) = s n (induction-principle P b s n) 

(Вы можете узнать induction-principle как Nat «s foldr.)

Вы можете быть в состоянии получить что-то немного, как это, когда TypeInType земли в GHC 8. Это будет не очень, хотя.