<defined op instance> == <expansion>
which stipulates that the left-hand side "expands" to the right-hand side.
Or more generally, for any "instantiation" of the definition, its left-hand side expands to its right-hand side. As a convenience it is also permitted to use function applications on the left-hand-side instead of lambda operators on the right-hand-side; for example the definition of function composition x.f(g(x))
This leaves three things to be explained:
1. | So what if one term expands to another? |
2. | What is an instance of a definition? |
3. | What restrictions are there on legitimate definitions? |
1. Part of the meaning of an assertion in Nuprl is that it is true iff expanding all the defined operators within it (until none remain) results in a true assertion. Thus, a term can be regarded as meaning whatever it fully expands to.
Below we shall employ the concepts about the form of expressions explained in
2. Instantiating a definition consists of possible change of binding variables, first- and second-order substitution for free variables throughout the definition, and uniform replacement of op-parm variables by op-parm values or other suitable expressions. See
expands to {i: according to| 0
i }
Def == {i:
| 0
i }
1+2 expands tox
according to x<1+2
Def A B ==
B<A
x.12 expands to<"x",12> according toDef $abc.$n == <"$abc",$n>
"Induction for x: . 0<x"
expands to"0<0 & ( x:
. 0<x
0<x+1)
(
x:
. 0<x)"
according toDef Induction for x: . P(x) == P(0) & (
x:
. P(x)
P(x+1))
(
x:
. P(x))
Weird(3; u,v. v expands tov-u)
3 3-(0
0-3)
according toDef Weird(x; u,v. F(u;v)) == F(F(x;0);x)
HigherConsequence{k'}(0<x) expands to{X:Prop{k''}| 0<x X }
according toDef HigherConsequence{i}(P) == {X:Prop{i'}| P X }
(
Prop{[level]} takes a level-expression; seeProp Levels and Predicativity .)
3. See
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() |