		Search-engine friendly clone of the ACL2 documentation.

ACL2-programming-language

Evaluation

Evaluation.

The evaluation semantics of ACL2 is formalized here in terms of a succession of the evaluation states formalized by the fixtype eval-state. This is a small-step operational semantics, from which we could also define a big-step operational semantics (by composing the small steps).

A small-step semantics is more flexible than a big-step semantics, because it lets us talk about intermediate evaluation states, and not just the final states. This is particularly important to describe non-terminating executions. Also, we can easily derive a big-step semantics from a small-step one, but not vice versa.

There are different options for the granularity of the (small) steps. The granularity that we formalize here should be adequate, but it can be changed if needed or useful.

Subtopics

Step-from-trans: Evaluation step from a transitional state.
Call-primitive-function: Call a primitive function on some arguments.
Step-from-init: Evaluation step from the initial state.
Put-leftmost-nonconst: Replace the leftmost term in a list that is not a quoted constant with a quoted constant with the given value.
Exec-outcome: Fixtype of execution outcomes.
Stepn: Perform at most a given number of evaluation steps.
Step: Evaluation step from any state that is not final or error.
Terminatingp: Check if an evaluation state is terminating.
Get-leftmost-nonconst: Return the leftmost term in a list that is not a quoted constant.
Exec-call: Execute a call of a function on a list of arguments.
Step*: Attempt to exhaustively perform execution steps from a state.