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 Fr Okt 27 2017 - 09:49:19 CEST