Scheme - abstract syntax, carriers and constructors

Author

abstract syntax, carriers and constructors

Marlene Miller

2007-03-11, 7:13 pm

Suppose we have a grammar for an abstract syntax.
t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t

Some people say t is a set of phrases; the grammar is an inductive
definition; the same set can also be defined constructively as a union of
sets defined recursively (as in TAPL 3.2).

However, is a grammar only the names of some as yet undefined sets and
signatures of some as yet undefined functions? Do we have to start by
specifying a universe of phrases that is bigger than what we want, define
some functions on tuples of phrases, appeal to the least fixed point theorem
to restrict the functions and then define the sets as the values of the
functions?

I am wondering how these two ways of describing abstract syntax are related.
My guess is to define the sets of abstract phrases, we need a bigger set
from which to get our elements (such as the set of all strings with balanced
parentheses).

Pascal Bourguignon

2007-03-12, 4:18 am

"Marlene Miller" <marlenemiller@worldnet.att.net> writes:

> Suppose we have a grammar for an abstract syntax.
> t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t
>
> Some people say t is a set of phrases; the grammar is an inductive
> definition; the same set can also be defined constructively as a union of
> sets defined recursively (as in TAPL 3.2).

Yes, these notations are equivalent, they define the same set of
phrases.

> However, is a grammar only the names of some as yet undefined sets and
> signatures of some as yet undefined functions?

A grammar is a definition of the set, as would be a definition given
in terms of set, or an in extension enumeration of the elements (for
finite languages/sets).

A language is a set of "words" (what you call "phrases" and some call
"sentences"), nothing more, nothing less.

> Do we have to start by
> specifying a universe of phrases that is bigger than what we want, define
> some functions on tuples of phrases, appeal to the least fixed point theorem
> to restrict the functions and then define the sets as the values of the
> functions?

Well, this is a way. But note that you may have some difficulty in
defining this bigger set. In particular, you don't want to give such
a lousy definition of it that it contains itself... So you're reduced
to give a construction of it, so you could as well do the same for the
set/language you're concerned with in the first place. But otherwise,
indicator functions are also another way to define a set. Remember
that functions themselves are nothing else than sets. So you are
still defining sets using sets.

For example, imagine I consider as universe

U = ( p, {p}, {'(',')'}, { p ::= '(' p ')' , p ::= <empty> } )

(I define here the set U as a grammar (start, non-terminals, terminals, productions)).

and then I define a filter:

f : U ----> { true, false }
<empty> |---> true
'(' ')' |---> false
'(' w ')' |---> (not (f w))

Well, wouldn't have been simplier to directly define the set f as:

f = ( p, {p}, {'(',')'}, { p ::= '(' '(' p ')' ')' , p ::= <empty> } )

?

> I am wondering how these two ways of describing abstract syntax are related.
> My guess is to define the sets of abstract phrases, we need a bigger set
> from which to get our elements (such as the set of all strings with balanced
> parentheses).

They are simply related in that they are just different way to express
the same idea of sets and set construction.

--
__Pascal Bourguignon__ http://www.informatimago.com/
Un chat errant
se soulage
dans le jardin d'hiver
Shiki

Sponsored Links