Go backward to Meaning of Non-Terminal Sentences Go up to Top Go forward to Meaning of Sentence |
B in Binary-numeral
D in Binary-digit
B ::= BD | D
D :: = 0 | 1
Natural Numbers:
Domain Nat = N
Operations zero, one, two, ...: Nat
plus, times: Nat × Nat -> Nat
B: Binary-numeral -> Nat
B[[ D ]] = D[[ D ]]
B[[ BD ]] = (B[[B]] times two) plus D[[ D ]]
D: Binary-digit -> Nat
D [[ 0 ]] = zero
D [[ 1 ]] = one