cicada-lang / mugda Goto Github PK

(1) Equivalent without type is wrong, because the meaning of equivalent is only determined for specific type.

(2) Ap has target & args instead of target & arg.

(3) Using Var & Ap as Value instead of defining a Neutral type.

Code:

(data Nat () ()
  [zero () Nat]
  [add1 ([prev Nat]) Nat])

(fn func (-> Nat Nat)
  [((zero)) zero]
  [((add1 zero)) zero]
  [((add1 (add1 x))) (func (add1 x))])

(func (add1 (add1 zero)))

The result of this code should be zero instead of (add1 zero).

The following definition of sub-to-zero
with an abstraction my-add1 over constructor add1
can not pass termination-check:

(data Nat () ()
  [zero () Nat]
  [add1 ([prev Nat]) Nat])

(fn my-add1 (-> Nat Nat)
  [(x) (add1 x)])

(fn sub-to-zero (-> Nat Nat)
  [((zero)) zero]
  [((add1 (zero))) zero]
  [((add1 (add1 x))) (sub-to-zero (my-add1 x))])

test: https://github.com/cicada-lang/mugda/blob/master/tests/termination/sub-to-zero-indirect-add1.error.mu

https://en.wikipedia.org/wiki/Three-valued_logic