Knowledge

[jlw501]

I'm new to functional programming and Haskell and I love its expressive ability! I've been trying to formalize the following function for time. Given people and a piece of information, can all people know the same thing? Anyway, this is just a bit of fun... but can anyone help me reduce it or talk about strictness and junk as I'd like to make a blog on it?

contains :: Eq a => [a]->a->Bool
contains [] e = False
contains (x:xs) e = if x==e then True else contains xs e
perfectcomm :: Bool
perfectcomm = undefined
knowself :: Bool
knowself = undefined
allKnow :: Eq a => [a]->String->Bool
allKnow _ "" = True
allKnow [] k = False
allKnow (x:[]) k = knowself
allKnow (x:xs) k =
   comm x xs k && allKnow xs k
   where
      comm p [] k = False
      comm p ps k = if contains ps p then knowself
                       else perfectcomm

[Luke Palmer-2]

On Dec 19, 2007 7:26 PM, jlw501 <jlw501@...> wrote:
>
> I'm new to functional programming and Haskell and I love its expressive
> ability! I've been trying to formalize the following function for time.
> Given people and a piece of information, can all people know the same thing?
> Anyway, this is just a bit of fun... but can anyone help me reduce it or
> talk about strictness and junk as I'd like to make a blog on it?

This looks like an encoding of some philosophical problem or something.  I
don't really follow.  I'll comment anyway.

> contains :: Eq a => [a]->a->Bool
> contains [] e = False
> contains (x:xs) e = if x==e then True else contains xs e

contains = flip elem

> perfectcomm :: Bool
> perfectcomm = undefined
> knowself :: Bool
> knowself = undefined

Why are these undefined?

> allKnow :: Eq a => [a]->String->Bool
> allKnow _ "" = True
> allKnow [] k = False
> allKnow (x:[]) k = knowself
> allKnow (x:xs) k =
>    comm x xs k && allKnow xs k
>    where
>       comm p [] k = False

This case will never be reached, because you match against (x:[]) first.

>       comm p ps k = if contains ps p then knowself
>                        else perfectcomm

And I don't understand the logic here. :-p

Luke
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Neil Mitchell]

Hi

> > contains :: Eq a => [a]->a->Bool
> > contains [] e = False
> > contains (x:xs) e = if x==e then True else contains xs e
>
> contains = flip elem

And even if not using the elem function, the expression:

if x==e then True else contains xs e

can be written as:

x==e || contains xs e

Thanks

Neil
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[jlw501]

Just to clarify, this is a little gag almost. It just demonstrates the problem of understanding knowledge as discussed by philosophers. perfectcomm is undefined as it is unknown if you can perfectly pass on your intention to another person. Likewise, it is unknown if you can express your subconscious mind in reason to yourself, hence knowself being undefined. The function then just slots these in on the cases of:

no one knowing it,
some knowing nothing,
no one knowing nothing,
one knowing it,
and finally the important one (at least for those who are unfortunate enough to work in KM), some knowing it.

Kudos for spotting the  redundant line, you are right, sorry I though you meant the allKnow (x:[]) was redundant.

Sorry, if I've messed with your heads, it's just I've been into Haskell for a month and though I'd join (what seems to be) the forum and post something quirky.

Luke Palmer-2 wrote:

On Dec 19, 2007 7:26 PM, jlw501 <[e-mail]> wrote:
>
> I'm new to functional programming and Haskell and I love its expressive
> ability! I've been trying to formalize the following function for time.
> Given people and a piece of information, can all people know the same thing?
> Anyway, this is just a bit of fun... but can anyone help me reduce it or
> talk about strictness and junk as I'd like to make a blog on it?

This looks like an encoding of some philosophical problem or something.  I
don't really follow.  I'll comment anyway.

> contains :: Eq a => [a]->a->Bool
> contains [] e = False
> contains (x:xs) e = if x==e then True else contains xs e

contains = flip elem

> perfectcomm :: Bool
> perfectcomm = undefined
> knowself :: Bool
> knowself = undefined

Why are these undefined?

> allKnow :: Eq a => [a]->String->Bool
> allKnow _ "" = True
> allKnow [] k = False
> allKnow (x:[]) k = knowself
> allKnow (x:xs) k =
>    comm x xs k && allKnow xs k
>    where
>       comm p [] k = False

This case will never be reached, because you match against (x:[]) first.

>       comm p ps k = if contains ps p then knowself
>                        else perfectcomm

And I don't understand the logic here. :-p

Luke
_______________________________________________
Haskell-Cafe mailing list
[e-mail]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[jlw501]

The main observation I've made is when playing with the values of knowing the self and perfect communication, nothing else becomes undefined if just perfect communication becomes defined, it is still dependent on knowing the self if you can have knowledge. Makes sense. One tick on the verification checklist.



Just to clarify, this is a little gag almost. It just demonstrates the problem of understanding knowledge as discussed by philosophers. perfectcomm is undefined as it is unknown if you can perfectly pass on your intention to another person. Likewise, it is unknown if you can express your subconscious mind in reason to yourself, hence knowself being undefined. The function then just slots these in on the cases of:

no one knowing it,
some knowing nothing,
no one knowing nothing,
one knowing it,
and finally the important one (at least for those who are unfortunate enough to work in KM), some knowing it.

Kudos for spotting the  redundant line, you are right, sorry I though you meant the allKnow (x:[]) was redundant.

Sorry, if I've messed with your heads, it's just I've been into Haskell for a month and though I'd join (what seems to be) the forum and post something quirky.

Luke Palmer-2 wrote:

On Dec 19, 2007 7:26 PM, jlw501 <[e-mail]> wrote:
>
> I'm new to functional programming and Haskell and I love its expressive
> ability! I've been trying to formalize the following function for time.
> Given people and a piece of information, can all people know the same thing?
> Anyway, this is just a bit of fun... but can anyone help me reduce it or
> talk about strictness and junk as I'd like to make a blog on it?

This looks like an encoding of some philosophical problem or something.  I
don't really follow.  I'll comment anyway.

> contains :: Eq a => [a]->a->Bool
> contains [] e = False
> contains (x:xs) e = if x==e then True else contains xs e

contains = flip elem

> perfectcomm :: Bool
> perfectcomm = undefined
> knowself :: Bool
> knowself = undefined

Why are these undefined?

> allKnow :: Eq a => [a]->String->Bool
> allKnow _ "" = True
> allKnow [] k = False
> allKnow (x:[]) k = knowself
> allKnow (x:xs) k =
>    comm x xs k && allKnow xs k
>    where
>       comm p [] k = False

This case will never be reached, because you match against (x:[]) first.

>       comm p ps k = if contains ps p then knowself
>                        else perfectcomm

And I don't understand the logic here. :-p

Luke
_______________________________________________
Haskell-Cafe mailing list
[e-mail]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Tillmann Rendel]

jlw501 wrote:
> I'm new to functional programming and Haskell and I love its expressive
> ability! I've been trying to formalize the following function for time.
> Given people and a piece of information, can all people know the same thing?
> Anyway, this is just a bit of fun... but can anyone help me reduce it or
> talk about strictness and junk as I'd like to make a blog on it?

I don't think your representation of unknown information is reasonable.
Haskell is not lazy enough to make it work out:

   Prelude> True || undefined
   True

   Prelude> undefined || True
   *** Exception: Prelude.undefined

 From a logic perspective, unknown || true == true || unknown == true.
But this behaviour is impossible to implement in Haskell with unknown =
undefined, because you don't know in advance wich argument you should
inspect first. if you choose the undefined one, you will loop forever
without knowing the other argument would have been true.

In theoretical computer science, you would use a growing resource bound
to simulate the parallel evaluation of the two arguments. Maybe you can
use multithreading to implement the same trick in Haskell, but it
remains a trick.

So what can you do instead? I would encode the idea of unknown
information using an algebraic data type:

     data Modal a = Known a | Unknown deriving Show

We can express knowing that something is true as (Known True), not
knowing anything as (Unknown) and knowing something as (Known
undefined). The advantage of this aproach is that we can define our
operations as strict or nonstrict as we want by pattern matching on the
Modal constructors.

     (&&&) :: Modal Bool -> Modal Bool -> Modal Bool
     Known True  &&& Known True  = Known True
     Known False &&& _           = Known False
     _           &&& Known False = Known False
     _           &&& _           = Unknown

     (|||) :: Modal Bool -> Modal Bool -> Modal Bool
     Known False ||| Known False = Known False
     Known True  ||| _           = Known True
     _           ||| Known True  = Known True
     _           ||| _           = Unknown

     not' :: Modal Bool -> Modal Bool
     not' (Known True) = Known False
     not' (Known False) = Known True
     not' Unknown = Unknown

By strictness, I'm not talking about Haskell strictness, but about Modal
strictness, that is:

     A function (f :: Modal a -> Modal b) is Modal strict
     if and only if f Unknown = Unknown

A nice property of modal strictness is that we can test for it. given a
total function f, we can use

     isModalStrict :: (Modal a -> Modal b) -> Bool
     isModalStrict f = case f Unknown of
         Unknown -> True
         _ -> False

to so wether it is strict. The results are as expected:

   *Truth> isModalStrict not'
   True

   *Truth> isModalStrict (Known True |||)
   False

   *Truth> isModalStrict (Known True &&&)
   True

   *Truth> isModalStrict (&&& Known False)
   False

Let's compare the last case to the representation unknown = undefined:

   *Truth> (&& False) undefined
   *** Exception: Prelude.undefined

As expected, (&& False) is Haskell strict, but (&&& Known False) not
Modal strict.

I don't know if this will help you, in the end you may find that Haskell
is a programming language, not a theorem prover. But at least for me, it
seems better to encode information explicitly instead of using undefined
to encode something.

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[jlw501]

Good point.
By fold/unfold transformation you get the following:

contains = flip elem [Eureka]
=
contains xs e = flip elem xs e [Expose data structures]
=
contains [] e = False
contains (x:xs) e = flip elem (x:xs) e [Instantiate]
=
contains [] e = False
contains (x:xs) e = elem e (x:[]) || flip elem xs e [Unfold flip one step]
=
contains [] e = False
contains (x:xs) e = elem e (x:[]) || contains xs e [Fold back to original defintion]
=
contains [] e = False
contains (x:xs) = e==x || contains xs e [Substitute]

Apparently, the fold/unfold transformation law will always yield an equally or more efficient computation. So this begs the question...

contains [] e = False
contains (x:xs) = e==x || contains xs e

OR

contains = flip elem

Neil Mitchell wrote:

Hi

> > contains :: Eq a => [a]->a->Bool
> > contains [] e = False
> > contains (x:xs) e = if x==e then True else contains xs e
>
> contains = flip elem

And even if not using the elem function, the expression:

if x==e then True else contains xs e

can be written as:

x==e || contains xs e

Thanks

Neil
_______________________________________________
Haskell-Cafe mailing list
[e-mail]
http://www.haskell.org/mailman/listinfo/haskell-cafe