1. \cfrac{premise}{conclusion}

    is called inference rule, it stands for: if premise above the line is established, we can then derive the conclusion below the line.

  2. There are several ways to define a set, inductively, concretely and by using inference rules. Inductive definition starts with a base case and then derive inductive rules. Concrete definition using mathematical notations such as \cup to form a set explicitly. The inference rules using the axiom and premise part as the base case and conclusion part as induction rules. for example, suppose \mathcal{T} is set of terms, following inference rules define a language L(\mathcal{T}) on \mathcal{T}

    &\text{1. } \tt true\in\mathcal{T}\ \ \ \tt false\in\mathcal{T}\ \ \ \ \tt0\in\mathcal{T}\\
    &\text{2. } \cfrac{t_1\in\mathcal{T}}{\tt succ\ t_1\in\mathcal{T}}\ \ \ \cfrac{t_1\in\mathcal{T}}{\tt pred\ t_1\in\mathcal{T}}\ \ \ \cfrac{t_1\in\mathcal{T}}{\tt iszero\ t_1\in\mathcal{T}}\\
    &\text{3. } \cfrac{t_1\in\mathcal{T}\land t_2\in\mathcal{T}\land t_3\in\mathcal{T}}{\tt if\ t_1\ then\ t_2\ else\ t_3\in\mathcal{T}}

    which can also be defined by Backus-Naur Form as given below:

    term \rightarrow\
    &\tt true|\tt false|\\
    &\tt if\ \textit{term}\ then\ \textit{term}\ else\ \textit{term}|\\
    &\tt 0|\\
    &\tt succ\ \textit{term}|\tt pred\ \textit{term}|\tt iszero\ \textit{term}\\
  3. Operational Semantics use an abstract state machine to describe the behavior of the program, the meaning of a program is the final state of its corresponding state machine's halt state.

  4. Denotational Semantics use mathematical functions to represent the meaning of a program, e.g., a function on natural numbers.
  5. Axiomatic Semantics use program statement as laws and the meaning of the program is what can be proved about it, generally speaking, both operational and denotational semantics use program's behavior to derive statements, which is opposed to the axiomatic semantics
  6. Evaluation Relation is a binary relation on a language(or other structures, in this example, L(\mathcal{T}), written in \mathtt{t}\rightarrow \mathtt{t}', denotes "\tt t evalutes to \tt t'" in one step, which stands for a transition of the state mechine: if the state machine is in state t, we can change to state t'. it can be constructed by a set of inference rules, for example:

    &\text{1. }\mathtt{if\ true\ then\ t_2\ else\ t_3\rightarrow t_2}\\
    &\text{2. }\mathtt{if\ false\ then\ t_2\ else \ t_3\rightarrow t_3}\\
    &\text{3. }\cfrac{\tt t_1\rightarrow t_{1}'}{\tt if\ t_1\ then\ t_2\ else\ t_3\rightarrow if\ t_{1}'\ then\ t_2\ else\ t_3}

    the above inference rules stated:

    1. if the current state(specifically, the expression/term that are currently being evaluated) satisifies rule 1, we can replace its entire content to \tt t_2, and so for rule 2. If their is another machine that evaluates \tt t_1 to \tt t_{1}', then we can replace all the occurences of \tt t_1 to \tt t_{1}'
  7. An instance of an inference rule is obtained by consistenly replacing each metavariable by the corresponding actual value in both premise(if exist) and conclusions(similar to substitution)

  8. A rule is satisified by a relation if for all instance of the rule, either one of the premises is not in the relation or its conclusion is in the relation.

  9. The one-step evaluation (denote \rightarrow) is the smallest binary relation sastisfies all of the inference rules, which, in this example, is rule 1, 2 and 3, pair (\tt t, t') is said to be derivable if it is in the relation. generally speaking, a statement \tt t \rightarrow t' is derivable if and only if it is either an instance of one of the computation rule in the inference rules, or it's the conclusion of an instance of congruence rules, who's premises are derivable.

  10. A term \tt t is said to be in normal form if no rule can apply to it, which means there is no such a \tt t' that \tt t\rightarrow t'

We Choose to Go to the Moon