A syntax checker for an extended subset of Scheme, logically

For consistency with the previous definitions of recursive procedures, let us specify the syntax checker logically, with one judgment per non-terminal.

• The Scheme value v denotes a well-formed list of toplevel forms whenever the following judgment holds:

  (%toplevel-forms v)
  

• The Scheme value v denotes a well-formed toplevel form whenever the following judgment holds:

  (%toplevel-form v)
  

• The Scheme value v denotes a well-formed definition whenever the following judgment holds:

  (%definition v)
  

• The Scheme value v denotes a well-formed list of expressions whenever the following judgment holds:

  (%expressions v)
  

• The Scheme value v denotes a well-formed variable whenever the following judgment holds:

  (%variable v)
  

• The Scheme value v denotes a well-formed expression whenever the following judgment holds:

  (%expression v)
  

• The Scheme value v denotes a well-formed else-clause whenever the following judgment holds:

  (%else-clause v)
  

• The Scheme value v denotes a well-formed list of cond-clauses whenever the following judgment holds:

  (%cond-clauses v)
  

• The Scheme value v denotes a well-formed list of case-clauses whenever the following judgment holds:

  (%case-clauses v)
  

• The Scheme value v denotes a well-formed list of let-bindings whenever the following judgment holds:

  (%let-bindings v)
  

• The Scheme value v denotes a well-formed list of let*-bindings whenever the following judgment holds:

  (%letstar-bindings v)
  

• The Scheme value v denotes a well-formed list of letrec-bindings whenever the following judgment holds:

  (%letrec-bindings v xs)
  

• The Scheme value v denotes a well-formed quotation whenever the following judgment holds:

  (%quotation v)
  

• The Scheme value v denotes well-formed formal parameters whenever the following judgment holds:

  (%lambda-formals v)
  

These judgments are defined with the following proof rules, where for narrative fluidity we occasionally write “x is blah” instead of “x denotes blah”. Caveat emptor.

• The syntax-checking relation for a list of toplevel forms:

  TOPLEVEL_FORMS_NIL
  	(%toplevel-forms '())

  TOPLEVEL_FORMS_CONS	(%toplevel-form tlf)	(%toplevel-forms tlfs)
  	(%toplevel-forms (cons tlf tlfs))

  Let us review these two rules:

  • The first rule, TOPLEVEL_FORMS_NIL, says that the empty list is a well-formed list of toplevel forms.
  • The second rule, TOPLEVEL_FORMS_CONS, says that if tlf denotes a well-formed toplevel form and if tlfs denotes a well-formed list of toplevel forms, then the list (cons tfl tlfs) is a well-formed list of toplevel forms.

• The syntax-checking relation for a toplevel form:

  TOPLEVEL_FORM_DEFINITION	(%variable x)	(%expression e)
  	(%toplevel-form (list 'define x e))

  TOPLEVEL_FORM_EXPRESSION	(%expression e)
  	(%toplevel-form e)

  Let us review these two rules:

  • The first rule, TOPLEVEL_FORM_DEFINITION, says that if x denotes a well-formed variable and e a well-formed expression, then the list (list 'define x e) is a well-formed toplevel form.
  • The second rule, TOPLEVEL_FORM_EXPRESSION, says that if e denotes a well-formed expression, then it also denotes a well-formed toplevel form.

• The syntax-checking relation for a list of expressions:

  EXPRESSIONS_NIL
  	(%expressions '())

  EXPRESSIONS_CONS	(%expression e)	(%expressions es)
  	(%expressions (cons e es))

  Let us review these two rules:

  • The first rule, EXPRESSIONS_NIL, says that the empty list is a well-formed list of expressions.
  • The second rule, EXPRESSIONS_CONS, says that if e denotes a well-formed expression and es a well-formed list of expressions, then the list (cons e es) denotes a well-formed list of expressions.

• The syntax-checking relation for a variable:

  VARIABLE		if x is a symbol that is not a keyword
  	(%variable x)

  This rule says that a symbol that is not a keyword is a well-formed variable.

• The syntax-checking relation for an expression:

  EXPRESSION_NUMBER		if n is a number
  	(%expression n)

  EXPRESSION_BOOLEAN		if b is a number
  	(%expression b)

  EXPRESSION_CHARACTER		if c is a character
  	(%expression c)

  EXPRESSION_STRING		if s is a string
  	(%expression s)

  EXPRESSION_VARIABLE	(%variable x)
  	(%expression x)

  EXPRESSION_TIME	(%expression v)
  	(%expression (list 'time e))

  EXPRESSION_IF	(%expression e1)	(%expression e2)	(%expression e3)
  	(%expression (list 'if e1 e2 e3))

  EXPRESSION_AND	(%expressions es)
  	(%expression (cons 'and es))

  EXPRESSION_OR	(%expressions es)
  	(%expression (cons 'or es))

  EXPRESSION_COND	(%cond-clauses cs)
  	(%expression (cons 'cond cs))

  EXPRESSION_CASE	(%expression e)	(%case-clauses cs)
  	(%expression (cons 'case (cons e cs)))

  EXPRESSION_LET	(%let-bindings let-bindings)	(%expression e)
  	(%expression (list 'let let-bindings e))

  EXPRESSION_LETSTAR	(%letstar-bindings letstar-bindings)	(%expression e)
  	(%expression (list 'letstar letstar-bindings e))

  EXPRESSION_LETREC	(%letrec-bindings letrec-bindings '())	(%expression e)
  	(%expression (list 'letrec letrec-bindings e))

  EXPRESSION_BEGIN	(%expression e)	(%expressions es)
  	(%expression (cons 'begin (cons e es)))

  EXPRESSION_QUOTE	(%quotation q)
  	(%expression (list 'quote q))

  EXPRESSION_LAMBDA	(%lambda-formals fs)	(%expression e)
  	(%expression (list 'lambda fs e))

  EXPRESSION_TRACE_LAMBDA	(%variable x)	(%lambda-formals fs)	(%expression e)
  	(%expression (list 'trace-lambda x fs e))

  EXPRESSION_APPLICATION	(%expression e)	(%expressions es)
  	(%expression (cons e es))

  All of these rules are structural.

• The syntax-checking relation for a list of cond-clauses:

  COND_CLAUSES_NIL	(%else-clause c)
  	(%cond-clauses (list c))

  COND_CLAUSES_CONS	(%cond-clause c)	(%cond-clauses cs)
  	(%cond-clauses (cons c cs))

  These two rules are structural.

• The syntax-checking relation for an else-clause:

  ELSE_CLAUSE	(%expression e)
  	(%else-clause (list (list 'else e)))

  This rule is structural.

• The syntax-checking relation for a cond-clause:

  COND_CLAUSE_INCONSEQUENTIAL	(%expression e)
  	(%cond-clause (list e))

  COND_CLAUSE_SIMPLE	(%expression e0)	(%expression e1)
  	(%cond-clause (list e0 e1))

  COND_CLAUSE_BINDING	(%expression e0)	(%expression e1)
  	(%cond-clause (list e0 '=> e1))

  These three rules are structural.

• The syntax-checking relation for a list of case-clauses:

  CASE_CLAUSES_NIL	(%else-clause c)
  	(%case-clauses (list c))

  CASE_CLAUSES_CONS	(%case-clause c)	(%case-clauses cs)
  	(%case-clauses (cons c cs))

  These two rules are structural.

• The syntax-checking relation for a case-clause:

  CASE_CLAUSE	(%quotations qs)	(%expression e)
  	(%case-clause (list qs e))

  This rule is structural.

• The syntax-checking relation for a list of let-bindings:

  LET_BINDINGS	(%let-bindings_aux bs xs)
  	(%let-bindings bs)

  This rule uses the auxiliary relation %let-bindings_aux. The judgment (%let-bindings_aux bs xs) holds whenever bs denotes a well-formed list of let-bindings that declare the distinct variables listed in xs.

  The rule LET_BINDINGS says that if bs denotes a well-formed list of let-bindings that declare the distinct variables listed in xs, then bs denotes a well-formed let header.

• The auxilary syntax-checking relation for a list of let-bindings:

  LET_BINDINGS_AUX_NIL
  	(%let-bindings_aux '() '())

  LET_BINDINGS_AUX_CONS	(%let-bindings_aux bs xs)	(%let-binding b xs x)
  	(%let-bindings_aux (cons b bs) (cons x xs))

  These two rules are structural:

  • The first rule, LET_BINDINGS_AUX_NIL, says that the empty list is a well-formed list of let-bindings that declare the vacuously distinct variables listed in the empty list.

  • The second rule, LET_BINDINGS_AUX_CONS, says that

    • if bs denotes a well-formed list of let-bindings that declare the distinct variables listed in xs, and
    • if b denotes a well-formed let-binding that declares a variable x that does not occur among the distinct variables listed in xs,

    then the list (cons b bs) denotes a well-formed list of let-bindings that declare the distinct variables listed in (cons x xs).

• The syntax-checking relation for a let-binding:

  LET_BINDING	(%variable x)	(%expression e)	if x does not occur in xs
  	(%let-binding (list x e) xs x)

  This rule says that if x denotes a well-formed variable and if e denotes a well-formed expression, then (list x e) denotes a well-formed let-binding that declares a variable x that does not occur among the distinct variables listed in xs whenever this variable does not occur among these distinct variables.

• The syntax-checking relation for a list of letstar-bindings:

  LETSTAR_BINDINGS_NIL
  	(%letstar-bindings '())

  LETSTAR_BINDINGS_CONS	(%letstar-binding b)	(%letstar-bindings bs)
  	(%letstar-bindings (cons b bs))

  These two rules are structural.

• The syntax-checking relation for a letstar-binding:

  LETSTAR_BINDING	(%variable x)	(%expression e)
  	(%letstar-binding (list x e))

  This rule is structural.

• The syntax-checking relation for a list of letrec-bindings:

  LETREC_BINDINGS	(%letrec-bindings_aux '() bs ys)
  	(%letrec-bindings bs)

  This rule uses the auxiliary relation %letrec-bindings_aux. The intuition behind it is that for a list of letrec-bindings obtained by concatenating

  • the well-formed list of letrec-bindings b1s that declare the distinct variables listed in xs,
  • the putative list of letrec-bindings b2s, and
  • the list of distinct variables ys,

  the judgment (%letrec-bindings_aux xs b2s ys) holds whenever b2s is well-formed and declares the variables listed in ys, all of which are distinct and none of which is listed in xs.

  The rule LETREC_BINDINGS says that if bs denotes a well-formed list of letrec-bindings that declare the distinct variables listed in ys, then bs denotes a well-formed letrec header.

• The auxiliary syntax-checking relation for a list of letrec-bindings:

  LETREC_BINDINGS_AUX_NIL
  	(%letrec-bindings_aux xs '() '())

  LETREC_BINDINGS_AUX_CONS	(%letrec-binding xs b x)	(%letrec-bindings_aux (cons x xs) bs ys)	if x does not occur in ys
  	(%letrec-bindings_aux xs (cons b bs) (cons x ys))

  Let us review these two rules:

  • The first rule, LETREC_BINDINGS_AUX_NIL, says that the empty list of letrec-bindings is well formed and declares no variables.

  • The second rule, LETREC_BINDINGS_AUX_CONS, says that

    • if b is a well-formed letrec-binding that declares x and is prefixed by letrec-bindings that declare distinct variables listed in xs and
    • if bs is a well-formed list of letrec-bindings
      • that is prefixed by letrec-bindings declaring distinct variables listed in (cons x xs) and
      • that declares distinct variables listed in ys,

    then (cons b bs) is a well-formed list of letrec bindings that is prefixed by letrec-bindings declaring distinct variables listed in xs and that declares distinct variables listed in (cons x ys) whenever x does not occur in ys.

• The auxilary syntax-checking relation for a letrec-binding:

  LETREC_BINDING_LAMBDA	(%variable x)	(%lambda-formals fs)	(%expression e)	if x does not occur in xs
  	(%letrec-binding xs (list x (list 'lambda fs e)) x)

  LETREC_BINDING_TRACE_LAMBDA	(%variable x)	(%variable v)	(%lambda-formals fs)	(%expression e)	if x does not occur in xs
  	(%letrec-binding xs (list x (list 'trace-lambda v fs e)) x)

  Let us review these two rules:

  • The first rule, LETREC_BINDING_LAMBDA, says that if x is a well-formed variable, fs are well-formed formal parameters, and e is a well-formed expression, then (list x (list 'trace-lambda v fs e)) is a well-formed letrec-binding that declares x whenever x does not occur in xs.
  • The second rule, LETREC_BINDING_TRACE_LAMBDA, says essentially the same for trace-lambda-abstractions.

• The syntax-checking relation for a list of quotations:

  QUOTATIONS_NIL
  	(%quotations '())

  QUOTATIONS_CONS	(%quotation q)	(%quotations qs)
  	(%quotations (cons q qs))

  These two rules are structural.

• The syntax-checking relation for a quotation:

  QUOTATION_NUMBER		if n is a number
  	(%quotation n)

  QUOTATION_BOOLEAN		if b is a boolean
  	%quotation b)

  QUOTATION_CHARACTER		if c is a character
  	(%quotation c)

  QUOTATION_STRING		if s is a string
  	(%quotation s)

  QUOTATION_SYMBOL		if x is a symbol
  	(%quotation x)

  QUOTATION_NIL
  	(%quotation '())

  QUOTATION_CONS	(%quotation q1)	(%quotation q2)
  	(%quotation (cons q1 q2))

  These rules are structural.

• The syntax-checking relation for formal parameters:

  LAMBDA_FORMALS	(%lambda-formals_aux fs xs)
  	(%lambda-formals fs)

  This rule uses the auxiliary relation %lambda-formals_aux. The judgment (%lambda-formals_aux fs xs) holds whenever fs denotes well-formed formal parameters whose variables are all distinct and listed in xs.

  The rule LAMBDA_FORMALS says that if fs denotes well-formed formal parameters whose variables are all distinct and listed in xs, then fs denotes well-formed formal parameters.

• The auxiliary syntax-checking relation for formal parameters:

  LAMBDA_FORMALS_AUX_NIL
  	(%lambda-formals_aux '() '())

  LAMBDA_FORMALS_AUX_VARIABLE	(%variable f)
  	(%lambda-formals_aux f (list f))

  LAMBDA_FORMALS_AUX_CONS	(%variable f)	(%lambda-formals_aux fs xs)	if f does not occur in xs
  	(%lambda-formals_aux (cons f fs) (cons f xs)

  Let us review these two rules:

  • The first rule, LAMBDA_FORMALS_AUX_NIL, says that the empty list fits as well-formed formal parameters whose variables are listed in the empty list.
  • The second rule, LAMBDA_FORMALS_AUX_VARIABLE, says that if f is a well-formed variable, then f fits as well-formed formal parameters whose variables are listed in a singleton list containing this variable.
  • The third rule, LAMBDA_FORMALS_AUX_CONS, says that if f denotes a well-formed variable and if fs denotes well-formed formal parameters whose variables are distinct and listed in xs, then (cons f fs) denotes well-formal parameters whose variables are distinct and listed in (cons f xs) whenever f does not occur in xs.

Version

Created [14 Oct 2025]