在勒柯克

在Haskell退状态单子，绑定的如下定义被接受：在勒柯克

type RState s a = s -> (a, s) 

bind :: RState s a -> (a -> RState s b) -> RState s b 
bind sf f = \s -> 
    let (a, s'') = sf s' 
     (b, s') = f a s 
    in (b, s'')

我怎样才能获得通过勒柯克接受了类似的定义？我的尝试是：

Definition RState (S A : Type) : Type := S -> A * S. 

Definition bind (S A B : Type) (sf : RState S A) (f : A -> RState S B) : RState S B := 
    fun s => 
    let (a, s'') := sf s' in 
    let (b, s') := f a s in 
    (b, s'').

但它失败，出现以下错误信息：

Error: The reference s' was not found in the current environment.

来源

2017-01-18 Bob

诀窍工作哈斯克尔因为'let'表达两个绑定相互递归。 IDK它如何在Coq中工作，但我猜是有某种'mutual'关键字？ –

您还需要使用良好的关系证明终止。我不确定这是否有可能在没有在bind中使用某种额外的（证明）参数（也许是特定的有用的关系）。 –

假设g :: s -> s。考虑

sf :: RState s s 
sf = get = \s -> (s, s) 

f :: s -> RState s s 
f = put . g = \a _ -> ((), g a)

我们得到：

bind sf f = \s -> 
    let (a, s'') = sf s' 
     (b, s') = f a s 
    in (b, s'') 
      = \s -> 
    let (a, s'') = (s', s') 
     (b, s') = ((), g a) 
    in (b, s'') 
      = \s -> 
    let (b, s') = ((), g s') 
    in (b, s') 
      = \s -> 
    let s' = g s' in ((), s')

这涉及到计算为g一个固定的点，这是一般不可能勒柯克由于缺乏可能终止。

正如David Young在上面提到的那样，如果像bind这样的东西在Coq中是可行的，那么必须用证明术语证明这个递归终止。这种增强是不平凡的。

来源

2017-01-19 08:47:23 chi

bind需要证明函数将实际返回。如果添加一个参数H，其类型取决于实际的sf,f和s值，则可以从该“已认证”的术语H中提取所需的(b, s'')对。

注意如何实际计算的sf和f功能具有在H建设来解释，对于特定sf，f和s。

（有可能是achieveing这个其他/更好的办法。希望别人可以添加到这个线程）。

Definition RState (S A : Type) : Type := S -> A * S. 

Section Bind. 
    Variables S A B:Type. 

    (* define a type that a proof should have *) 
    Definition sf_f_s_are_ok (sf : RState S A) (f : A -> RState S B) (s:S) := 
    {x | exists a s'' b s', x = (a, s'', b, s') /\ 
     (a, s'') = sf s' /\ (b, s') = f a s}. 

    (* bind just returns the values we were interested in *) 
    Definition bind sf f (s:S) (H : sf_f_s_are_ok sf f s) := 
    match H with exist _ (a, s'', b, s') _ => (b, s'') end. 

    (* make sure bind is ok *) 
    Lemma bind_is_ok: forall sf f s H b s'', 
     bind sf f s H = (b, s'') -> exists a s', (a,s'') = sf s' /\ (b,s') = f a s. 
    Proof. 
    intros sf f s [[[[a s''0] b0] s'] [a0 [b1 [s'0 [s''1 [Ha [Hb Hc]]]]]]] b s'' H0. 
    simpl in H0; generalize H0 Ha Hb Hc; do 4 inversion 1; subst; eauto. 
    Qed. 
End Bind.

来源

2017-01-19 23:34:22 larsr

回答

相关问题