# How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

I have a recursively defined function in Coq whose arguments in the recursive invocations are surely decreasing, but Coq cannot understand this fact since they are not subterms of the function's argument. This is a snippet exemplifying the situation:

Inductive expression : Type :=
| Get : expression -> identifier -> expression
| IfThenElse : expression -> expression -> expression -> expression
...
end.

Fixpoint eval (M : memory) (e : expression) : value :=
match e with
| Get (IfThenElse cond e1 e2) var_name => ... eval M (Get e1 var_name) ... eval M (Get e2 var_name) ...
...
end.


While the recursive invocations of eval have not a subterm of e as their argument, it is easy to find a decreasing measure for the e argument of eval, e.g., the maximum nesting level of subterms in it. I read that Program Fixpoint allows to specify a measure, but I found the section on Program in the reference manual too obscure, nor I was able to find a tutorial or examples that may suit a beginner as I am. Can anyone provide me some references, or a quick explanation, or perhaps suggest an alternative approach that does not imply restructuring the inductive type definitions?

• It is difficult to suggest a solution without knowing more about memory and value. If you design them correctly, then eval ought ot be structurally recursive. Perhaps you can show a real example that is closer to what you are trying to do. Feb 2 at 16:09
• What is Get e x supposed to mean, intuitively? Feb 2 at 16:18
• It is supposed to mean: get the value of field named x from object e. Feb 2 at 17:58
• And how is memory supposed to work? Feb 2 at 17:59
• it is a map from references to objects, which are maps from field names to values. But the structure of the memory should be immaterial, since there is no structural, or any other kind of, recursion over memory. Feb 2 at 18:01

It turns out that using Program Fixpoint is much easier than I thought:

From Coq Require Import Program.Wf.

...

Inductive height (e : expression) : nat
match e with
| Get e1 => height e1 + 1
| IfThenElse e1 e2 e3 => (Nat.max (height e1) (Nat.max (height e2) (height e3))) + 1
...
end.

Program Fixpoint eval (M : memory) (e : expression) {measure (height e)} : value := ...


A more worked-out example, similar in spirit to a subset of the specification I am working on, is available at https://gist.github.com/pietrobraione/22cad84ed2d84da57e2fd500ee14fe02. The next point would be, as far as I could understand, proving the obligations that are generated.

Maybe you could have a fixpoint dedicated to Get to avoid rebuilding terms.

Fixpoint eval_get (M : memory) (e : expression)  (var_name : identifier) : value :=
match e with
| IfThenElse cond e1 e2 var => ... eval_get M e1 var_name ... eval_get M e2 var_name ...
...
end.


and then

Fixpoint eval (M : memory) (e : expression) : value :=
match e with
| Get e var_name => eval_get e1 var_name
end.

• Technically, yes. Practically, I don't want to break my spec in parts just for the sake of making it palatable to Coq and make it less readable, or making it too different from the corresponding declarative definition of eval. So I would avoid this solution. Feb 2 at 17:53
• There is a declarative definition of eval? May we see it. Feb 2 at 18:06
• Well, it is really more complicated than that: eval is just a way to minimize the problem I am working on, that is a symbolic interpreter for a small object-oriented language. I am afraid that there is no easy way to simplify the spec, but I will try. Feb 2 at 18:30
• But once you have defined your eval function in bits and pieces. You can always get back the readable form by proving the theorem eval M e = match e ....
– Lolo
Feb 2 at 18:44

I find your definition of eval a bit odd. You are implementing something like large-step evaluation, which should be defined by structural recursion on the expression being evaluated.

I would expect your pseudo-code to look like this:

Inductive expression : Type :=
| Get : expression -> identifier -> expression
| IfThenElse : expression -> expression -> expression -> expression
...
end.

Fixpoint eval (M : memory) (e : expression) : value :=
match e with
| IfThenElse cond e1 e2 =>
match eval M cond with
| ValueFalse => eval M e2
| ValueTrue => eval M e1
| _ => ValueRuntimeError
end

| Get e var_name =>
match eval M e with
| ValueObject obj => get_field obj var_name
| _ => ValueRuntimeError

...

end.


Above get_field is a primitive function (not part of your source language) that extracts a field from an object, represented as a value.

• No. Getting with one kind of expression has a radically different semantics than getting with another kind of expression (e.g., Get (Reference n) field_name vs. Get (IfThenElse cond e1 e2) field_name). Feb 2 at 18:11
• I do not understand what "No" refers to, you will have to be a bit more verbose. And your pseudocode indicates that all expressions are evaluated to a single value type. If you want this conversation to be more productive, please amend your question and provide some real information. You are not doing us any favors by omitting details. Feb 2 at 18:20
• But my main point is independent of all of this, because it is: large-step semantics should be structurally recursive (as in "structural operational semantics"). Feb 2 at 18:22
• At gist.github.com/pietrobraione/22cad84ed2d84da57e2fd500ee14fe02 you can find a more detailed example that is closer to the specification I am writing. It should provide sufficient details to get an idea of what I am trying to do without going too deeply. If this is still not enough, I cannot see any solution other than passing you the full specification. Feb 2 at 20:09
• So it looks like your problems would go away if you had objects as values. Then eval can be structurally recursive. Feb 3 at 6:55