Title: Theory / Unimportant / CS / Fundamental / Practical Foundations for Programming Language{ / 1 - Judgments and Rules
Tags: récupéré hasSeenConjDef

Name: Surface syntax
Definition: how phrases are entered and displayed on a computer
Chapter: 1
Name2: Concrete syntax

Name: Structural syntax
Definition: The structure of phrases, specifically how they are composed from other phrases
Chapter: 1
Name2: Abstract syntax

Name: Abstract Syntax Tree
Definition: whose leaves are variables
Chapter: 1
Definition2: whose interior nodes are operators whose arguments are its children
Conjdef: A tree
Abbreviation: AST

Name: Binding structure of syntax
Definition: The part concerned with the introduction and use of identifiers:
Chapter: 1

Name: abstract binding trees
Definition: AST enriched with concepts of binding and scope
Chapter: 1

Name: A variable
Definition: an unspecified, or generic, piece of syntax of a specified sort
Chapter: 1
Definition2: an&nbsp unknown object drawn from some domain

Name: An operator
Definition: Something which has an arity specifying the sort of the operator and the number and sorts of its arguments
Chapter: 1

Name: A sort
Definition: One way to classify AST
Chapter: 1
Example: Expression
Example2: Command

Smaller0: P hold on each AST
Greater0: the property holds for any variable of this sort
Chapter: 1
Variables: \(P\) a property on AST
Smaller to greater: iff
Name: Structural induction
Greater1: for each \(o\) of arity \((s_1,\dots,s_n)s\), and \(a_i\in\mathcal A[\mathcal X]_{s_i}\),
if \(P(a_i)\) then \(o(a_1;\dots;a_n)\)

Name: A set of sorts
Chapter: 1
Notation: \(\mathcal S\)

Name: An arity
Definition: \((s_1,\dots,s_n)s\), with \(s,s_i\in\mathcal S\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts

Name: The sort of this arity
Definition: \(s\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts
\((s_1,\dots,s_n)s\) an arity

Name: The \(i\)-th of this sort
Definition: \(s_i\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts
\((s_1,\dots,s_n)s\) an arity

Name: The set of variables of sort \(s\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts
\(s\in\mathcal S\) an arity
Notation: \(\mathcal X_s\)

Definition: \(\{\mathcal X_s\}_{s\in\mathcal S}\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts
Notation: \(\mathcal X\)

Name: A fresh variable for \(\mathcal X\)
Definition: A variable \(x\not\in \mathcal X_s\) for any sort \(s\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts,
\(\mathcal X=\{\mathcal X_s\}_{s\in\mathcal S}\) a set of variables

Name: A variable of sort \(s\)
Definition: An element of \(\mathcal X_s\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts,
\(\mathcal X=\{\mathcal X_s\}_{s\in\mathcal S}\) a set of variables
\(s\in\mathcal S\)

Definition: the family of sets of variables obtained by adding \(x\) to \(\mathcal X_s\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts,
\(\mathcal X=\{\mathcal X_s\}_{s\in\mathcal S}\) a set of variables
\(s\in\mathcal S\)
\(x\) fresh
Notation: \(\mathcal X,x\)

Definition: \(x\in X_s\) belongs to \(A[X_s]\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts,
\(\mathcal X=\{\mathcal X_s\}_{s\in\mathcal S}\) a set of variables
\(s\in\mathcal S\)
\(x\) fresh
Notation: \(\mathcal{A[X]}\)
Definition2: for each \(o\) of arity \((s_1,\dots,s_n)s\), and \(a_i\in\mathcal A[\mathcal X]_{s_i}\), \(o(a_1;\dots;a_n)\in\mathcal A[\mathcal X]_s\)
Conjdef: The smallest family
Denoted by: \(\{\mathcal{A[X}_s]\}_{s\in\mathcal S}\)

Definition: \(b\) if \(x=a\)
Chapter: 1
Variables: \(\mathcal S\) a set of sorts,
\(\mathcal X=\{\mathcal X_s\}_{s\in\mathcal S}\) a set of variables
\(s,s'\in\mathcal S\)
\(a\in\mathcal {A[X},x]_{s'}\)
\(b\in\mathcal {A[X]}_s\)
Notation: \([b/x]a\)
Kind: , Theo
Definition2: \(y\) if \(y\in\mathcal X_s\) and \(y\ne a\)
Conjdef: By induction
Definition3: \(o([b/x]a_1;\dots;[b/x]a_n)\) if \(a=o(a_1;\dots;a_n)\)
Typ: \(\mathcal {A[X]}_{s'}\)
Applied to3: result of substituting \(b\) for every occurrence of \(x\) in \(a\)