Midterm 1 Definitions Flashcards
abstract syntax tree (AST)
A tree representation of a program that is abstracted from the details of a particular programming language and its surface syntax.
association list
in Lisp, a list composed of pairs of a symbolic name and associated value, used to represent variable bindings, substitutions, and data sets.
atom
- in propositional or predicate calculus, a predicate symbol with the appropriate number of arguments. For example, MORTAL(Socrates) is an atom, where MORTAL is the predicate and Socrates is a constant term that is its argument. Also, atomic formula.
- in Lisp, data that is not a cons cell, such as a symbol or a number.
backchaining
a proof that starts with the conclusion and searches for facts or rules that support the conclusions, recursively.
backtrack
in a tree search, to move back from the node currently being examined to its parent.
base case
A simple case that can be solved easily, without recursion.
binary tree
A tree in which each node has at most two children.
Contents and left and right links.
Node = cons, binary links = first and rest.
E.g. arithmetic expressions
binary search tree (BST)
A binary tree in which all elements less than the current element are to its left and all elements greater are to its right.
binding
an association of a name with a value.
box
in logic or resolution theorem proving, the empty clause; from its mathematical symbol, &box;
False, contradiction, empty.
branching factor
in a search tree, the number of children of a given node. Usually, the branching factors of individual nodes will vary.
combinatoric explosion
the rapid growth of the number of possibilities to be explored in a search, often exponential because it is the product of the number of possible choices at each level of the search tree.
The rapid growth of combinations of possible moves.
combine
an operator that is used to combine elements in an accumulation
conjunctive normal form (CNF)
a canonical form of writing predicate calculus formulas as a conjunction (AND) of clauses (disjunction (OR) of literals); used in resolution theorem proving.
consistent
of a logical formula, having some interpretation that makes it true.
constant folding
performing at compile time an operation whose operands are constant, giving a new constant result.
constructive
proving that a formula is consistent by constructing an element that makes it true.
Constructive proof: given a theorem ∀x∃y P(x, y), prove it by constructing a y that satisfies the theorem.
During program synthesis, witnesses are constructed for existential terms. The witnesses correspond to subroutines in the SPICE library (concrete terms).
specification → theorem → proof → program
decidable
of a theorem proving or decision making task, able to be decided one way or the other (e.g., proved or disproved) within a finite time bound that can be determined from the size of the input problem. cf. undecidable.
depth
depth of a tree in number of links below the root.
depth-first search (DFS)
a search in which children of a node are considered (recursively) before siblings are considered
design pattern
a pattern that describes a set of similar programs.
destructive
describes a function that modifies its arguments.
eval
Lisp / Clojure function that evaluates an expression.
exists
the logical quantifier ∃, pronounced “there exists” or “for some”.
fixpoint
a value of a function where f(x) = x, i.e. applying a function such as optimization to an expression no longer can do any more.
for all
the logical quantifier ∀, describing something that is true for all possible values of the quantified variable.
functional program
a program in which all computation is performed by functions and there are no side-effects.
homoiconic
describes a language such as Lisp where programs and data are the same.
Horn clause
a logical formula that is a disjunction (OR) of literals and has at most one positive literal. Viewed as a rule, a Horn clause is a rule from a conjunction (AND) of positive literals to a single positive conclusion literal, e.g. A ∧ B ∧ C → D
Clauses that have at most one positive literal when written in Conjunctive Normal Form as a disjunction of literals.. Assumed by backward chaining.
A ∧ B → C
(A ∧ B) → C
¬(A ∧ B) ∨ C
¬A ∨ ¬B ∨ C
identity element
for a given operation, an element that leaves the value unchanged. E.g., for + the identity element is 0.
immutable
a data structure whose value cannot be changed once it is created.
inconsistent
a logical formula that is contradictory or unsatisfiable
inference
derivation of additional true statements from a given set of true statements.
interpretation
an assignment of values to variables in a logical statement
in-line
to expand a function as code at the point of call
interior node
a node of a tree that has children
interpreter
a program that reads an instruction, determines its meaning, and executes it. Lisp has an interpreter (eval) that can execute code constructed at runtime.
invalid
not valid, i.e. not always true or possibly false
Not true under every possible interpretation: P.
leaf
a bottom node of a tree
linked list
a linear data structure where records are linked by pointers
literal
a logical predicate or its negation: P or ¬P
loop unrolling
converting a loop into straight-line code by repeating the code inside the loop while substituting successive values of the loop index
macro
a short amount of code that expands into a large amount of in-line code.
operand
a value on which an operator acts
operator
an action such as + that produces new values from given values
partial evaluation
to evaluate an expression in which some operands are known, e.g. x + 0 ⇒ x
predicate
in predicate calculus, a symbol that is applied to zero or more arguments and is assigned values of True or False in an interpretation
a function that tests a condition and returns a value of true or false.
propositional calculus
a logical representation in terms of propositional variables, each of which is true or false and has no arguments.
quote
a Lisp function that returns its argument, without evaluating it
recursion
a function that calls itself as a subroutine
rewrite rule
a rule containing variables that tells how to rewrite a given form of expression as another form
root
the top element of a tree
SAT
testing whether a logical formula is satisfiable, i.e. true under some interpretation
SAT solver
a program that can efficiently find solutions to problems expressed as SAT problems, e.g. WalkSAT and CHAFF.
satisfiable
consistent, i.e. true for some interpretation.
scope
the region of program text over which a name can be referenced.
search
to try sequences of operators to attempt to find a sequence that satisfies a goal.
side-effect
any effect of a function other than returning a value, such as printing or changing the value of a global variable
specialize
to make a version of a generic procedure that is specialized for certain data types or constant values.
state space search
a search for a sequence of operators that will transform a given starting state into some goal state. Each operator transforms a state into a different state.
structure sharing
a case where two data structures share some elements.
symbol
a runtime data structure that represents an algebraic or symbolic name
tail recursion
a function whose value either does not involve a recursive call, or is exactly the value of a recursive call.
term
in logic, an algebraic variable that represents an object in the application domain. Terms include variables, constants, and functions applied to terms.
unsatisfiable
of a logical formula, false under every interpretation; inconsistent or contradictory.
valid
of a logical formula, true under every interpretation.
variable capture
a problem of a macro including a variable from its call in its generated code
variable in pattern
a symbol that can be replaced by a corresponding part of the matched input
well-founded ordering
an ordering that can be guaranteed to terminate, e.g. starting at a positive integer and counting down to 0.
