[Agda] Ringsolver seems ok, but how to get NF?

[Nils Anders Danielsson]

On 2010-08-23 18:37, Christoph HERRMANN wrote:
> However, while function *works* typechecks, function *fails* does not
> although they only differ in the argument to the *normExp* function
> which computes a unique result *ConstrNorm* that differs only in its
> type, which is indexed by the normal form.

The result of "normalise m", where m is a neutral term, is
"normalise m". The ring-solver cannot magically turn m into an
object-language variable.

> Any ideas how to modify the program to make *fails*
> working for the given argument, but still fail
> for something semantically different such as "(cP 2) :+ m" ?

If you're working with open terms I think you will face difficulties.
Even if you're working with closed terms you will have problems with the
current definition of Normal, because normal forms contain proofs.
Example:

   normalise {n = 1} (con 1 :+ con 1) = (con 2 ∶ …) ↑ ∶ …

   normalise {n = 1} (con 2)          = con 2 ↑

If you need actual normal forms you can use a type such as the
following:

   data Normal : ℕ → Set r₁ where
     con   : (c : C.Carrier) → Normal 0
     _↑    : ∀ {n} (p : Normal n) → Normal (suc n)
     _*x+_ : ∀ {n} (p : Normal (suc n)) (c : Normal n) → Normal (suc n)

--
/NAD