Wie Mathematik Induktion auf 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) 

Frage implementieren:

Beweisen Sie, dass, wenn basecase p und indstep p, dann forAllNat p

Was ich nicht verstehe, ist, dass, wenn basecase p und indstep p, so forAllNat pTrue sein sollte, Na sicher.

Ich denke, basecase p sagt, dass P(0) wahr ist, und indstep p sagt, dass P(Succ n) die P(n+1) ist, ist wahr Und wir müssen beweisen, P(n) wahr ist. Bin ich richtig? Irgendwelche Vorschläge, wie man das macht?

Answer 1

Wie Benjamin Hodgson angibt, kann man das in Haskell nicht ganz beweisen. Sie können jedoch eine Aussage mit etwas stärkeren Voraussetzungen nachweisen. Ich werde auch die unnötige Komplexität von Bool ignorieren.

{-# 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

Das kann man innerhalb von Haskell nicht beweisen. (Turns out you can.) Die Sprache ist nicht abhängig genug eingegeben. Es ist eine Programmiersprache, kein Proofassistent. Ich denke, die Aufgabe erwartet wahrscheinlich, dass Sie es auf Papier und Bleistift beweisen.

Sie können es in Agda tun, obwohl.

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) 

(Sie erkennen können induction-principle als Nat ‚s foldr zu sein.)

Sie in der Lage sein, etwas ein bisschen wie diese zu erhalten, wenn TypeInType landet in GHC 8. Es wird zwar nicht schön sein.