Hi
Thanks for the interesting comments. Its looks like learning some of
the basics about System Fw is probably the way forward.
However GHC goes beyond Fw by adding
data types
letrec
This blows strong normalisation out of the water. (Assuming you have
reasonable rules
| To: Haskell Cafe
| Subject: [Haskell-cafe] Termination of substitution
|
| Hi
|
| I'm trying to show that a system of rules for manipulating Haskell
| expressions is terminating. The rules can be applied in any order, to
| any subexpression - and there is a problem if there is any possible
Hi
I'm trying to show that a system of rules for manipulating Haskell
expressions is terminating. The rules can be applied in any order, to
any subexpression - and there is a problem if there is any possible
infinite sequence.
The rule that is giving me particular problems is:
(\v - x) y =
On 3/12/08, Neil Mitchell [EMAIL PROTECTED] wrote:
However, I don't believe this expression is type safe in Haskell.
Using higher-order polymorphism:
f (x :: forall a. a - a) = x x
--
Taral [EMAIL PROTECTED]
Please let me know if there's any further trouble I can give you.
-- Unknown
On Wed, Mar 12, 2008 at 09:05:03PM +, Neil Mitchell wrote:
Hi
I'm trying to show that a system of rules for manipulating Haskell
expressions is terminating. The rules can be applied in any order, to
any subexpression - and there is a problem if there is any possible
infinite sequence.
On Wed, Mar 12, 2008 at 02:30:41PM -0700, Taral wrote:
On 3/12/08, Neil Mitchell [EMAIL PROTECTED] wrote:
However, I don't believe this expression is type safe in Haskell.
Using higher-order polymorphism:
f (x :: forall a. a - a) = x x
Interestingly, this doesn't work - f is a
