Equational reasoning consists in manipulating definitions in referentially transparent code as if they were mathematical equations.
Questions tagged [equational-reasoning]
22 questions
45
votes
1 answer
If return a = return b then does a=b?
Can you prove that if return a = return b then a=b? When I use =, I mean in the laws and proofs sense, not the Eq class sense.
Every monad that I know seems to satisfy this, and I can't think of a valid monad that wouldn't (Const a is a functor and…
PyRulez
- 10,513
- 10
- 42
- 87
14
votes
3 answers
Is it possible to use church encodings without breaking equational reasoning?
Mind this program:
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)
type List h = forall t . (h -> t -> t) -> t -> t
sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0
toList :: [a] -> List a
toList = \ list cons nil -> foldr cons…
MaiaVictor
- 51,090
- 44
- 144
- 286
13
votes
3 answers
Haskell: Equation Expander 1+(1+(1+(1+(…))))=∞
Does there exist a equation expander for Haskell?
Something like foldr.com: 1+(1+(1+(1+(…))))=∞
I am new to Haskell I am having trouble understanding why certain equations are more preferable than others. I think it would help if I could see the…
user295190
7
votes
0 answers
Problems with equational proofs and interface resolution in Idris
I'm trying to model Agda style equational reasoning proofs for Setoids (types with an equivalence relation). My setup is as follows:
infix 1 :=:
interface Equality a where
(:=:) : a -> a -> Type
interface Equality a => VerifiedEquality a where …
Rodrigo Ribeiro
- 3,198
- 1
- 18
- 26
6
votes
2 answers
Haskell - How to transform map sum (map (x:) xss) to map (x+) (map sum xss)
Reading "Thinking Functionally with Haskell" I came across a part of a program calculation that required that map sum (map (x:) xss) be rewritten as map (x+) (map sum xss)
Intuitively I know that it makes sense ...
if you have some lists that you…
Barry Rogerson
- 598
- 2
- 15
6
votes
3 answers
Am I using sound equational reasoning about a definition of filter in terms of foldr?
well, this is the definition of the filter function using foldr:
myFilter p xs = foldr step [] xs
where step x ys | p x = x : ys
| otherwise = ys
so for example let's say i have this function:
myFilter odd…
Azriel
- 407
- 2
- 9
3
votes
1 answer
Why is chain of equational reasoning failing to meet trivially solvable constraints?
The following Agda code:
module test where
open import Data.Float
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
postulate
distrib : {m a b : Float} → m * (a + b) ≡…
dbanas
- 1,707
- 14
- 24
3
votes
1 answer
Keeping track of "state" when writing equality proofs that are long chains of transitively linked steps
I was writing the following proof in Idris:
n : Nat
n = S (k + k)
lemma: n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
lemma = sym $
rewrite plusZeroRightNeutral ((k * n) + k) in
rewrite plusAssociative ((k * n) + k) 1 ((k * n)…
Cactus
- 27,075
- 9
- 69
- 149
3
votes
1 answer
To prove equality of two function definitions inductively
How do I do the induction to establish the statement moll n = doll n, with
moll 0 = 1 --(m.1)
moll n = moll ( n-1) + n --(m.2)
doll n = sol 0 n --(d.1)
where
sol acc 0 = acc…
letter
- 91
- 1
- 7
3
votes
1 answer
reduce(x+y, xs) and sum(xs) are not equivalent in python?
I would expect the two to mean the same, from a functional equational standpoint, however:
x = [1, 2, 3]
y = ['a', 'b', 'c']
reduce(lambda x, y: x + y, zip(x, y)) # works
sum(zip(x, y)) # fails
Why is sum failing here?
Henry Henrinson
- 5,203
- 7
- 44
- 76
3
votes
2 answers
Haskell - How to transform maximum (xs ++ map (x+) xs) to max (maximum xs) (x + maximum xs)
One of the excercises in "Thinking Functionally With Haskell" is about making a program more efficient using the fusion law. I am having some trouble trying to replicate the answer.
A part of the calculation requires that you transform maximum (xs…
Barry Rogerson
- 598
- 2
- 15
3
votes
3 answers
Understanding different foldr statments
I understand simple foldr statements like
foldr (+) 0 [1,2,3]
However, I'm having trouble with more complicated foldr statements, namely ones that take 2 parameters in the function, and with / and - computations. Could anyone explain the steps that…
p0ny
- 317
- 2
- 10
2
votes
1 answer
How to prove this Haskell code using equational reasoning
I found this exercise on equational reasoning and proofs in Haskell. The following code is given:
type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
deriving (Show)
--
-- Stack machine
--
exec :: Code -> Stack -> Stack
exec [ ] s = s
exec…
user4424299
2
votes
2 answers
Proof by induction with multiple lists
I am following the Functional Programming in Scala lecture on Coursera and at the end of the video 5.7, Martin Odersky asks to prove by induction the correctness of the following equation :
(xs ++ ys) map f = (xs map f) ++ (ys map f)
How to handle…
Gael
- 459
- 3
- 18
1
vote
1 answer
(sequence .) . flip fmap === forM?
Is (sequence .) . flip fmap the same as forM? I ask here because pointfree.io seems not to say the same...
Enlico
- 23,259
- 6
- 48
- 102