programming-by-simulations

From: Sebastian Hanowski <sebastian_hanowski_at_gmx.de>
Date: Fri, 27 Oct 2017 07:37:09 +0200




Hi


 When I began to exploit narrowing for hiding constructors in infinite list=
s I
needed to be able to unify them lazily.

Earlier definitions I gave just looked too involved. Only recently I found a
neater way to do this.



        (~=) = zipWith (=:=)


        (x:xs) `given` (p:ps) | p = x : (xs `given` ps)


        fibs | head xs =:= 1
             & head (tail xs) =:= 1 = xs `given` (tail (tail xs) ~==
 zipWith (+) xs (tail xs))

             where xs free



 This also carries over to giving your program as a specification in terms =
of
the "interface" of infinite lists in message passing style.



        infixr 0 `and`

        xs `and` ys = xs `given` (xs ~= ys) =



        proj `is` img = emb img where emb (proj preimg) = preimg


        fibs = head `is` 1
               `and`
               (head . tail) `is` 1
               `and`
               (tail . tail) `is` zipWith (+) fibs (tail fibs)



 Monads where introduced to computer science to give semantics to effectful
programs. On paper. Only later they were used as a device to structure
effectful programs.

Can we do the same to bisimulations?

Instead of proving properties of our programs, why not express them directl=
y in
terms of the desired properties?


Have a nice weekend,

Sebastian
_______________________________________________
curry mailing list
curry_at_lists.rwth-aachen.de
https://mailman.rwth-aachen.de/mailman/listinfo/curry
Received on Fri Oct 27 2017 - 09:49:19 CEST

This archive was generated by hypermail 2.3.0 : Fri Sep 20 2019 - 07:15:09 CEST