MAC: Computability of terms

Up.

The table below displays page number, some attributes, and name of construct for all constructs in Volume 3 of the text book.

The V attribute indicates that the given construct produces a value. An expression has a value if it is made up from variables, numerals, and constructs that have the V attribute. In Volume 3, this information is stated in the subsection named "sort", but it is repeated here for convenience. According to Section 1.20 in the text book, an expression is a term if it has a value and is a statement otherwise.

The C attribute indicates that the given construct is computable. A term is computable if it is made up from bound variables, numerals, and constructs that have the C attribute. Note that being computable does not guarantee that a computer can compute a value in finite time.

The S attribute indicates that the given construct returns the strong representation of a truth value, decimal fraction, or exception, whenever all parameters of the construct are weak representations of truth values, decimal fractions, or exceptions.

504 V - S all x in y colon z
505 V C - bottom
506 V C - case x comma y comma z end
507 V - - choose x in y colon z
508 V - S classical
509 - - - construct x
510 V C S empty list
511 V C S exception
512 V - S exists x in y colon z
514 V C S false
515 V C S f four of x end
516 V C S f one of x end
517 V C S f three of x end
518 V C - f two
519 V C - if x then y else z
521 V C S infinity
522 V C - lambda x dot y
523 V C S minimum x comma y end
524 V C S minus x
525 V C S nil map
526 V C S not x
527 Macro parenthesis x end
528 V C S plus x
529 V C S precision x
530 V C - substitute x where y is z end
532 V - S the class of sets
533 V - S the set of decimal fractions
535 V - S the set of decimal fractions of precision x end
537 V - S the set of exceptions
539 V - S the set of false maps
541 V - S the set of infinities of precision x end
543 V - S the set of integers
545 V - S the set of minus infinities of precision x end
547 V - S the set of natural numbers
549 V - S the set of negative integers
551 V - S the set of positive integers
553 V - S the set of the empty list
554 V - S the set of true maps
556 V - S the set of truth values
558 V C S true
559 V C - tuple x end
560 - - - variable x
561 V C S x and y
563 V C - x apply y
564 - - - x associates as y
565 V C S x atom
566 V - S x belongs to y
568 V - - x cartesian y
569 - - - x colon y
570 - - - x comma y
571 V C S x computational equal y
573 V C S x computational unequal y
575 - - - x concludes y
576 - - - x deduces y
577 - - - x defined equal y
578 V C S x divide y
580 - - - x equal y
582 V C S x exceptional
583 V C - x faculty
584 - - - x greater priority y
585 V C - x head
586 V C S x if and only if y
588 V C S x implied by y
590 V C S x implies y
591 - - - x infers y
592 V C S x integer divide y
594 - - - x lemma y colon z
595 V - - x listset
596 - - - x macro equal y
597 V C S x minus y
599 V C S x modulo y
601 - - - x modus ponens y
602 - - - x optimised equal y
603 V C S x or y
605 V C S x pair
606 V C - x pair y
607 V C S x plus y
609 V C S x power y end
611 V C S x predecessor
612 - - - x proof of y colon z
613 - - - x reduces to y
614 V C S x round y
616 - - - x rule y colon z
617 - - - x same priority y
618 - - - x semicolon y
619 V C - x simple head
620 V C - x simple pair
621 V C - x simple tail
622 V C S x strongly greater than
624 V C S x strongly less than
626 V C S x successor
627 V C - x tail
628 - - - x term reduces to y
630 V C S x times y
632 V C S x weakly greater than
634 - - - x weakly less information y
636 V C S x weakly less than y

Klaus Grue, GRD-2004-08-16