Transcript inductive-revisited

Inductive definitions revisited
 Generated and Freely generated sets
o Pattern match, unification
o Syntax-directed definitions (of semantics, ..)
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
1
Generated & freely generated sets
Generated set: Least set that
• includes certain constants
• closed under certain operations
(may require elements of some given sets)
Examples:
• N generated from 0, succ,
• N generated from 0, 1, addition
• Int list generated from integers, [], ::
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
2
Each element has expression tree
• Leaves labeled by constants/ elements of given
sets
• Internal nodes labeled by operations
Can be formulated as inductive definition
expression tree isomorphic to proof tree
Freely generated: each element has unique tree
Example: N generated from 0, succ
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
3
Every domain of labeled trees is freely generated
A label ~ an operation to construct trees
--- a constructor
Examples:
• all data types of OCAML
• abstract syntax trees
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
4
Properties of freely generated domains:
• inductively defined functions are always welldefined (explains their use in functional pl’s)
• Membership is decidable
• Pattern: expression p that has constants and
variables as leaves, constructors as internal nodes
• Pattern match: given expression E, pattern p, is there
a variable assignment that maps p to E
 , s.t.  ( p )  E ?
Has a simple algorithm
(Result is the satisfying assignment, or FAIL)
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
5
• Unification: (a generalization of pattern matching)
Given two patterns, is there a variable assignment
that makes them equal? (and, is there a best one?)
Used in theorem provers, logic programming (prolog),
and in type inference (ML)
Has an (almost) linear time algorithm
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
6
Of interest to us:
Goal resolution for semantics relations (d , ) inductively
defined over abstract syntax (a freely generated set)
The semantics is
syntax-directed
• The rules are organized by syntax classes
Allows to select for each expression candidate applicable rules
(pattern match)
• Conditions in the rules allow to select a unique new goal for recursive
calls – no backtracking
• The goals in premises of a rule are sub-expressions of the goal in the
rule’s head
– Each recursive call of next, natEval has a smaller argument
 termination is guaranteed
where do we use here the free generation?
Catriel Beeri Pls/Winter 2004/5
inductive-revisited
7