Term Rewriting: Equational Logic (Aart Middeldorp)

This is all about TERMS I think

49 flashcards · Mathematics · by lakesare

Name 2 objects that exist in equational logic.
functions (0-arity function is a constant) variables
How to read this?
s is a subterm of t
How to read this?
Variables occurring in term t.
What's a ground term?
A term with no variables. A term t is called ground if Var(t) = ∅. The set of all ground terms is denoted by 𝒯(𝐹).
What do these denote: T(𝐹, 𝒱) VS T(𝐹)
T(𝐹, 𝒱) - all terms generated by functions 𝐹 and variables 𝒱 T(𝐹) - all ground terms generated by functions 𝐹.
What's the root symbol of a term?
Leftest function name.
What does |t| denote?
|all variable and function symbols in a term| The number of variable symbols AND function symbols.
What does |t|a denote?
|"a" symbols in a term| The number of "a" symbols in the term.
What does ∥t∥ denote?
|function symbols in a term| The number of function symbols in the term.
What's 𝐹 and V in this term?
𝐹: a binary function symbol +, a unary function symbol s, and a constant 0. V: x and y are variables in V. Tree representation of a term
What's root(t)?
What's |t| (the size of this term)?
What's |t|+?
What's ∥t∥?
What's the height(term)?
Max height of the tree, and we only count 1+-ary functions.
How to read this?
All positions (Pos) of variables (V) in a term (t).
How to read this?
All positions (Pos) of functions (F) in a term (t).
Difference between: t(p) VS t|p
What's t|11?
What's t(11)?
t(11) = +
What's t[x + 3]2?
Substitute t|2 with [x+3]
How is σ pronounced?
Sigma uppercase Σ
What is the substitution a mapping: from & to?
from: variable to: term
What does Dom(σ) likely denote?
Domain of the substitution σ.
What does tσ likely denote?
Term t with the substitution σ.
What's an instance of a term?
This term with some substitution.
Visually imagine: some term is an instance of some term.
█████████ is an instance of ███
Visually imagine: some term matches some term.
███ matches █████████
[Positions in terms: <, >, ∥] How do 2 and 211 relate?
less = less deep
[Positions in terms: <, >, ∥] How do 1 and 212 relate?
Sum up how we decide the matching problem?
Strip off the function symbol.
What does this mean in symbols?
=> If s is a subterm of t, and σ is an arbitrary substitution, then sσ is a subterm is tσ.
Visually imagine a linear term.
linear term == variables don't occur multiple times. t is linear because the variable x appears only once in t.
What's "the matching problem"?
Find a substitution σ.
[Equational Reasoning] Visually imagine an equation.
[Equational Reasoning] Visually imagine an equational system (ES).
ES 𝐸 consisting of the two equations.
What's does α and 𝒜 denote here:
[variable assignment]function assignment(term)
What does =𝒜 mean?
[any variable assignment!]function assignment(term) == [any variable assignment!]function assignment(term)
What could this mean?
Interpretation of term in 𝐵-algebra.
What does ES stand for?
Equational system
What 2 things do we need to specify an equational system? ES 𝓔 consisting of the two equations
signature 𝓕 set of equations 𝓔
In equational logic, what is: semantic component syntactic component?
In equational logic, what is: semantic component - algebra syntactic component - equational reasoning
What's the relationship between these: s ≈𝐸 t s =𝐸 t
Equational logic is sound and complete: s ≈𝐸 t ⇔ s =𝐸 t. Below we show that equational reasoning is sound. This means that every equation s ≈ t deducible from an ES E by equational reasoning is valid in all models of E. Completeness of equational reasoning.
Visually imagine what these mean: s ≈𝐸 t s =𝐸 t 𝐸 is the "Equational System 𝐸"
s ≈𝐸 t - syntactic ⊢, equational reasoning. Let 𝐸 be an ES. We write s ≈𝐸 t if the equation s ≈ t is derivable from the following inference rules.s =𝐸 t - semantic ⊨, algebra. An algebra A is a model of an ES 𝐸 if every equation in 𝐸 is valid in A. We write s =𝐸 t if s ≈ t is valid in all models of 𝐸.
What's: equational system VS equational theory?
equational system equational theory - all possible equations in ES
What's the validity problem? Equational system
Whether s ≈ t belongs to the equational theory generated by ES. Rephrased in syntactical terms, the validity problem for E is the question whether the relation ≈E is computable.
What's the name of this ES?
Combinatory Logic. Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any me…
How would you show that: equation belongs to the equational theory of 𝐸 VS equation doesn't belong to the equational theory of 𝐸? Consider the ES 𝐸 consisting of the three equations
equation belongs - build a proof tree equation doesn't belong - find a counterexample algebra
A𝒱 denotes { all possible assignments }, what's: A 𝒱?
A - { carrier of the algebra } 𝒱 - { variables } It's A𝒱 because if:A = { true, false }𝒱 = { x, y, z }A𝒱 = { 23 possible assignments }