2 
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

私が理解していないのは、 ifbasecase pと、もちろんindstep pそうforAllNat pあるべきだということです。True

私basecase pはそれP(0)が真実であると indstep p言い、P(Succ n)どちらが真実であると言い、それが真実であるかP(n+1)を証明する必要があると思いP(n)ます。私は正しいですか？これを行う方法について何か提案はありますか?

4

2 に答える 2

7

これを Haskell 内で証明することはできません。(できることがわかりました。 ) 言語は依存型付けが十分ではありません。これはプログラミング言語であり、証明アシスタントではありません。課題ではおそらく、紙と鉛筆で証明することが求められていると思います。

ただし、Agdaでそれを行うことができます。

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。foldr)

GHC 8に着陸すると、このようなものを少し取得できる可能性がTypeInTypeあります。きれいではありません。

于 2016-04-07T17:03:54.920 に答える