Simple function comparison

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|

Simple function comparison

Stephen Renehan
Hi,

I'm looking to do a comparison between 2 simple functions to see if
they are equivalent but I appear to be running into some problems if
anyone can help.

The two functions I want to compare are f (g a) and g (f a).

I have f defined and g defined as
 f :: a -> a
 f = undefined

g :: a -> a.
g =  undefined

The compiler was complaining about the type signature lacking a
binding so added undefined to get around the error. I understand that
I must be missing something very basic as they look incomparable in
this form. Any suggestions of what changes I should make such a
comparison practical?

Many thanks,

Stephen

--


This email originated from DIT. If you received this email in error, please
delete it from your system. Please note that if you are not the named
addressee, disclosing, copying, distributing or taking any action based on
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to
Grangegorman <http://www.dit.ie/grangegorman>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Francesco Ariis
On Wed, Nov 25, 2015 at 11:39:15AM +0000, Stephen Renehan wrote:

> Hi,
>
> I'm looking to do a comparison between 2 simple functions to see if
> they are equivalent but I appear to be running into some problems if
> anyone can help.
>
> The two functions I want to compare are f (g a) and g (f a).
>
> I have f defined and g defined as
>  f :: a -> a
>  f = undefined
>
> g :: a -> a.
> g =  undefined
>
> The compiler was complaining about the type signature lacking a
> binding so added undefined to get around the error. I understand that
> I must be missing something very basic as they look incomparable in
> this form. Any suggestions of what changes I should make such a
> comparison practical?

Hello Stephen,
    I don't think there is a way to /prove/ f (g a) == g (f a) if their
domain is not finite inside Haskell (you could do it with pen and
paper).

If you have two functions and a finite domain you can do, say:

    -- function function domain
    compfun :: (Eq a) => (a -> a) -> (a -> a) -> [a] -> Bool
    compfun f g d = and $ map (\x -> (f . g) x == (g . f) x) d

    λ> compfun (+1) (+17) [1..10]
    True
    λ> compfun (*5) (+17) [1..10]
    False

Of course this is a toy example, use a proper library (quickcheck, etc.)
if you are writing a real program.

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Stephen Renehan
Many thanks Franceso, I had thought as much as I was dealing with them
only abstractly. Appreciate the quick reply and thanks for the help.

On 25 November 2015 at 14:20, Francesco Ariis <[hidden email]> wrote:

> On Wed, Nov 25, 2015 at 11:39:15AM +0000, Stephen Renehan wrote:
>> Hi,
>>
>> I'm looking to do a comparison between 2 simple functions to see if
>> they are equivalent but I appear to be running into some problems if
>> anyone can help.
>>
>> The two functions I want to compare are f (g a) and g (f a).
>>
>> I have f defined and g defined as
>>  f :: a -> a
>>  f = undefined
>>
>> g :: a -> a.
>> g =  undefined
>>
>> The compiler was complaining about the type signature lacking a
>> binding so added undefined to get around the error. I understand that
>> I must be missing something very basic as they look incomparable in
>> this form. Any suggestions of what changes I should make such a
>> comparison practical?
>
> Hello Stephen,
>     I don't think there is a way to /prove/ f (g a) == g (f a) if their
> domain is not finite inside Haskell (you could do it with pen and
> paper).
>
> If you have two functions and a finite domain you can do, say:
>
>     -- function function domain
>     compfun :: (Eq a) => (a -> a) -> (a -> a) -> [a] -> Bool
>     compfun f g d = and $ map (\x -> (f . g) x == (g . f) x) d
>
>     λ> compfun (+1) (+17) [1..10]
>     True
>     λ> compfun (*5) (+17) [1..10]
>     False
>
> Of course this is a toy example, use a proper library (quickcheck, etc.)
> if you are writing a real program.
>
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

--


This email originated from DIT. If you received this email in error, please
delete it from your system. Please note that if you are not the named
addressee, disclosing, copying, distributing or taking any action based on
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to
Grangegorman <http://www.dit.ie/grangegorman>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

MJ Williams
In reply to this post by Francesco Ariis
[snip]

>I don't think there is a way to /prove/ f (g a) == g (f a) if their
>domain is not finite inside Haskell (you could do it with pen and paper).
[snip]
         Just out of interest, could you demonstrate the proof
without a finite domain?

Sincerely, Matthew

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Francesco Ariis
On Wed, Nov 25, 2015 at 03:48:08PM +0000, MJ Williams wrote:
> [snip]
>
> >I don't think there is a way to /prove/ f (g a) == g (f a) if their domain
> >is not finite inside Haskell (you could do it with pen and paper).
> [snip]
>         Just out of interest, could you demonstrate the proof without a
> finite domain?
>
> Sincerely, Matthew

Say we have:

    f(x) = x + 1
    g(x) = x + 7

Then we can substitute:

    f(g(x))
    f(x+7)
    (x+7) + 1
    x+8

and

    g(f(x))
    g(x+1)
    (x+1) + 7
    x+8

which shows f(g(x)) = g(f(x))

For anything more, my lawyer suggested I say: I have discovered a
truly marvellous proof for it, but the margin of this email is to
narrow to contain it. :P

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Stephen Renehan
In reply to this post by MJ Williams
Hi Matthew,

Was just about to reply that I only have the process written in long
hand from the video that I enclose but I see Francesco beat me to it
with a more concise explanation. Thanks again Francesco :)

https://www.youtube.com/watch?v=ZhuHCtR3xq8


On 25 November 2015 at 15:48, MJ Williams <[hidden email]> wrote:

> [snip]
>
>> I don't think there is a way to /prove/ f (g a) == g (f a) if their domain
>> is not finite inside Haskell (you could do it with pen and paper).
>
> [snip]
>         Just out of interest, could you demonstrate the proof without a
> finite domain?
>
> Sincerely, Matthew
>
>
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

--


This email originated from DIT. If you received this email in error, please
delete it from your system. Please note that if you are not the named
addressee, disclosing, copying, distributing or taking any action based on
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to
Grangegorman <http://www.dit.ie/grangegorman>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

emacstheviking
Awesome video, I watched it about ten times in a row and so many pennies dropped.

On 25 November 2015 at 16:35, Stephen Renehan <[hidden email]> wrote:
Hi Matthew,

Was just about to reply that I only have the process written in long
hand from the video that I enclose but I see Francesco beat me to it
with a more concise explanation. Thanks again Francesco :)

https://www.youtube.com/watch?v=ZhuHCtR3xq8


On 25 November 2015 at 15:48, MJ Williams <[hidden email]> wrote:
> [snip]
>
>> I don't think there is a way to /prove/ f (g a) == g (f a) if their domain
>> is not finite inside Haskell (you could do it with pen and paper).
>
> [snip]
>         Just out of interest, could you demonstrate the proof without a
> finite domain?
>
> Sincerely, Matthew
>
>
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

--


This email originated from DIT. If you received this email in error, please
delete it from your system. Please note that if you are not the named
addressee, disclosing, copying, distributing or taking any action based on
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to
Grangegorman <http://www.dit.ie/grangegorman>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Henk-Jan van Tuyl
In reply to this post by Stephen Renehan
On Wed, 25 Nov 2015 12:39:15 +0100, Stephen Renehan <[hidden email]>  
wrote:

> Hi,
>
> I'm looking to do a comparison between 2 simple functions to see if
> they are equivalent but I appear to be running into some problems if
> anyone can help.
>
> The two functions I want to compare are f (g a) and g (f a).
>
> I have f defined and g defined as
>  f :: a -> a
>  f = undefined
>
> g :: a -> a.
> g =  undefined

As you can not say anything about the type of input or output (except that  
they are equal), the only normally terminating function possible is 'id'.  
So, if you don't want to use 'undefined' or 'error', f and g are equal.

Regards,
Henk-Jan van Tuyl


--
Folding@home
What if you could share your unused computer power to help find a cure? In  
just 5 minutes you can join the world's biggest networked computer and get  
us closer sooner. Watch the video.
http://folding.stanford.edu/


http://Van.Tuyl.eu/
http://members.chello.nl/hjgtuyl/tourdemonad.html
Haskell programming
--
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

MJ Williams
All right, how about this for a proof:

Let f x = x + 1
let g x = x + 2

if f ( g a )
then f ( a + 2 ) .............. (g)
then ( a + 2 ) + 1 ............ (f)
...
then a + 3 .................... (+)
therefore f ( g a ) <-> a + 3

if g ( f a )
then g ( a + 1 ) .............. (f)
then ( a + 1 ) + 2 ............ (g)
...
then a + 3 .................... (+)
therefore g ( f a ) <-> a + 3

therefore f ( g a ) = g ( f a ) (transitivity)

Feel free to take it apart and smash it to bits. Seriously, any
feedback welcome.

Cheers, Matthew


On 25/11/2015, Henk-Jan van Tuyl <[hidden email]> wrote:

> On Wed, 25 Nov 2015 12:39:15 +0100, Stephen Renehan <[hidden email]>
> wrote:
>
>> Hi,
>>
>> I'm looking to do a comparison between 2 simple functions to see if
>> they are equivalent but I appear to be running into some problems if
>> anyone can help.
>>
>> The two functions I want to compare are f (g a) and g (f a).
>>
>> I have f defined and g defined as
>>  f :: a -> a
>>  f = undefined
>>
>> g :: a -> a.
>> g =  undefined
>
> As you can not say anything about the type of input or output (except that
>
> they are equal), the only normally terminating function possible is 'id'.
> So, if you don't want to use 'undefined' or 'error', f and g are equal.
>
> Regards,
> Henk-Jan van Tuyl
>
>
> --
> Folding@home
> What if you could share your unused computer power to help find a cure? In
>
> just 5 minutes you can join the world's biggest networked computer and get
>
> us closer sooner. Watch the video.
> http://folding.stanford.edu/
>
>
> http://Van.Tuyl.eu/
> http://members.chello.nl/hjgtuyl/tourdemonad.html
> Haskell programming
> --
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

MJ Williams
All right, a revised version:

Let f x = x + 1
let g x = x + 2

f ( g a )
= f ( a + 2 ) ................... (g)
= ( a + 2 ) + 1 ................. (f)
...
= a + 3 ......................... (+)
therefore f ( g a ) <-> a + 3 ... (transitivity)

g ( f a )
= g ( a + 1 ) ................... (f)
= ( a + 1 ) + 2 ................. (g)
...
= a + 3 ......................... (+)
therefore g ( f a ) <-> a + 3 ... (transitivity)

therefore f ( g a ) = g ( f a ) . (transitivity)


On 26/11/2015, MJ Williams <[hidden email]> wrote:

> All right, how about this for a proof:
>
> Let f x = x + 1
> let g x = x + 2
>
> if f ( g a )
> then f ( a + 2 ) .............. (g)
> then ( a + 2 ) + 1 ............ (f)
> ...
> then a + 3 .................... (+)
> therefore f ( g a ) <-> a + 3
>
> if g ( f a )
> then g ( a + 1 ) .............. (f)
> then ( a + 1 ) + 2 ............ (g)
> ...
> then a + 3 .................... (+)
> therefore g ( f a ) <-> a + 3
>
> therefore f ( g a ) = g ( f a ) (transitivity)
>
> Feel free to take it apart and smash it to bits. Seriously, any
> feedback welcome.
>
> Cheers, Matthew
>
>
> On 25/11/2015, Henk-Jan van Tuyl <[hidden email]> wrote:
>> On Wed, 25 Nov 2015 12:39:15 +0100, Stephen Renehan <[hidden email]>
>> wrote:
>>
>>> Hi,
>>>
>>> I'm looking to do a comparison between 2 simple functions to see if
>>> they are equivalent but I appear to be running into some problems if
>>> anyone can help.
>>>
>>> The two functions I want to compare are f (g a) and g (f a).
>>>
>>> I have f defined and g defined as
>>>  f :: a -> a
>>>  f = undefined
>>>
>>> g :: a -> a.
>>> g =  undefined
>>
>> As you can not say anything about the type of input or output (except
>> that
>>
>> they are equal), the only normally terminating function possible is 'id'.
>> So, if you don't want to use 'undefined' or 'error', f and g are equal.
>>
>> Regards,
>> Henk-Jan van Tuyl
>>
>>
>> --
>> Folding@home
>> What if you could share your unused computer power to help find a cure?
>> In
>>
>> just 5 minutes you can join the world's biggest networked computer and
>> get
>>
>> us closer sooner. Watch the video.
>> http://folding.stanford.edu/
>>
>>
>> http://Van.Tuyl.eu/
>> http://members.chello.nl/hjgtuyl/tourdemonad.html
>> Haskell programming
>> --
>> _______________________________________________
>> Beginners mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

Kim-Ee Yeoh
Administrator

On Thu, Nov 26, 2015 at 6:20 PM, MJ Williams <[hidden email]> wrote:


therefore f ( g a ) = g ( f a ) . (transitivity)

If you're interested in getting a firm grasp of airtight proofs -- with a view toward Haskell (and Agda and Idris) mastery -- you might want to pick and choose your way through the web-based proof exercises here:

https://www.coursera.org/course/intrologic

This is a course firmly in the American analytic philosophy tradition, so Logic here is Symbolic Logic. Bonus: the course keeps AI and Machine Learning applications in the backdrop.

It's unfortunate that it's some kind of well-kept secret.

Those who don't need it -- because they've obtained the knowledge elsewhere -- won't know about it. And those who do want that knowledge also won't know about it.

Did I mention the exercises are web-based? Yes, you get instantaneous feedback on whether you've got a correct proof or not.

-- Kim-Ee

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Simple function comparison

MJ Williams
That's great, thanks.
Matt

At 11:53 26/11/2015, you wrote:

On Thu, Nov 26, 2015 at 6:20 PM, MJ Williams <[hidden email]> wrote:


therefore f ( g a ) = g ( f a ) . (transitivity)


If you're interested in getting a firm grasp of airtight proofs -- with a view toward Haskell (and Agda and Idris) mastery -- you might want to pick and choose your way through the web-based proof exercises here:

https://www.coursera.org/course/intrologic

This is a course firmly in the American analytic philosophy tradition, so Logic here is Symbolic Logic. Bonus: the course keeps AI and Machine Learning applications in the backdrop.

It's unfortunate that it's some kind of well-kept secret.

Those who don't need it -- because they've obtained the knowledge elsewhere -- won't know about it. And those who do want that knowledge also won't know about it.

Did I mention the exercises are web-based? Yes, you get instantaneous feedback on whether you've got a correct proof or not.

-- Kim-Ee
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners