Re: [Haskell-cafe] Knowledge
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/Knowledge-tp14423007p14577605.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Knowledge
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Knowledge
On Dec 19, 2007 7:26 PM, jlw501 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Knowledge
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Knowledge
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 - I had to chuck that one in as a special case... it was argued it was redundant, but the behavior changes without it, try setting knowself to true, then allKnow [1,1] a truth ( equivalent in semantics to allKnow [1] a truth) should be true, but without that line it is false. Can anyone explain? and finally the important one (at least for those who are unfortunate enough to work in KM), some knowing it. 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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/Knowledge-tp14423007p14426329.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Knowledge
The main observation I've made it when playing with the values of knowing the self and perfect communication, nothing else becomes undefined if just perfect communication is true, it is still depended on knowing the self if you can have knowledge. Makes sense. jlw501 wrote: 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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- View this message in context: http://www.nabble.com/Knowledge-tp14423007p14426967.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
