Principles of Programming Languages

Abstract Syntax

Andrei Arusoaie1
1 Department of Computer Science
Outline

Alphabet. Lexical analysis. Parsing.

Parse Trees

Abstract syntax trees

Abstract syntax in Lean

IMP Language Demo

Sentences in a programming language

Which phrases are correct?

▶ int x; x = x + 2
▶ int x; x = x + 2;
▶ if (a > 0) then x = 1; else x = -1;
▶ (a > 0) ? x = 1 : x = -1;
Sentences in a programming language

Which phrases are correct?

▶ int x; x = x + 2
▶ int x; x = x + 2;
▶ if (a > 0) then x = 1; else x = -1;
▶ (a > 0) ? x = 1 : x = -1;
Sentences in a programming language

Which phrases are correct?

▶ int x; x = x + 2
▶ int x; x = x + 2;
▶ if (a > 0) then x = 1; else x = -1;
▶ (a > 0) ? x = 1 : x = -1;
Overview: alphabet, lexical analysis, syntax

▶ Alphabet: set of (allowed) symbols

▶ Lexical analysis: identify the sequence of symbols
constituting the words (or tokens)
▶ Lexical rules
▶ Syntax: describes which sequences of words constitute
“legal” phrases
▶ Grammars
Overview: alphabet, lexical analysis, syntax

▶ Alphabet: set of (allowed) symbols

▶ Lexical analysis: identify the sequence of symbols
constituting the words (or tokens)
▶ Lexical rules
▶ Syntax: describes which sequences of words constitute
“legal” phrases
▶ Grammars
Overview: alphabet, lexical analysis, syntax

▶ Alphabet: set of (allowed) symbols

▶ Lexical analysis: identify the sequence of symbols
constituting the words (or tokens)
▶ Lexical rules
▶ Syntax: describes which sequences of words constitute
“legal” phrases
▶ Grammars
Alphabet

The Alphabet of C from the Standard has 96 symbols:

▶ a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,
u,v,w,x,z
▶ A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,
U,V,W,X,Y,Z
▶ 0,1,2,3,4,5,6,7,8,9
▶ ! " # % & ’ ( ) * + , - . /
▶ : ; < = > ? [ \ ] ^ _ { | } ~
▶ Separators: space, horizontal and vertical tab, form feed,
newline
Lexical analysis

Problem: Given a sequence of characters, find the pieces with

assigned meaning from that sequence: words or tokens

Example:
▶ Input: if (a > 0) then x = 1; else x = -1;
▶ Output: if, (, a, >, 0,), then, x, =, 1,;, else, x, =, -1,;
▶ Tokens = pieces with assigned/identified meaning
Lexical analyzer (lexer) = a program that implements an
algorithm that solves the problem above
Lexical analysis

Problem: Given a sequence of characters, find the pieces with

assigned meaning from that sequence: words or tokens

Example:
▶ Input: if (a > 0) then x = 1; else x = -1;
▶ Output: if, (, a, >, 0,), then, x, =, 1,;, else, x, =, -1,;
▶ Tokens = pieces with assigned/identified meaning
Lexical analyzer (lexer) = a program that implements an
algorithm that solves the problem above
Lexical analysis

Problem: Given a sequence of characters, find the pieces with

assigned meaning from that sequence: words or tokens

Example:
▶ Input: if (a > 0) then x = 1; else x = -1;
▶ Output: if, (, a, >, 0,), then, x, =, 1,;, else, x, =, -1,;
▶ Tokens = pieces with assigned/identified meaning
Lexical analyzer (lexer) = a program that implements an
algorithm that solves the problem above
Lexical analysis

Problem: Given a sequence of characters, find the pieces with

assigned meaning from that sequence: words or tokens

Example:
▶ Input: if (a > 0) then x = 1; else x = -1;
▶ Output: if, (, a, >, 0,), then, x, =, 1,;, else, x, =, -1,;
▶ Tokens = pieces with assigned/identified meaning
Lexical analyzer (lexer) = a program that implements an
algorithm that solves the problem above
Example I - Lexical rules

▶ Integers: 6, 0, −2, +3
▶ The alphabet A = {+, −} ∪ N
▶ Lexical rules: used to describe atomic language
constructions: numbers, identifiers, . . .
▶ Lexical rules are expressed using regular grammars (see
Formal Languages, Compilers and Automata course)
▶ Regular expressions, a.k.a regex
▶ Regex for integers: [\+-]?\d+
Example I - Lexical rules

▶ Integers: 6, 0, −2, +3
▶ The alphabet A = {+, −} ∪ N
▶ Lexical rules: used to describe atomic language
constructions: numbers, identifiers, . . .
▶ Lexical rules are expressed using regular grammars (see
Formal Languages, Compilers and Automata course)
▶ Regular expressions, a.k.a regex
▶ Regex for integers: [\+-]?\d+
Example I - Lexical rules

▶ Integers: 6, 0, −2, +3
▶ The alphabet A = {+, −} ∪ N
▶ Lexical rules: used to describe atomic language
constructions: numbers, identifiers, . . .
▶ Lexical rules are expressed using regular grammars (see
Formal Languages, Compilers and Automata course)
▶ Regular expressions, a.k.a regex
▶ Regex for integers: [\+-]?\d+
Example I - Lexical rules

▶ Integers: 6, 0, −2, +3
▶ The alphabet A = {+, −} ∪ N
▶ Lexical rules: used to describe atomic language
constructions: numbers, identifiers, . . .
▶ Lexical rules are expressed using regular grammars (see
Formal Languages, Compilers and Automata course)
▶ Regular expressions, a.k.a regex
▶ Regex for integers: [\+-]?\d+
Example I - Lexical rules

▶ Integers: 6, 0, −2, +3
▶ The alphabet A = {+, −} ∪ N
▶ Lexical rules: used to describe atomic language
constructions: numbers, identifiers, . . .
▶ Lexical rules are expressed using regular grammars (see
Formal Languages, Compilers and Automata course)
▶ Regular expressions, a.k.a regex
▶ Regex for integers: [\+-]?\d+
Parsing

Problem: how to combine the tokens in (valid) sentences?

▶ Answer: we define the grammar of the language
▶ Noam Chomsky: generative grammar
▶ Grammars allow us to transform a program given as a
sequence of characters into a syntax tree
▶ Parser = program which attempts to do this transformation
▶ Only valid programs can be parsed!
Parsing

Problem: how to combine the tokens in (valid) sentences?

▶ Answer: we define the grammar of the language
▶ Noam Chomsky: generative grammar
▶ Grammars allow us to transform a program given as a
sequence of characters into a syntax tree
▶ Parser = program which attempts to do this transformation
▶ Only valid programs can be parsed!
Parsing

Problem: how to combine the tokens in (valid) sentences?

▶ Answer: we define the grammar of the language
▶ Noam Chomsky: generative grammar
▶ Grammars allow us to transform a program given as a
sequence of characters into a syntax tree
▶ Parser = program which attempts to do this transformation
▶ Only valid programs can be parsed!
Parsing

Problem: how to combine the tokens in (valid) sentences?

▶ Answer: we define the grammar of the language
▶ Noam Chomsky: generative grammar
▶ Grammars allow us to transform a program given as a
sequence of characters into a syntax tree
▶ Parser = program which attempts to do this transformation
▶ Only valid programs can be parsed!
Parsing

Problem: how to combine the tokens in (valid) sentences?

▶ Answer: we define the grammar of the language
▶ Noam Chomsky: generative grammar
▶ Grammars allow us to transform a program given as a
sequence of characters into a syntax tree
▶ Parser = program which attempts to do this transformation
▶ Only valid programs can be parsed!
Example II - Grammar

▶ Language of palindromic strings using symbols a and b

▶ The alphabet A = {a, b}
▶ Can we describe palindromes using regex?
Example II - Grammar

▶ Language of palindromic strings using symbols a and b

▶ The alphabet A = {a, b}
▶ Can we describe palindromes using regex?
Example II - Grammar

▶ Language of palindromic strings using symbols a and b

▶ The alphabet A = {a, b}
▶ Can we describe palindromes using regex?
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ How do we “formally” describe palindromic strings?

▶ Note that there is a simple recursion in a palindromic string
▶ Base: a and b are palindromic strings
▶ Recursion: if s is a palindromic string then so are asa and
bsb
▶ Examples: “aba”, “aabaa”, “bab”, etc.
▶ Problem? Yes: “aa”, “abba”.
▶ Fix: add the empty string to base, hereafter denoted by ϵ
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Example II - Grammar

▶ Base case:
▶ P→ϵ
▶ P→a
▶ P→b
▶ Recursion:
▶ P → aPa
▶ P → bPb
▶ Context-free grammar (you study this in your compiler
course!)
Backus-Naur Form (BNF)

▶ Meta-language introduced by Backus and Naur to define

ALGOL60
▶ Vocabulary:
▶ Terminals: simple language strings; typically: tokens or
symbols
▶ Non-terminals: complex language constructions
Backus-Naur Form (BNF)

▶ Meta-language introduced by Backus and Naur to define

ALGOL60
▶ Vocabulary:
▶ Terminals: simple language strings; typically: tokens or
symbols
▶ Non-terminals: complex language constructions
Backus-Naur Form (BNF)

▶ Meta-language introduced by Backus and Naur to define

ALGOL60
▶ Vocabulary:
▶ Terminals: simple language strings; typically: tokens or
symbols
▶ Non-terminals: complex language constructions
BNF - example I

▶ Palindromic strings:
P ::= ϵ (1)
| a (2)
| b (3)
| a P a (4)
| b P b (5)
Derivations

▶ How to obtain a derivation: read the production as rewrite

rules and find a finite sequence of rewrite steps

▶ Example: derivation for abba

P →4 aPa →5 abPba →1 abba
Parse trees

▶ Derivation: P →4 aPa →5 abPba →1 abba

▶ Parse tree:
▶ contains nodes labeled with terminals, nonterminals, and ϵ

P
/|\
/ | \
a P a
/|\
/ | \
b P b
|
|
e
Parse trees

▶ Derivation: P →4 aPa →5 abPba →1 abba

▶ Parse tree:
▶ contains nodes labeled with terminals, nonterminals, and ϵ

P
/|\
/ | \
a P a
/|\
/ | \
b P b
|
|
e
BNF - example II

▶ Simple expressions language:

Int ::= [\+-]?[0-9]+
Exp ::= Int
| Exp "+" Exp
| Exp "*" Exp
| Exp "/" Exp
| "(" Exp ")"
Multiple parses available

Possible parse trees for 2 + 4 + 6:

Exp Exp

Exp + Exp Exp + Exp

Int Exp + Exp Exp + Exp Int

2 Int Int Int Int 6

4 6 2 4
Multiple parses available

Possible parse trees for 2 + 4 + 6:

Exp Exp

Exp + Exp Exp + Exp

Int Exp + Exp Exp + Exp Int

2 Int Int Int Int 6

4 6 2 4
Ambiguities

Possible parse trees for 2 + 4 + 6:

Exp Exp
Exp + Exp Exp + Exp
Int Exp + Exp Exp + Exp Int
2 Int Int Int Int 6
4 6 2 4

▶ Solutions?
▶ Use the parentheses defined in the syntax: ‘(’ and ‘)’
▶ Encode some kind of associativity: left or right
Ambiguities

Possible parse trees for 2 + 4 + 6:

Exp Exp
Exp + Exp Exp + Exp
Int Exp + Exp Exp + Exp Int
2 Int Int Int Int 6
4 6 2 4

▶ Solutions?
▶ Use the parentheses defined in the syntax: ‘(’ and ‘)’
▶ Encode some kind of associativity: left or right
Ambiguities

Possible parse trees for 2 + 4 + 6:

Exp Exp
Exp + Exp Exp + Exp
Int Exp + Exp Exp + Exp Int
2 Int Int Int Int 6
4 6 2 4

▶ Solutions?
▶ Use the parentheses defined in the syntax: ‘(’ and ‘)’
▶ Encode some kind of associativity: left or right
Priorities

Possible parse trees for 4 / 2 + 6:

Exp Exp
Exp / Exp Exp + Exp
Int Exp + Exp Exp / Exp Int
4 Int Int Int Int 6
2 6 4 2

▶ Which parse tree is correct in this case?

Priorities

Possible parse trees for 4 / 2 + 6:

Exp Exp
Exp / Exp Exp + Exp
Int Exp + Exp Exp / Exp Int
4 Int Int Int Int 6
2 6 4 2

▶ Which parse tree is correct in this case?

Priorities

Possible parse trees for 4 / 2 + 6:

Exp Exp
Exp / Exp Exp + Exp
Int Exp + Exp Exp / Exp Int
4 Int Int Int Int 6
2 6 4 2

▶ Which parse tree is correct in this case?

Priorities

NO YES
Exp Exp
Exp / Exp Exp + Exp
Int Exp + Exp Exp / Exp Int
4 Int Int Int Int 6
2 6 4 2
Solutions:
▶ Establish priorities between various constructs
▶ Filtering vs. modifying the grammar
Abstract Syntax Trees

▶ Grammars define concrete syntax

▶ Arithmetic expressions:

▶ 1 + 2 – infix notation
▶ (+ 1 2) – prefix notation
▶ (1 2 +) – postfix notation
▶ Each variant has a particular grammar production:
▶ E → E + E // infix
▶ E → + E E // prefix
▶ E → E E + // postfix
Abstract Syntax Trees

▶ Grammars define concrete syntax

▶ Arithmetic expressions:

▶ 1 + 2 – infix notation
▶ (+ 1 2) – prefix notation
▶ (1 2 +) – postfix notation
▶ Each variant has a particular grammar production:
▶ E → E + E // infix
▶ E → + E E // prefix
▶ E → E E + // postfix
Abstract Syntax Trees

▶ Grammars define concrete syntax

▶ Arithmetic expressions:

▶ 1 + 2 – infix notation
▶ (+ 1 2) – prefix notation
▶ (1 2 +) – postfix notation
▶ Each variant has a particular grammar production:
▶ E → E + E // infix
▶ E → + E E // prefix
▶ E → E E + // postfix
Abstract syntax trees

▶ Variants:
▶ 1 + 2 – infix notation
▶ (+ 1 2) – prefix notation
▶ (1 2 +) – postfix notation
▶ Parse trees:

infix prefix postfix

E E E
/|\ /|\ /|\
/ | \ / | \ / | \
1 + 2 + 1 2 1 2 +
Abstract syntax trees

▶ Variants:
▶ 1 + 2 – infix notation
▶ (+ 1 2) – prefix notation
▶ (1 2 +) – postfix notation
▶ Parse trees:

infix prefix postfix

E E E
/|\ /|\ /|\
/ | \ / | \ / | \
1 + 2 + 1 2 1 2 +
Abstract syntax trees

▶ Parse trees:

infix prefix postfix

E E E
/|\ /|\ /|\
/ | \ / | \ / | \
1 + 2 + 1 2 1 2 +
▶ Abstract representation of all the above trees:

add
/ \
/ \
1 2
Abstract syntax trees

▶ Parse trees:

infix prefix postfix

E E E
/|\ /|\ /|\
/ | \ / | \ / | \
1 + 2 + 1 2 1 2 +
▶ Abstract representation of all the above trees:

add
/ \
/ \
1 2
Abstract Syntax Trees

▶ Grammars define concrete syntax

▶ An AST is a tree representation of the structure of a
program where syntactical details are abstracted away
▶ For instance, addition has the same abstract tree even if
the concrete syntax differs across languages (e.g., C vs.
Haskell)
▶ Compilers use ASTs as the main data structure
Example: arithmetic expressions

AST for 2 + (4 + 6):

plus inductive Exp where
| number : Nat → Exp
| plus : Exp → Exp → Exp

2 plus instance : Coe Nat Exp where

coe := [Link]

#check ([Link] 2 ([Link] 4 6))

4 6 -- [Link] 2 ([Link] 4 6) : Exp
Abstract Syntax in Lean

The BNF grammar of arithmetic expressions:

▶ E ::= nat | E + E | E * E
The corresponding Lean encoding is:
inductive Exp : Type where
| num : Nat → Exp
| plus : Exp → Exp → Exp
| mul : Exp → Exp → Exp
Abstract Syntax in Lean

The BNF grammar of arithmetic expressions:

▶ E ::= nat | E + E | E * E
The corresponding Lean encoding is:
inductive Exp : Type where
| num : Nat → Exp
| plus : Exp → Exp → Exp
| mul : Exp → Exp → Exp
Instances

Complicated:

#check ([Link] ([Link] 1) ([Link] 2))

open Exp
#check plus (num 1) (num 2)

Less complicated:

instance : OfNat Exp n where

ofNat := [Link] n

#check (plus 1 2)
Instances

Complicated:

#check ([Link] ([Link] 1) ([Link] 2))

open Exp
#check plus (num 1) (num 2)

Less complicated:

instance : OfNat Exp n where

ofNat := [Link] n

#check (plus 1 2)
Notations
inductive Exp : Type where
| num : Nat → Exp
| var : String -> Exp
| plus : Exp → Exp → Exp
| mul : Exp → Exp → Exp
open Exp

instance : OfNat Exp n where

ofNat := [Link] n
#check (plus 1 2)

instance : Coe String Exp where

coe := var

#check (plus "x" 2)

infixl:50 " +' " => plus

infixl:40 " *' " => mul

#check 1 +' "x"

IMP

Demo
▶ Arithmetic expressions
▶ Boolean expressions
▶ Statements
IMP: BNF Syntax
▶ Arithmetic Expressions:
AExp ::= n | v | AExp "+" AExp | AExp "*" AExp
...

▶ Boolean Expressions:
BExp ::= "true" | "false"
| AExp "<=" AExp
| "!" BExp
| BExp "&&" BExp
| BExp "||" BExp
▶ Statements:
Stmt ::= "skip"
| String ":=" AExp
| Stmt ";" Stmt
| "if" BExp "then" Stmt "else" Stmt
| "while" BExp "do" Stmt
IMP: BNF Syntax
▶ Arithmetic Expressions:
AExp ::= n | v | AExp "+" AExp | AExp "*" AExp
...

▶ Boolean Expressions:
BExp ::= "true" | "false"
| AExp "<=" AExp
| "!" BExp
| BExp "&&" BExp
| BExp "||" BExp
▶ Statements:
Stmt ::= "skip"
| String ":=" AExp
| Stmt ";" Stmt
| "if" BExp "then" Stmt "else" Stmt
| "while" BExp "do" Stmt
IMP: BNF Syntax
▶ Arithmetic Expressions:
AExp ::= n | v | AExp "+" AExp | AExp "*" AExp
...

▶ Boolean Expressions:
BExp ::= "true" | "false"
| AExp "<=" AExp
| "!" BExp
| BExp "&&" BExp
| BExp "||" BExp
▶ Statements:
Stmt ::= "skip"
| String ":=" AExp
| Stmt ";" Stmt
| "if" BExp "then" Stmt "else" Stmt
| "while" BExp "do" Stmt
IMP: Arithmetic Expressions

inductive AExp : Type where

| num : Nat → AExp
| var : String → AExp
| plus : AExp → AExp → AExp
| mul : AExp → AExp → AExp

open AExp
#check plus (num 3) (mul (var "x") (num 4))
-- (num 3).plus ((var "x").mul (num 4)) : AExp
Coercions

inductive AExp : Type where

| num : Nat → AExp
| var : String → AExp
| plus : AExp → AExp → AExp
| mul : AExp → AExp → AExp

open AExp
#check plus (num 3) (mul (var "x") (num 4))

instance : OfNat AExp n where

ofNat := num n
instance : Coe String AExp where
coe := var

#check plus 3 (mul "x" 4)

-- plus 3 ((var "x").mul 4) : AExp
Why Use Custom Notations?

Custom notations make code more readable and closer to

mathematical notation:

Without notation:
plus (plus (num 1) (num 2)) (num 3)

Notations:
infixl:65 " +' " => plus
infixl:65 " -' " => minus
infixl:70 " *' " => mul
infixl:70 " /' " => div

With notation:
1 +' 2 +' 3
Basic Infix Notation Syntax

Lean 4 provides three types of infix operators:

▶ infixl – left associative
▶ infixr – right associative
▶ infix – non-associative

General syntax:
infixl:precedence "operator" => function
Example: Arithmetic Expressions
inductive AExp : Type where
| num : Nat → AExp
| var : String → AExp
| plus : AExp → AExp → AExp
| mul : AExp → AExp → AExp
open AExp

instance : OfNat AExp n where

ofNat := num n
instance : Coe String AExp where
coe := var

infixl:65 " +' " => plus

infixl:65 " -' " => minus
infixl:70 " *' " => mul
infixl:70 " /' " => div

#check 1 +' 2 +' 3 -- plus (plus 1 2) : AExp → AExp

#check 2 *' 3 +' 4 -- plus (mul 2 3) : AExp → AExp
Precedence Levels

Higher numbers = tighter binding

▶ Multiplication at 70: binds tighter

▶ Addition at 65: binds looser

Example:
2 *' 3 +' 4
-- Parses as: (2 *' 3) +' 4
-- NOT as: 2 *' (3 +' 4)
Docs

Metaprogramming – declare and operate with syntax in Lean 4:

[Link]
lean4-metaprogramming-book/main/05_syntax.html
Associativity: Left vs Right

Left associative (infixl):

a +' b +' c -- means (a +' b) +' c

Right associative (infixr):

infixr:60 " ^' " => power

a ^' b ^' c -- means a ^' (b ^' c)

Non-associative (infix):
infix:50 " == " => equal

a == b == c -- ERROR: requires parentheses

Spaces in Notation

Spaces in the notation string matter!

-- Recommended: spaces around operator

infixl:65 " +' " => plus

-- Also works: no spaces

infixl:65 "+'" => plus

-- The spaces affect parsing!

1+' 2 -- works with no spaces
1 +' 2 -- works with spaces

Best practice: Include spaces for readability.

Prefix and Postfix Notations

Lean 4 also supports prefix and postfix notation:

Prefix:
prefix:75 "-' " => neg

#check -' x -- means (neg x)

Postfix:
postfix:80 "!" => factorial

#check n! -- means (factorial n)

More Complex Notations

For more complex syntax, use the notation command:

notation:65 a " + " b " + " c =>

plus (plus a b) c

notation:max "|" e "|" => abs e

notation "if" c "then" t "else" e =>

ite c t e

notation "let" x " := " v " in " body =>

(fun x => body) v
Summary

▶ Use infixl, infixr, or infix for operators

▶ Higher precedence numbers = tighter binding
▶ Choose precedence levels that match mathematical
intuition
▶ Include spaces in notation strings for clarity
▶ Use notation for complex syntax patterns
IMP: Boolean Expressions

inductive BExp : Type where

| btrue : BExp
| bfalse : BExp
| beq : AExp → AExp → BExp -- equality
| ble : AExp → AExp → BExp -- less or equal
| bnot : BExp → BExp -- negation
| band : BExp → BExp → BExp -- conjunction
| bor : BExp → BExp → BExp -- disjunction

open BExp

notation:70 a:70 " =' " b:71 => beq a b

notation:70 a:70 " <=' " b:71 => ble a b
prefix:75 "!' " => bnot
infixr:60 " &&' " => band
infixr:55 " ||' " => bor
IMP: Boolean Examples

-- Example: x = 5
#check "x" =' 5

-- Example: x <= y
#check "x" <=' "y"

-- Example: !(x = 0)
#check !' ("x" =' 0)

-- Example: (x <= 10) && (y = 5)

#check ("x" <=' 10) &&' ("y" =' 5)

-- Example: (x = 0) || (y > 0)
-- Note: y > 0 encoded as !(y <= 0)
#check ("x" =' 0) ||' (!' ("y" <=' 0))
IMP: Statements
inductive Stmt : Type where
| skip : Stmt
| assign : String → AExp → Stmt
| seq : Stmt → Stmt → Stmt
| ifthenelse : BExp → Stmt → Stmt → Stmt
| while : BExp → Stmt → Stmt

open Stmt

notation:2 var:2 " ::= " a:3 => assign var a

infixr:1 " ;; " => seq

▶ notation:2: the precedence of the entire notation

▶ var:2: minimum precedence for parsing var; accept operators
with precedence greater than 2 as part of var
▶ a:3: The minimum precedence for parsing a. Since 3 > 2, this
means a binds slightly tighter than var.
IMP: Statement Examples

-- Example: x := 5
#check "x" ::= 5

-- Example: x := x + 1
#check "x" ::= ("x" +' 1)

-- Example: x := 0 ;; y := 1
#check ("x" ::= 0) ;; ("y" ::= 1)

-- Example: if (x = 0) then y := 1 else y := 2

#check ifthenelse ("x" =' 0)
("y" ::= 1)
("y" ::= 2)
IMP: Program

The following program parses now in Lean:

def factorial : Stmt :=
("result" ::= 1) ;;
("counter" ::= "n") ;;
[Link] (!' ("counter" <=' 0)) (
("result" ::= ("result" *' "counter")) ;;
("counter" ::= ("counter" -' 1))
)

#check factorial
-- factorial : Stmt
Summary: IMP Language

▶ Arithmetic expressions: variables, numbers, operations

(+, -, *, /)
▶ Boolean expressions: comparisons (=, <=), logical
operations (¬, ∧, ∨)
▶ Statements:
▶ Assignment: x := e
▶ Sequence: s1 ;; s2
▶ Conditional: if b then s1 else s2
▶ Loop: while b do s
▶ All defined as inductive types in Lean
▶ Lean’s notation system makes code readable
▶ Will be used for defining semantics and proving properties!
Summary: IMP Language

▶ Arithmetic expressions: variables, numbers, operations

(+, -, *, /)
▶ Boolean expressions: comparisons (=, <=), logical
operations (¬, ∧, ∨)
▶ Statements:
▶ Assignment: x := e
▶ Sequence: s1 ;; s2
▶ Conditional: if b then s1 else s2
▶ Loop: while b do s
▶ All defined as inductive types in Lean
▶ Lean’s notation system makes code readable
▶ Will be used for defining semantics and proving properties!
Summary: IMP Language

▶ Arithmetic expressions: variables, numbers, operations

(+, -, *, /)
▶ Boolean expressions: comparisons (=, <=), logical
operations (¬, ∧, ∨)
▶ Statements:
▶ Assignment: x := e
▶ Sequence: s1 ;; s2
▶ Conditional: if b then s1 else s2
▶ Loop: while b do s
▶ All defined as inductive types in Lean
▶ Lean’s notation system makes code readable
▶ Will be used for defining semantics and proving properties!
Summary: IMP Language

▶ Arithmetic expressions: variables, numbers, operations

(+, -, *, /)
▶ Boolean expressions: comparisons (=, <=), logical
operations (¬, ∧, ∨)
▶ Statements:
▶ Assignment: x := e
▶ Sequence: s1 ;; s2
▶ Conditional: if b then s1 else s2
▶ Loop: while b do s
▶ All defined as inductive types in Lean
▶ Lean’s notation system makes code readable
▶ Will be used for defining semantics and proving properties!