<jupyter_start><jupyter_text>$\newcommand{\To}{\Rightarrow}$<jupyter_code>import os, sys
sys.path.append(os.path.split(os.getcwd())[0])
from kernel.type import TFun, boolT
from kernel.term import Var, Const, Comb, Term
from logic.nat import natT, zero, plus, times
from logic.logic import true, false, conj, disj, neg<jupyter_output><empty_output><jupyter_text>Terms We now introduce the concept of *terms*. Terms are the building block of the language of higher-order logic. To understand types and terms intuitively, we make an analogy to ordinary programming languages: in a statement `int x = y + z`, both `x` and `y + z` are terms while `int` is a type. The statement declares a new variable `x` of type `int`, and sets it to the value of the term `y + z`. In higher-order logic, each term has a unique type (introduced in the previous section). A basic example of a term is a *variable*. It is constructed by providing a name and a type:<jupyter_code>a = Var("a", natT)
print(a)<jupyter_output>a<jupyter_text>Note a variable is displayed using its name. Its type is not displayed. To get the type of any term, we use the `get_type()` method:<jupyter_code>print(a.get_type())<jupyter_output>nat<jupyter_text>Another example of a term is a *constant*. A constant is also determined by its name and type. The difference between constants and variables is that a constant is assumed to represent some fixed mathematical concept, while a variable can stand in for any other term. Examples of constants include true, false (both boolean values) and zero (a natural number).<jupyter_code>print(Const("zero", natT))
print(Const("true", boolT))
print(Const("false", boolT))<jupyter_output>zero
true
false<jupyter_text>These are used so frequently that we provide shorthands for them:<jupyter_code>print(zero)
print(true)
print(false)<jupyter_output>zero
true
false<jupyter_text>A variable (or constant) can also have function type. For example, the following declares a variable that is a property of natural numbers:<jupyter_code>f = Var("f", TFun(natT, boolT))
print(f.get_type())<jupyter_output>nat => bool<jupyter_text>Given a term $f$ of function type $A \To B$, and a term $a$ of type $A$, we can form the term $f\ a$, representing the evaluation of $f$ at $a$. In ordinary mathematics, this is also written as $f(a)$. However, we follow the usual convention in higher-order logic, with a space between two terms denoting function application. The term $f\ a$ can be constructed as follows (here Comb stands for *combination*):<jupyter_code>c = Comb(f, a)
print(c)<jupyter_output>f a<jupyter_text>We take advantage of Python's ability to install custom `__call__` functions to create the following shortcut for forming combinations:<jupyter_code>c = f(a)
print(c)<jupyter_output>f a<jupyter_text>A function application $f\ a$ is only permitted when $f$ has function type, and the type of $a$ agrees with the domain of that function type. In all other cases, the function application is illegal, and we say *type-checking* fails on that term. While we can form a function application that is illegal, an error is raised when we try to *type-check* the term. Type checking is performed with `checked_get_type()`, which also returns the type of the term. Here is an example where `checked_get_type()` fails:<jupyter_code>f = Var("f", TFun(natT, boolT))
x = Var("x", boolT)
t = f(x)
t.checked_get_type()   # raises TypeCheckException<jupyter_output><empty_output><jupyter_text>Given a function with two arguments, we can evaluate the function one argument at a time. For example, if $g$ is a function of type $nat \To nat \To nat$, and $a$ and $b$ are both of type $nat$, then $(g\ a)\ b$ is the evaluation of $g$ on $a$ and $b$. Note this is very different from the term $g\ (a\ b)$ (which will not type-check). Since the former occurs more frequently, we have the convention that function application associates to the left. Hence, $(g\ a)\ b$ can be written more compactly as $g\ a\ b$.<jupyter_code>g = Var("g", TFun(natT, natT, boolT))
a = Var("a", natT)
b = Var("b", natT)
print(g(a)(b))<jupyter_output>g a b<jupyter_text>But in fact, the `__call__` function for terms is written such that all arguments can be provided at the same time:<jupyter_code>print(g(a, b))<jupyter_output>g a b<jupyter_text>While the printed form $g\ a\ b$ is very simple, it is worth remembering how the term is represented behind the scenes. The `repr` function returns the detailed representation of the term:<jupyter_code>print(repr(g(a, b)))<jupyter_output>Comb(Comb(Var(g,nat => nat => bool),Var(a,nat)),Var(b,nat))<jupyter_text>Common operators Many of the most frequently used operators are functions on two arguments. For example, addition and multiplication are both functions of type $nat \To nat \To nat$. In propositional logic, conjunction and disjunction are both functions of type $bool \To bool \To bool$. Negation is a function of type $bool \To bool$.<jupyter_code>print(repr(plus))
print(repr(times))
print(repr(conj))
print(repr(disj))
print(repr(neg))<jupyter_output>Const(plus,nat => nat => nat)
Const(times,nat => nat => nat)
Const(conj,bool => bool => bool)
Const(disj,bool => bool => bool)
Const(neg,bool => bool)<jupyter_text>These can be applied to terms just like any function. For example, the term $x + y$ (where $x$ and $y$ are natural numbers) is represented as follows:<jupyter_code>x = Var("x", natT)
y = Var("y", natT)
z = Var("z", natT)
t = plus(x, y)
print(t)<jupyter_output>plus x y<jupyter_text>The output is not very readable, as the basic printing function does not understand how to print binary operators using symbols and infix form. This gets worse as the expression gets longer. Hence, from now on we use a more sophisticated printing function. This printing function needs to be provided a *theory*, which contains information about currently available types, constants and theorems. It also contains information about how to print the basic operators. Theories will be discussed in more detail in later sections, for now we just use some boilerplate code to setup the printing.<jupyter_code>from logic import basic
from syntax import printer
thy = basic.load_theory('nat')
print(printer.print_term(thy, t))<jupyter_output>x + y<jupyter_text>The printing function understands usual order of evaluation rules. Note addition (and multiplication) associates to the left.<jupyter_code>t1 = plus(x, times(y, z))
print(printer.print_term(thy, t1))

t2 = times(plus(x, y), z)
print(printer.print_term(thy, t2))

t3 = plus(x, plus(y, z))
print(printer.print_term(thy, t3))

t4 = plus(plus(x, y), z)
print(printer.print_term(thy, t4))<jupyter_output>x + y * z
(x + y) * z
x + (y + z)
x + y + z<jupyter_text>Likewise, we can use conjunction and disjunction to form expressions in propositional logic.<jupyter_code>P = Var("P", boolT)
Q = Var("Q", boolT)
R = Var("R", boolT)

t1 = conj(P, Q)
print(printer.print_term(thy, t1))

t2 = disj(P, Q)
print(printer.print_term(thy, t2))<jupyter_output>P & Q
P | Q<jupyter_text>Here, we use ASCII characters `&` to represent conjunction, and `|` to represent disjunction. This is in keeping with programming languages such as C, where `&&` stands for `and` and `||` stands for `or`. However, if the user interface allows, we can also print in unicode:<jupyter_code>print(printer.print_term(thy, t1, unicode=True))
print(printer.print_term(thy, t2, unicode=True))<jupyter_output>P ∧ Q
P ∨ Q<jupyter_text>Here are some more examples. Observe the order of evaluation between conjunction and disjunction, as well as the fact that both logical operators associate to the right.<jupyter_code>t1 = conj(P, disj(Q, R))
print(printer.print_term(thy, t1, unicode=True))

t2 = disj(conj(P, Q), R)
print(printer.print_term(thy, t2, unicode=True))

t3 = conj(P, conj(Q, R))
print(printer.print_term(thy, t3, unicode=True))

t4 = conj(conj(P, Q), R)
print(printer.print_term(thy, t4, unicode=True))<jupyter_output>P ∧ (Q ∨ R)
P ∧ Q ∨ R
P ∧ Q ∧ R
(P ∧ Q) ∧ R<jupyter_text>The equality operator is special in that it can take arguments of any type, as long as the two arguments have the same type. The output type is always bool. Hence, the type of the equality operator is $'a \To\ 'a \To bool$. Here $'a$ is a *type variable*, introduced in the previous section. To form an equality expression, we use the `mk_equals` function in `Term`. Note how the type of the equality constant is instantiated according to the type of the arguments provided to `mk_equals`.<jupyter_code>t = Term.mk_equals(x, y)
print(printer.print_term(thy, t))
print(repr(t))

t = Term.mk_equals(P, Q)
print(printer.print_term(thy, t))
print(repr(t))<jupyter_output>x = y
Comb(Comb(Const(equals,nat => nat => bool),Var(x,nat)),Var(y,nat))
P = Q
Comb(Comb(Const(equals,bool => bool => bool),Var(P,bool)),Var(Q,bool))<jupyter_text>Accessing part of a term For both variables and constants, `name` is the name of the term:<jupyter_code>x = Var("x", natT)
print(repr(x.name))<jupyter_output>'x'<jupyter_text>Given a combination, `fun` and `arg` returns the function and argument of the combination:<jupyter_code>f = Var("f", TFun(natT, natT))
t = f(x)
print(t.fun)
print(t.arg)<jupyter_output>f
x<jupyter_text>Let's try this on the evaluation of a binary operator:<jupyter_code>y = Var("y", natT)
t = plus(x, y)
print(t.fun)
print(t.arg)<jupyter_output>plus x
y<jupyter_text>What's going on here? Recall that a binary operator like `plus` is represented by a function of type $nat \To nat \To nat$. The term $x + y$ is really `plus x y` or, with parenthesis put in, `(plus x) y`. Hence, at the outermost level, the term is a function application with function `plus x` and argument `y`. The term `plus x` is a *partial application* of the function `plus`. It is, on its own, a function of type $nat \To nat$ that adds $x$ to its argument.Given the application of a binary operator, most often we want to access the operator itself, as well as the two arguments. We have already seen that the second argument can be accessed by `arg`. The first argument can be accessed by `arg1`, and the operator can be accessed by `head`:<jupyter_code>print(t.head)
print(t.arg1)<jupyter_output>plus
x<jupyter_text>More generally, given a term of the form $f\ t_1\ t_2\cdots t_n$, the method `strip_comb` returns the pair $f, [t_1, \dots, t_n]$. The properties `head` and `args` correspond to $f$ and $[t_1, \dots, t_n]$, respectively. We demonstrate these functions below. Note the use of multiple assignment syntax in Python to simplify the code.<jupyter_code>g = Var("g", TFun(natT, natT, natT))
z = Var("z", natT)
t = g(x, y, z)
print(t.strip_comb())
print(repr(t.head))
print(t.args)

f, (a1, a2, a3) = t.strip_comb()
print(f, a1, a2, a3)<jupyter_output>(Var(g,nat => nat => nat), [Var(x,nat), Var(y,nat), Var(z,nat)])
Var(g,nat => nat => nat)
[Var(x,nat), Var(y,nat), Var(z,nat)]
g x y z<jupyter_text>Given an equality term, its left and right side can be accessed using `arg1` and `arg`. However, writing the code in this way is unintuitive. We further provide properties `lhs` and `rhs` to access the left and right sides of an equality:<jupyter_code>t = Term.mk_equals(x, y)
print(t.lhs)
print(t.rhs)<jupyter_output>x
y
{'fraction_non_alphanumeric': 0.11411010154997328, 'fraction_numerical': 0.003206841261357563, 'mean_word_length': 5.485846331600231, 'pattern_counts': {'":': 0, '<': 81, '<?xml version=': 0, '>': 101, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '26', 'dir': 'jupyter-structured-clean-dedup', 'id': '255208', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 3772, 'n_tokens_neox': 3682, 'n_words': 1487, 'path': 'tutorial/terms.ipynb', 'repo_name': 'zhouwenfan/temp', 'size': '11226'}