- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Fri, 01 Jan 2010 23:47:15 +0100

Hello again,

On Nov 25, 2009, at 4:29 PM, Wolfgang Lux wrote:

*> just another case that shows that beta-reduction is also not valid
*

*> in general in a functional-logic language
*

Very true. I now realise that I was surprised by something else. Let

me nail down the observation differently.

I previously thought that `let x = a in b` can be replaced by b[a/x]

(meaning b where every free occurrence of x is replaced by a) if there

is at most one free occurrence of x in b. However, this is not true as

demonstrated by the following functions.

f1 = let x = 1?2 in \y -> x+y

f2 = \y -> (1?2) + y

Although f2 results from f1 by substituting the *unique* variable x,

f1 and f2 are not semantically equivalent. The context `twice _ 10`

(where _ denotes the hole) distinguishes them:

twice f x = f (f x)

test1 = twice f1 10

test2 = twice f2 10

test1 has 2 results, test2 has 4.

Inlining nondeterministic expressions under lambdas is invalid even if

the replaced variable occurs at most once.

Cheers,

Sebastian

Date: Fri, 01 Jan 2010 23:47:15 +0100

Hello again,

On Nov 25, 2009, at 4:29 PM, Wolfgang Lux wrote:

Very true. I now realise that I was surprised by something else. Let

me nail down the observation differently.

I previously thought that `let x = a in b` can be replaced by b[a/x]

(meaning b where every free occurrence of x is replaced by a) if there

is at most one free occurrence of x in b. However, this is not true as

demonstrated by the following functions.

f1 = let x = 1?2 in \y -> x+y

f2 = \y -> (1?2) + y

Although f2 results from f1 by substituting the *unique* variable x,

f1 and f2 are not semantically equivalent. The context `twice _ 10`

(where _ denotes the hole) distinguishes them:

twice f x = f (f x)

test1 = twice f1 10

test2 = twice f2 10

test1 has 2 results, test2 has 4.

Inlining nondeterministic expressions under lambdas is invalid even if

the replaced variable occurs at most once.

Cheers,

Sebastian

-- Underestimating the novelty of the future is a time-honored tradition. (D.G.) _______________________________________________ curry mailing list curry_at_lists.RWTH-Aachen.DE http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curryReceived on Sa Jan 02 2010 - 12:31:42 CET

*
This archive was generated by hypermail 2.3.0
: Sa Feb 24 2024 - 07:15:10 CET
*