how to evaluate/simplify a term contain if-then-else's?
Subject: how to evaluate/simplify a term contain if-then-else's?
From: Robert Dodier
Date: Tue, 13 Apr 2010 09:25:54 -0600
On 4/13/10, Oliver Kullmann <O.Kullmann at swansea.ac.uk> wrote:
> exactf_tau_arithprog(k,n) :=
> if n < k then 0
> elseif k=1 then n
> elseif k=2 then n-1
> elseif n <= 2*k-1 and evenp(k) then
> if n = 2*k-1 then 2 else 1
> elseif n <= 2*k and oddp(k) then
> if n = 2*k then 2 else 1
> else unknown$
>
> which yields
>
> exactf_tau_arithprog(1,n);
> if n < 1 then 0 elseif 1 = 1 then n elseif 1 = 2 then n-1 elseif n <= 1 and
> evenp(1)
> then (if n = 1 then 2 else 1) elseif n <= 2 and oddp(1) then (if
> n = 2 then 2 else 1)
> else unknown
>
> however this should yield "if n < 1 then 0 else n" --- how to achieve this?
Since the first condition doesn't evaluate to true or false,
none of the following conditions are evaluated either.
This is probably justified by the desideratum of preventing
side effects.
There is an experimental share package boolsimp which
attempts some half-hearted simplifications of conditional
expressions:
load (boolsimp);
exactf_tau_arithprog (1, n);
=> if n < 1 then 0 else n
I guess that's enough in this case. boolsimp is pretty simple-minded,
and possibly out of date; don't expect much from it. There are some
comments in boolsimp.lisp if you care to read them.
Incidentally, part of the problem is that 1=1 and 1=2 don't simplify
to true and false, respectively. There has been some discussion
about simplifying boolean expressions; I don't remember where we
ended up last time the topic arose.
best
Robert Dodier