Lispex 2.0 specification · not released · Tested product not run · Examples not run
# Evaluation and bindings
Evaluation order, lexical scope, immutable bindings, and recursion.
Canonical: /v2.0/en/docs/language/evaluation
Document revision: 2.0-draft-1. Content locale: en. Translation: current.
- language: `lispex`
- languageVersion: `2.0`
## Scope
This chapter covers evaluation order, lexical scope, and immutable bindings. It also covers duplicate definitions, recursive procedures, and tail calls.
## Evaluation order
Evaluation computes values by following the program. A first failure ends the current evaluation path unless a permitted [guard](/v2.0/en/docs/language/conditions) handles it. Each later expression stays unevaluated until the preceding expression has completed.
The cases use symbolic finite limits large enough to reach the stated language result. Resource event order is defined in [Resources](/v2.0/en/docs/language/resources).
### Evaluate the operator and arguments in order
An application evaluates its operator first. It then evaluates every argument from left to right. After those evaluations complete, it checks that the operator is a procedure and that the argument count is accepted. The called operation checks its argument domains in the specified order. The first failure takes precedence over every later check.
**Why**
Pure expressions can still fail. A fixed order lets every product report the same first failure for the same request.
Claim: `lispex.claim.v2.evaluation.application-order` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "procedure-application",
"operands": "source-order",
"evaluation": "strict"
},
"result": {
"kind": "ordered-application",
"sequence": [
"operator",
"arguments-left-to-right",
"callability",
"arity",
"operation-domain-checks",
"body"
],
"failureSelection": "first-reached-failure"
},
"pendingCases": [
"Additional cases must combine value count, callability, arity, domain checks, and resource reservations at the same call site.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### An operator failure comes first
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
((car '()) (cdr '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The operator produces the car domain failure before the argument is evaluated. Product invocation awaits its 2.0 adapter."
}
```
The cdr expression would also fail. The plan requires the car failure and no result datum.
### The left argument fails first
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ (car '()) (cdr '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The left argument produces the car domain failure before the right argument is evaluated. Product invocation awaits its 2.0 adapter."
}
```
Neither the second argument nor the addition can replace the first failure.
### An argument failure precedes callability
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(0 (car '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The argument produces the car domain failure before the operator is checked for callability. Product invocation awaits its 2.0 adapter."
}
```
The integer operator cannot be called. Its later callability failure does not replace the argument failure.
### An argument failure precedes arity
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
((lambda (x) x) 1 (car '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The second argument produces the car domain failure before the argument count is checked. Product invocation awaits its 2.0 adapter."
}
```
The procedure accepts one argument. The plan requires the earlier domain failure instead of an arity failure.
### Evaluate only the selected expressions
An if form has one test and two written branches. A cond form ends with one nonempty else clause. The [conditional grammar](/v2.0/en/docs/language/evaluation#lispex.grammar.v2.evaluation.conditionals) fixes these source forms. A conditional evaluates its test before the selected branch. Only #f is false in a test. Every other value is true, including the empty list and exact zero. A conditional does not evaluate an unselected branch. The selected branch forwards its complete internal result sequence. An author may explicitly return zero values with values. A missing branch never supplies an implicit result. The and and or forms evaluate operands from left to right and stop when the result is determined. A begin body evaluates its expressions in order and returns the values of its final expression.
**Why**
Selecting a branch must also select which failures and resource events can occur. Evaluating unused expressions would change the meaning of the rule.
Only #f is false.
Written alternatives make the result policy explicit for every conditional path. They preserve internal multiple values without inventing an unmatched result.
Claim: `lispex.claim.v2.evaluation.selected-expressions` · interaction · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "conditional-or-sequence",
"forms": [
"if",
"cond",
"and",
"or",
"begin"
]
},
"result": {
"kind": "selected-evaluation",
"conditionBeforeBranch": true,
"unselectedBranchEvaluated": false,
"sequenceOrder": "left-to-right",
"sequenceResult": "final-expression-values",
"truthTest": "only-false-is-false",
"ifOperandCount": 3,
"condFinalElse": "required-nonempty",
"implicitNoMatchResult": false,
"selectedResult": "zero-one-or-many-explicit-values"
},
"pendingCases": [
"Additional malformed forms, clause failures, value counts, and short circuit boundaries require cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
Cond tests run once in source order. Each test requires one value. Only #f selects the next clause. A selected test-only clause returns that test value. A selected body returns the values of its final expression. An arrow clause evaluates its recipient once and calls it with the saved test value. The recipient requires one procedure value and follows the ordinary call checks. No later clause runs after a match or a failure. The final else body runs when every test is false. Selected branches may explicitly return zero, one, or many internal values. The [single-value context rule](/v2.0/en/docs/language/procedures#lispex.rule.v2.procedures.single-value-contexts) and [entry result rule](/v2.0/en/docs/language/procedures#lispex.rule.v2.procedures.entry-result) still apply at their boundaries.
The else and arrow markers use the binding-independent clause interpretation from [Conditions](/v2.0/en/docs/language/conditions#lispex.rule.v2.conditions.guard-grammar). Preparation rejects malformed conditional forms under the existing [source order](/v2.0/en/docs/language/source#lispex.rule.v2.source.preparation-order). The reached form is checked before its child expressions. Cond clause shape checks follow source order. The final else requirement is checked after those clause shape checks. A reservation failure keeps its existing precedence.
| Malformed form | Phase | Code | Data |
| --- | --- | --- | --- |
| If without exactly three operands | normalize | syntax.form | form = if and reason = expected-shape |
| Cond without a final else clause | normalize | syntax.form | form = cond and reason = expected-shape |
| Empty or improper cond clause | normalize | syntax.form | form = cond and reason = clause-shape |
| Else before another cond clause | normalize | syntax.form | form = cond and reason = else-position |
| Cond else without an expression | normalize | syntax.form | form = cond and reason = else-body |
| Cond arrow without exactly one recipient | normalize | syntax.form | form = cond and reason = arrow-shape |
These are existing fields and reasons from the [diagnostic catalog](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.typed-fields). An empty cond has no final else and fails with expected-shape. Neither source normalization nor prepared validation synthesizes an alternative. The [resource event catalog](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-catalog) supplies the existing conditional schedule.
### Require written conditional alternatives
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(if #t 1))))
```
File: `if-false-missing.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(if #f 1))))
```
File: `if-extra.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(if #t 1 2 3))))
```
File: `cond-true-missing.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond (#t 1)))))
```
File: `cond-false-missing.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond (#f 1)))))
```
File: `cond-empty.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond))))
```
File: `cond-empty-clause.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond () (else 7)))))
```
File: `cond-early-else.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond (else 1) (#t 2)))))
```
File: `cond-empty-else.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond (#f 1) (else)))))
```
File: `cond-arrow-shape.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cond (#t => (lambda (x) x) 9) (else 0)))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"case": "if-true-missing",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "if-false-missing",
"source": "if-false-missing.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "if-false-missing.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "if-extra",
"source": "if-extra.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "if-extra.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-true-missing",
"source": "cond-true-missing.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-true-missing.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-false-missing",
"source": "cond-false-missing.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-false-missing.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-empty",
"source": "cond-empty.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-empty.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-empty-clause",
"source": "cond-empty-clause.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-empty-clause.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-early-else",
"source": "cond-early-else.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-early-else.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-empty-else",
"source": "cond-empty-else.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-empty-else.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
},
{
"case": "cond-arrow-shape",
"source": "cond-arrow-shape.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "cond-arrow-shape.scm"
}
],
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Preparation rejects each malformed conditional before evaluation. Product invocation awaits its 2.0 adapter."
}
```
A true test cannot excuse a missing written alternative. Each source is an independent closed module.
### Select each admitted clause shape
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(list
(if #f (car '()) input)
(cond (#f (car '())) (input) (else (car '())))
(cond (#f (car '())) (input => (lambda (value) (+ value 1))) (else (car '())))
(cond (#f (car '())) (else 11 13))
(cond (else 17))))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "7"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The written branches return the list with elements 7, 7, 8, 13, and 17. Product invocation awaits its 2.0 adapter."
}
```
Unselected failures remain unevaluated. Test-only and recipient clauses keep the saved test value.
### Forward explicitly returned internal values
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(list
(call-with-values
(lambda () (if #f 99 (values)))
(lambda results (length results)))
(call-with-values
(lambda () (cond (#f 99) (else (values))))
(lambda results (length results)))
(call-with-values
(lambda () (if #t (values 2 3) (car '())))
(lambda results results))
(call-with-values
(lambda () (cond (#t (values 5 8)) (else (car '()))))
(lambda results results))))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Written branches preserve zero and multiple values for their explicit receivers. Product invocation awaits its 2.0 adapter."
}
```
The first two receivers observe zero values. The later receivers collect two values each. The entry returns one list Datum.
### Leave the other branch unevaluated
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(if #t 7 (car '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The selected branch returns the exact integer 7 and the other branch is not evaluated. Product invocation awaits its 2.0 adapter."
}
```
The unused car expression does not cause a failure or consume evaluation work.
### Stop after the deciding operand
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(list (and #f (car '()))
(or 9 (cdr '())))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The rule returns the list containing false and the exact integer 9. Product invocation awaits its 2.0 adapter."
}
```
Both failing expressions are skipped after the preceding operand determines the result.
### A sequence stops at its first failure
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(begin
1
(car '())
(cdr '()))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The sequence stops at the car domain failure and returns no datum. Product invocation awaits its 2.0 adapter."
}
```
The cdr expression is later in the sequence and cannot replace the first failure.
### Treat only false as false
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(list (if #f 1 2)
(if '() 3 4)
(if 0 5 6))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The rule returns the list of exact integers 2, 3, and 5. Product invocation awaits its 2.0 adapter."
}
```
The empty list and exact zero both select the true branch. Only #f selects the false branch.
## Conditional grammar
### EBNF · source · complete · transcribed
- language: `lispex`
- languageVersion: `2.0`
```ebnf
Conditional = IfForm | CondForm ;
IfForm = "(" "if" expression expression expression ")" ;
CondForm = "(" "cond" clause { clause } ")" ;
```
Imported productions: known; expression, clause.
Omitted productions: known; .
The imported expression is a reader datum admitted as an expression.
The imported clause uses the [guard grammar](/v2.0/en/docs/language/conditions#lispex.grammar.v2.conditions.guard). A clause has a test and body, a test alone, a test and recipient, or an else body. The cond form requires the else clause exactly once and last. Its body must be nonempty. Every preceding clause is a test clause. The if form requires both branches. Keywords compare decoded identifier values under the reader grammar. These restrictions concern ordinary conditionals. Guard keeps its own optional else and unmatched propagation rule.
## Scope and bindings
A binding associates a name with one value. Its scope is the region of source where that association is visible. Lexical scope follows the written nesting of bindings.
A procedure retains access to the bindings visible where it is defined. A call introduces fresh argument bindings. [Procedures](/v2.0/en/docs/language/procedures) defines parameter counts and returned values.
### Resolve a name in its lexical scope
A name refers to the nearest enclosing lexical binding with that name. A nested scope may introduce a new binding with the same spelling. A procedure uses its captured lexical bindings when it is called. A caller cannot change those bindings by declaring a name in its own scope.
**Why**
A procedure can be understood from its definition and captured values. Calling it from another scope preserves that meaning.
Claim: `lispex.claim.v2.evaluation.lexical-scope` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "lexical-name-use",
"context": "prepared-program"
},
"result": {
"kind": "lexical-resolution",
"selection": "nearest-enclosing-binding",
"capture": "definition-environment",
"nestedShadowing": "new-binding"
},
"pendingCases": [
"Capture through several nested procedures and lexical module imports requires further cases after the module syntax is settled.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### A procedure keeps the enclosing value
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((offset 5))
(let ((add-offset (lambda (x) (+ x offset))))
(let ((offset 99))
(add-offset input))))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "7"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The procedure uses the captured offset 5 and returns the exact integer 12. Product invocation awaits its 2.0 adapter."
}
```
The inner offset 99 is a separate binding. Creating it leaves the captured binding unchanged.
### Distinguish parallel and sequential bindings
The let form evaluates its initializers from left to right in the enclosing scope. It introduces the new bindings for the body after all initializers succeed. The let* form evaluates each initializer with the preceding new bindings in scope. Each let* binding introduces a nested scope. A later binding with the same name shadows the earlier binding. Each initializer follows the [single-value context rule](/v2.0/en/docs/language/procedures#lispex.rule.v2.procedures.single-value-contexts).
**Why**
Explicit initializer visibility prevents a name from acquiring a different value because of evaluation order or an implementation environment layout.
Each let* binding introduces a nested scope.
Claim: `lispex.claim.v2.evaluation.binding-initializers` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "local-binding-initialization",
"forms": [
"let",
"let*"
]
},
"result": {
"kind": "initializer-visibility",
"evaluationOrder": "left-to-right",
"letInitializers": "enclosing-scope",
"letBodyBindings": "after-all-initializers",
"letStarInitializers": "preceding-bindings-visible",
"requiredValueCount": 1,
"letStarRepeatedNames": "nested-shadowing"
},
"pendingCases": [
"Competing initializer failures, nested captures across sequential shadowing, and zero or multiple initializer values need additional cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### A let initializer sees the enclosing name
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((x 40))
(let ((x 1)
(y x))
(+ x y)))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The initializer for y sees the enclosing x and the rule returns the exact integer 41. Product invocation awaits its 2.0 adapter."
}
```
The new x is visible in the body. It is not visible to another initializer in the same let.
### A let* initializer sees the preceding name
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((x 40))
(let* ((x 1)
(y x))
(+ x y)))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The initializer for y sees the preceding x and the rule returns the exact integer 2. Product invocation awaits its 2.0 adapter."
}
```
The two binding forms have distinct scope rules even though both evaluate initializers from left to right.
### Reuse a name in a later sequential scope
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let* ((x 1)
(x (+ x 1)))
x)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The later initializer reads the earlier x and the body returns the exact integer 2. Product invocation awaits its 2.0 adapter."
}
```
Each let* binding belongs to a nested scope. The earlier binding is never updated.
### Keep each binding unchanged
A binding keeps its value for its lifetime. The language does not provide set! to replace that value. Passing a value to another procedure or capturing it in a closure does not grant an operation that changes the binding.
**Why**
A rule has no hidden history of assignments. Its lexical bindings remain valid inputs to reasoning, replay, and the meaning graph.
Claim: `lispex.claim.v2.evaluation.immutable-bindings` · rejection · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "binding-lifetime",
"visibility": "guest"
},
"result": {
"kind": "immutable-binding",
"assignment": "rejected",
"captureChangesBinding": false
},
"pendingCases": [
"Removed mutation names in nested forms and mutation attempts through aggregate values require separate cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### Reject an assignment
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(set! input 1)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "9"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The request is rejected and does not return a datum. Product invocation awaits its 2.0 adapter."
}
```
This is a new rejection expectation for 2.0. No successful assignment behavior is carried from the earlier pilot.
## Duplicate definitions
### Reject a repeated definition in one scope
A definition introduces a new binding in its definition scope. Defining the same name again in that scope is a static error. Repeated names in one parallel binding group are also rejected. An enclosing binding and a nested binding remain separate definitions.
**Why**
Replacing a definition would change the value seen by existing references. Rejecting duplicates keeps each name association immutable.
Claim: `lispex.claim.v2.evaluation.duplicate-definitions` · rejection · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "binding-definition",
"duplicateScope": "same-definition-or-parallel-binding-group"
},
"result": {
"kind": "duplicate-binding-rejection",
"duplicateDefinition": "static-error",
"replacement": false,
"nestedShadowing": "allowed"
},
"pendingCases": [
"Duplicate import names and duplicate names in every binding form require preparation and module cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### Reject a second definition
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define threshold 5)
(define threshold 6)
(define rule
(lambda (input)
threshold))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Preparation rejects the duplicate threshold definition and evaluation does not begin. Product invocation awaits its 2.0 adapter."
}
```
The earlier value is not updated and the later value is not selected.
### Reject duplicate names in one let
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((x 1)
(x 2))
x)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Preparation rejects the repeated x name in the parallel binding group. Product invocation awaits its 2.0 adapter."
}
```
Initializer order cannot choose a winner for a repeated name.
See [Diagnostic catalog and reports](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.catalog).
## Recursive bindings
A recursive procedure can call itself. Mutually recursive procedures can call one another. Recursion creates new calls with new argument bindings. It does not assign new values to earlier bindings.
### Tie recursive names only to procedures
Each initializer in letrec must be a lambda expression. The procedure bodies can refer to every name in the recursive group. The bindings are established before any of those bodies is called. Recursive internal definitions follow the same restriction. Calculate other values with let or let*.
**Why**
Restricting recursive initialization to procedures avoids observable partially initialized values while preserving mutual recursion.
Claim: `lispex.claim.v2.evaluation.lambda-recursion` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "recursive-binding-group",
"forms": [
"letrec",
"recursive-internal-definitions"
]
},
"result": {
"kind": "recursive-procedures",
"initializerForm": "lambda",
"bodyVisibility": "all-group-bindings",
"generalValueInitializers": "rejected",
"observableUninitializedValues": false
},
"pendingCases": [
"Computed expressions that return procedures, mixed internal definitions, and recursive references across module boundaries require additional preparation cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### Call another procedure in the recursive group
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(letrec ((even-step (lambda (n)
(if (= n 0) #t (odd-step (- n 1)))))
(odd-step (lambda (n)
(if (= n 0) #f (even-step (- n 1))))))
(even-step input))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "4"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The mutually recursive procedures return true for the exact integer 4. Product invocation awaits its 2.0 adapter."
}
```
Both initializers are lambda expressions. The first procedure body can refer to the second binding.
### Reject a value initializer in letrec
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(letrec ((x 1))
x)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The request is rejected because the recursive binding has a non-lambda initializer. Product invocation awaits its 2.0 adapter."
}
```
A constant value does not become an allowed recursive initializer merely because it has no recursive reference.
### Use an internal recursive procedure
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(define countdown
(lambda (n)
(if (= n 0)
7
(countdown (- n 1)))))
(countdown input)))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "4"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The internal recursive procedure returns the exact integer 7. Product invocation awaits its 2.0 adapter."
}
```
The recursive internal definition has a lambda initializer. Its calls use fresh argument bindings.
### Use named let for a recursive loop
A named let evaluates its initializer expressions from left to right in the enclosing scope. The new loop binding is visible in the loop body. It introduces a recursive procedure for that body and makes an initial call with the initializer values. Each recursive call creates new parameter bindings. The loop body can call the named procedure without replacing an earlier binding.
**Why**
Named let expresses repeated calculation with ordinary recursive procedures and immutable values.
Named let initializers are evaluated in the enclosing scope.
Claim: `lispex.claim.v2.evaluation.named-recursion` · structural · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "named-let",
"body": "recursive-procedure"
},
"result": {
"kind": "named-recursion",
"initialAction": "call-with-initializer-values",
"recursiveCallBindings": "fresh",
"assignment": false,
"initializerScope": "enclosing-scope",
"initializerOrder": "left-to-right",
"loopNameScope": "loop-body"
},
"pendingCases": [
"Zero parameter loops, multiple loop parameters, and nested named let forms require further cases.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### Accumulate a value through recursive arguments
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input)
(total 0))
(if (= n 0)
total
(loop (- n 1) (+ total n))))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "4"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The loop returns the exact integer 10. Product invocation awaits its 2.0 adapter."
}
```
The total for each call is a new parameter binding. The previous total is never assigned another value.
### Resolve an initializer before the new loop scope
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((loop 9))
(let loop ((n loop))
n))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The initializer reads the enclosing loop binding and the rule returns the exact integer 9. Product invocation awaits its 2.0 adapter."
}
```
The new recursive procedure is visible in its body. It does not replace the enclosing value used to calculate the initial argument.
## Tail calls
### Transfer a tail result without retaining a caller frame
The final expression of a procedure body is in tail position. A selected conditional branch and the final expression of a begin or binding body inherit tail position from the enclosing expression. A guard body is not in tail position. The final expression of a selected handler clause body inherits tail position from the guard expression. A tail call passes its result directly to the pending caller. Its frame capacity follows the [semantic-frame rule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.semantic-frames). Its work and logical allocation use those resource accounts.
The implicit target call of `apply` inherits the tail position of that `apply` call. The consumer call of `call-with-values` inherits the tail position of that `call-with-values` call. In tail position, the implicit call takes over the native call's frame and pending return. The replaced native call emits no `call-return`. The producer call and every other library callback are outside tail position.
**Why**
The number of completed tail steps must not become a hidden host stack limit. A loop expressed through `apply` has the same guarantee. Charging each step still guarantees finite execution.
An active guard must keep protecting its body. The enclosing call keeps its pending return if that body fails. Handler tail transfer is possible after guard deactivation.
Claim: `lispex.claim.v2.evaluation.tail-calls` · boundary · coverage partial · verification not-run
- language: `lispex`
- languageVersion: `2.0`
```json
{
"predicate": {
"kind": "tail-position-application",
"resultDestination": "enclosing-continuation"
},
"result": {
"kind": "tail-transfer",
"retainedAdditionalReturnFrame": false,
"workCharged": true,
"logicalAllocationCharged": true,
"executionLimits": "finite"
},
"pendingCases": [
"Every tail position, higher order tail calls, and non-tail recursion require frame boundary cases after the logical frame tariff is fixed.",
"The native, npm, and WASM plans require execution on every supported engine and architecture. Resource boundaries require separate cases below, at, and above each limit."
]
}
```
### Complete many tail calls with a fixed frame budget
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input)
(total 0))
(if (= n 0)
total
(loop (- n 1) (+ total 1))))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "the same finite work and allocation limits sufficient for both calculations",
"frames": "one fixed finite budget sufficient for the surrounding calls without retaining a frame for each tail step"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1000"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The two requests return the exact integers 1 and 1000 under the same finite frame budget. Product invocation awaits its 2.0 adapter."
}
```
The larger input requires more work. It does not require a pending return frame for every completed tail call.
### Stop an unending tail loop at a resource limit
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ()
(loop))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to finish preparation checks",
"evaluate": "finite values sufficient to enter the loop"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The unending tail loop reaches a terminal resource stop and returns control without a result datum. Product invocation awaits its 2.0 adapter."
}
```
Eliminating retained return frames does not eliminate work charges or permit unbounded execution.
See [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers).
### Finish a tail apply loop with a small frame budget
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input))
(if (= n 0)
7
(apply loop (list (- n 1))))))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": {
"work": "finite work sufficient for both complete requests",
"allocation": "finite allocation sufficient for both complete requests",
"frames": "one fixed small finite budget sufficient for module initialization, one active loop invocation, and its bounded operand calls and expression events, independent of the iteration count",
"channels": "finite channel limits sufficient for both requests and their result encoding"
}
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1000"
}
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Both requests return 7 under the same small frame budget. Every apply target inherits tail position and takes over the native frame. No replaced apply call emits call-return. Product invocation awaits its 2.0 adapter."
}
```
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
### Stop a nontail apply loop at its frame limit
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input))
(if (= n 0)
0
(+ 1 (apply loop (list (- n 1)))))))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": {
"work": "finite work sufficient for the complete recursion if frames permit it",
"allocation": "finite allocation sufficient for the complete recursion if frames permit it",
"frames": "a small finite budget sufficient for module initialization and at least one recursive step but insufficient for the full chain of pending calls for input 1000",
"channels": "finite channel limits sufficient for the request and terminal diagnostic"
}
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1000"
}
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The apply call is an argument of addition. Its target inherits nontail position and retains the native continuation. The small frame budget stops recursion before the base case. Product invocation awaits its 2.0 adapter."
}
```
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
### Transfer a call-with-values frame to its consumer
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input))
(if (= n 0)
7
(call-with-values
(lambda () (- n 1))
loop))))))
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": {
"work": "finite work sufficient for the complete request",
"allocation": "finite allocation sufficient for the complete request",
"frames": "one small finite budget sufficient for module initialization, one active loop invocation, and its bounded producer and operand work, independent of the iteration count",
"channels": "finite channel limits sufficient for the request and result encoding"
}
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1000"
}
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "The loop returns 7 under a small frame budget. Each producer call is nontail and finishes before its consumer. Each consumer inherits tail position and takes over the native frame. Product invocation awaits its 2.0 adapter."
}
```
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
### Stop guarded body recursion at the frame limit
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ()
(guard (condition
(else 99))
(loop)))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite work and allocation sufficient through the first frames refusal. Every other axis and channel is sufficient.",
"frames": "one fixed finite budget sufficient to enter the first guard and make one recursive call"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Recursive calls in the protected body exhaust the fixed frame budget. The terminal resource stop does not enter the handler. Product invocation awaits its 2.0 adapter."
}
```
Each recursive call keeps its active guard and pending return. The resource model selects the first refused frame reservation. The example fixes no tariff or failing depth.
### Repeat handler tail calls within one frame budget
Mode: illustrative. Stage: semantic-request. Verification: not-run.
- language: `lispex`
- languageVersion: `2.0`
File: `source.scm`
```lispex
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((remaining input))
(if (= remaining 0)
0
(guard (condition
(else (loop (- remaining 1))))
(car '()))))))
)
```
File: `request.json`
```lispex
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "the same finite work and allocation limits sufficient for both complete requests. Every channel is sufficient.",
"frames": "one fixed finite budget sufficient for the surrounding calls and one complete loop step. It covers the active guard and transient calls."
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1000"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
```
Fixture inputs and environment:
```json
{
"entry": "source.scm",
"argv": [],
"stdin": "",
"cwd": ".",
"environment": [],
"wrapper": null,
"packageRef": null,
"lockRef": null,
"generatedBindingRefs": {
"knowledgeState": "not-applicable",
"values": []
}
}
```
#### Expected result
```json
{
"status": "unspecified",
"reason": "Both requests return the exact integer 0 under the same finite frame budget. Completed handler tail calls retain no extra call or guard frames. Product invocation awaits its 2.0 adapter."
}
```
Each car failure selects the handler after guard deactivation. The handler tail call reuses the enclosing call frame. Work and logical allocation still accumulate.
## Related chapters
[Source and normalization](/v2.0/en/docs/language/source)
[Procedures](/v2.0/en/docs/language/procedures)
[Conditions](/v2.0/en/docs/language/conditions)
[Preparation and modules](/v2.0/en/docs/tools/prepare)
### Pending · Resource model numbers
The 2.0 tariff coefficients, logical allocation units, bit-size accounting, detailed frame accounting, finite defaults, representation limits, and physical memory envelopes remain open. This includes preparation, calls, values, exact arithmetic, equality, text, record conversion, and canonical encoding.
Profile host budget coefficients and defaults remain separate from language preparation and evaluation budgets. Trace capacity, reservation sizes, and host memory requirements retain their separate reporting scope. Each budget retains its own identity and accounting boundary.
Implementation and attack tests must support these choices. [Resource event declarations](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-catalog) and [native kernel membership](/v2.0/en/docs/library#lispex.pending.v2.standard-library.kernel-and-cost-model) remain separate contracts.
### Pending · Native kernel membership
The final native kernel list and count remain open. Implementation and product attack tests must support these choices. [Tariff coefficients, allocation units, finite defaults, and physical envelopes](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers) are tracked once with the resource numbers.
## Related
[Source and normalization](/v2.0/en/docs/language/source)
[Procedures](/v2.0/en/docs/language/procedures)
[Conditions](/v2.0/en/docs/language/conditions)
[Preparation and modules](/v2.0/en/docs/tools/prepare)