# Evolution of SASyLF 2008-2021

John Tang Boyland Work done in part while the author was in residence at
Northeastern University, Boston, MAUniversity of Wisconsin-Milwaukee
Milwaukee, Wisconsin, USA<EMAIL_ADDRESS>
###### Abstract

SASyLF was released in 2008 and used as a proof assistant in courses at
several universities. It proved itself useful and has continued to be used,
and each iteration of use has encouraged further development: fixing bugs and
adding enhancements. This paper describes how SASyLF was developed while
keeping true to its purpose. Most notable are making substitutions explicit,
support of “and” and “or,” support for mutual and lexicographic induction, and
IDE support.

##  1 Introduction

SASyLF (Second-order Abstract Syntax Logical Framework) is a proof assistant
based on LF using higher-order abstract syntax (HOAS) [12], but limited to
second-order, for notational simplicity. SASyLF was introduced in 2008 [2] by
Aldrich, Simmons and Shin. The project has a webpage (sasylf.org) hosted at
Carnegie Mellow and a page at github (https://github.com/boyland/sasylf/).

SASyLF has been used in courses based on Pierce’s Types and Programming
Languages [14] at Carnegie Mellon University, University of California at Los
Angeles, University of Wisconsin-Milwaukee, ETH Zurich, and Northeastern
University. The initial paper discusses some of the responses collected from
students, including that most felt that SASyLF helped them learn how to write
natural langauge proofs. The repeated interaction with new users exposes
previously unknown defects, underscores known mis-features and leads to
enhancement requests. This paper reports on the work completed (as of SASyLF
release 1.5.0) and the plans for the future.

The stated purpose of SASyLF was to provide a gentler learning curve to proof
mechanization for students within a type theory course, and secondarily for
researchers. The design philosophy of SASyLF was (and is) to follow
conventions of paper proofs as closely as possible, but also to make all the
steps explicit, so that errors could be easily pinpointed and expressed in
terms of these high-level concepts.

For example, when describing the structure of the language supporting the type
system, SASyLF follows paper conventions by having the user specify a context
free language, for example for the simply-typed lambda calculus with a “unit”
constant:

> $e$ | ::= | $\mathtt{\lambda}x\texttt{:}\tau\cdot e$
> ---|---|---
> | $|$ | $x$
> | $|$ |  $e$ $e$
> | $|$ | ()
>
>
>     syntax
>       e ::= fn x : tau => e[x]
>          | x
>          | e e
>          | "(" ")"
>

On the left, we give a typical presentation in a paper, and on the right, we
give the equivalent in SASyLF (from Figure 1 [2]). In this example, we see
that expressions (“e”) have four forms: lambda expressions, variables,
application and the unit constant (“()”). The parentheses for the unit
constant in SASyLF have to be quoted since parentheses have special meaning.
The other symbols (e.g., “:”) do not need to be quoted, but may be. The square
brackets in SASyLF (“`[.]`”) used in the definition of lambda expressions
express that the body of the lambda may have uses of variable “x” in it.
SASyLF supports higher-order abstract syntax (HOAS [12]) so that the user
doesn’t have to define complex name-based substitution rules.

Another way that shows how SASyLF follows paper conventions for specifying
type systems is in the inference rules. For example, consider the declaration
of the typing judgment and one of its rules:

> (typing) Γ⊢e : τ
>
> *[Right=T-App] Γ ⊢ e1 : τ’ →τ
>
> Γ ⊢ e2 : τ’ Γ ⊢ e1 e2 : τ
>
>
>     judgment has-type: Gamma |- e : tau
>     assumes Gamma
>
>     Gamma |- e1 : tau -> tau
>     Gamma |- e2 : tau
>     ------------------------- t-app
>     Gamma |- e1 e2 : tau
>

The figure on the left is a typical presentation which shows the form of the
typing relation and then uses natural-deduction-style inference rules. On the
right, we express the same idea in SASyLF (adapted from Figure 2 [2]). The
only significant difference is that in SASyLF, the fact that “Gamma” includes
bindings that may be used in the expression is declared using “assumes.”

The Curry-Howard Correspondence highlights the connection between computation
and logic. In particular, a proof can be seen as a computational object, and
_vice versa_. The correspondence is often used to highlight the logical
foundations of programming, especially to mathematicians. In contrast, SASyLF
encourages the dual viewpoint by using programming as a metaphor for proof
construction. The purpose is to make the less familiar world of logical proofs
accessible to competent programmers. For example, if a proof uses a lemma, it
will use syntax strongly resembling a function call, and a proof by induction
is expressed with (functional) recursion. An example of a proof in SASyLF in
given in the next section in Figure 2.

As originally designed, SASyLF incorporated a number of aspects to help it
meet its design goals. In particular:

  * •

The syntax of the terms being studied is described with context-free grammars.
Syntactic terms and judgments are described syntactically and parsed using GLR
parsing [16].

  * •

Name binding is supported using Higher-Order Abstract Syntax (HOAS) within LF
[12].

  * •

Derivations are produced one step at a time (“let normal form”).

  * •

Incremental proof construction is aided by the ability to leave unspecified
part of the proof while continuing elsewhere.

Seeing all the struggles that compilers students have getting a grammar
accepted as LALR(1) (or LL(k)), it is refreshing that users in SASyLF simply
need to give a context-free grammar. Ambiguity need only be handled where it
occurs, primarily using parentheses. So for example, the following term is
ambiguous:

> fn x => x "(" ")" must be written
> fn x => (x "(" ")") or
> (fn x => x) "(" ")" .

The original SASyLF paper mused the addition of precedence declarations to
handle ambiguity, but this was never added. For pedagogical purposes, it seems
best to require that all ambiguity be explicitly avoided with parentheses; it
makes it clear that the various choices are different ASTs.

The use of HOAS has been mostly successful. The alternative, deBruijn
notation, is tricky to learn and even in its clearest exposition (“locally
nameless” [9]) requires several technical lemmas for every use of binding. In
HOAS, students mainly need only be aware of standard static scoping rules,
plus be cognizant of “alpha renaming,” the irrelevance of formal parameter
names. The hardest parts to explain are the restrictions on the “assumption
rule.”

The most serious problem with HOAS is that certain proof approaches are simply
not possible. For instance, it’s not possible to express that all types of
variables in a context have a certain property that is not shared by all
types. We have started the theoretical work on extending LF with new features
to support the necessary changes to the meta-language [5] but that work has
stalled.

In sharp contrast to most other proof assistants, SASyLF eschews the use of
“tactics,” powerful techniques for generating a proof automatically. At the
risk of gross generalization, tactics handle all the easy aspects of proofs
but leave the harder parts. This is the wrong approach for a novice, who lacks
the intuition for the easier parts, let alone the harder parts.

So it seems that SASyLF as designed has the right approach for educational
purposes; our approach to changes is to ensure that these goals are kept in
view. In the next section, we discuss the changes already made to SASyLF, and
in the following section look at changes that are under consideration.

##  2 Changes in SASyLF

The original paper anticipated further developments. For reference, they are
listed here with a brief comment on to what extent the anticipation was
realized.

  1. 1.

“[We] are developing an integrated development environment that will help both
novice and expert users write boilerplate code. For example, it will allow
students to drag a rule into a case analysis and have the syntactic structure
of the case for that rule generated automatically.”

Indeed, an Eclipse plugin for SASyLF was initiated within a short time and
this plugin has undergone numerous improvements. There is still no support for
“dragging” a rule into a case analysis, but perhaps better, a “Quick Fix” has
been provided which will populate a case analysis with all missing cases.

  2. 2.

“In the future we plan to support namespaces to allow a file to rely on
declarations from another file without worrying about name clashes.”

The module system is still basic, but does permit a proof to be used in
another proof without name clashes.

  3. 3.

“We have considered adding ‘by solve’ which would automatically search for a
derivation, but this poses challenges in terms of giving away a derivation to
students in an educational setting.”

Indeed “by solve” does introduce the equivalent of a simple tactic into
SASyLF. It was added as a project but hasn’t been maintained. Fortunately for
educational purposes, it can only find simple proofs.

  4. 4.

“However, there are a few checks that are not yet implemented, including the
checks for substitution, weakening, exchange, and contraction.”

Substitution, weakening and exchange were all fully checked soon after Boyland
took over maintenance. Contraction remains a reserved word, but nothing can be
proved “by contraction” (the justification is not even accepted by the
parser). Since contexts in SASyLF are (currently) inextricably bound up with
variable introduction, and since it is not legal to bind the same variable
twice ($\/\Gamma,x:T,x:T\vdash R[x]$ is not legal), contraction is not ever
applicable. The superficially similar situation ($\Gamma,x:T,y:T\vdash
R[x,y]$) can be already be reduced using “substitution” to ($\Gamma,x:T\vdash
R[x,x]$).

  5. 5.

“Although some cleanup work is needed, the implementation could eventually
serve another educational role: illustrating, through a translation from
paper-proof syntax into the LF type theory, the formal underpinnings of common
notation and some of the basic ideas behind LF-based theorem provers.”

We are not aware of any use of SASyLF for this purpose.

  6. 6.

“We believe Part 2B [of POPLmark] will also be feasible in SASyLF; Parts 1A
and 2A will require the implementation of mutual induction (not expected to be
hard to add since the type theory has already been worked out in Twelf).

Indeed mutual induction was added early on. It is _not_ needed for Part 2A,
but is needed for Part 1A with narrowing being proved inductively with
transitivity of algorithmic subtyping. Part 2A has been completely mechanized
in SASyLF, but Part 1A is currently not mechanizable due to the context
manipulation needed by narrowing.

  7. 7.

“This comment suggests the need for better visualizations of proofs—–at a
minimum, syntax highlighting, but perhaps output in LaTeX or a graphical
depiction of a derivation tree. Several students felt that a tree-like
presentation of a derivation was easier to read than the linear format
supported by the tool.”

The IDE includes syntax highlighting which is a big help to avoid some simple
syntax errors, but graphical views have not been implemented. Nor has there
been any demand for them, since the original paper, to our knowledge.

  8. 8.

“Most …students still did have times when they wished they had better
feedback, for example real-time feed-back on syntax errors and incorrect rule
applications, rather than continually rerunning the tool, which was
‘disruptive and annoying.’ IDE integration could help with such issues.”

Indeed, anecdotally, the IDE has been very helpful to students, although some
used the command-line version occasionally.

In the remainder of this section we discuss the changes that actually have
been put into effect, as of SASyLF 1.5.0, starting with Eclipse plugin.

Figure 1: Screenshot of SASyLF 1.5.0 under Eclipse.

###  2.1 Eclipse Plugin

Programmers expect IDE support while coding, and to continue the
identification of proving with coding, SASyLF developers soon provided support
in an Eclipse plugin. Incrementally, new features have been added. While
editing, users will notice

  * •

an outline view,

  * •

syntax highlighting,

  * •

parenthesis matching,

  * •

automated indentation,

  * •

error and warning markers,

  * •

folding and unfolding of proof segments,

  * •

content assist (e.g. lemma name completion).

Some of these features can be seen in Figure 1. The plugin provides a number
of capabilities:

  * •

Checking proofs;

  * •

Addition/removal of comments;

  * •

Quick fixes of many kinds of errors;

  * •

Finding the definition of a theorem;

  * •

Changing syntax highlighting colors (“dark” mode available);

Unlike common plugins, such as for Java, the syntax is not checked on every
keystroke. The checking process is still non-incremental and so is done only
on a save, or on demand (e.g., pressing the green check-mark in the tool bar).

One of the most consequential aspects of the plugin is the “Quick Fix” system.
For many errors, the error marker in the left ruler contains a “light bulb”
icon (see Figure 1). Clicking on that, or using the “Quick Fix” keyboard
short-cut brings up a dialog in which one can select a fix. For missing cases
(as this error is), the plugin will add the cases which the proof is currently
missing. Indeed this feature is so powerful, that it is recommended to _not_
inform students of its existence for the first few weeks, so students will
write their own case analyses.

The proof engine of SASyLF (which can be run from the command line) is
architecturally separated from the Eclipse plugin architecture. Indeed the
“smarts” of “Quick Fix” are available from the command-line, enabling
enterprising students to use SASyLF with vim or IntelliJ.

###  2.2 Syntactic Comparison

SASyLF 1.5.0 accepts almost all legal proofs written in the original syntax,
but provides features not originally available. Figure 2 contrasts Figure 4
from the 2008 paper with a proof more idiomatic in current SASyLF.

    theorem preservation: forall dt: * |- e : tau
                          forall ds: e -> e’
                          exists * |- e’ : tau.
    dt’: * |- e’:tau                   by induction on ds :
      case rule
        d1 : e1 -> e1’
        -------------------- c-app-l
        d2 : e1 e2 -> e1’ e2
      is
        dt’ : * |- e’ : tau        by case analysis on dt :
          case rule
            d3 : * |- e1 : tau’ -> tau
            d4 : * |- e2 : tau’
            -------------------------- t-app
            d5 : * |- (e1 e2) : tau
          is
            d6 : * |- e1’ : tau’ -> tau
                         by induction hypothesis on d3, d1
            dt’: * |- e1’ e2 : tau by rule t-app on d6, d4
          end case
        end case analysis
      end case

      case rule... // case for rule c-app-r is similar

      case rule
        d1 : e2 value
        ---------------------------------------- r-app
        d2 : (fn x : tau’ => e1[x]) e2 -> e1[e2]
      is
        dt’ : * |- e’ : tau       by case analysis on dt :
          case rule
            d4 : * |- fn x : tau’ => e1[x] : tau’’ -> tau
            d5 : * |- e2 : tau’’
            ----------------------------------------- t-app
            d6 : * |- (fn x : tau’ => e1[x]) e2 : tau
          is
            dt’ : * |- e’ : tau    by case analysis on d4 :
              case rule
                d7: *, x:tau’ |- e1[x] : tau
                -------------------------------------- t-fn
                d8: * |- fn x:tau’ => e1[x] : tau’ -> tau
              is
                d9: * |- e1[e2] : tau by substitution on d7, d5
              end case
            end case analysis
          end case
        end case analysis
      end case
    end induction
    end theorem

    theorem preservation :
        // Unicode identifiers and operators supported
        forall d: * $\vdash$ t : T
        forall e: t $\to$ t’
        exists * $\vdash$ t’ : T // “.” not required

        // Induction can be declared separately
        use induction on d

        // “proof” serves instead of repeating goal
        proof by case analysis on e:
            case rule
                e1: t1 $\to$ t1’
                --------------------- E-App1
                _: (t1 t2) $\to$ (t1’ t2)
                where t := t1 t2 and t’ := t1’ t2
                // “where” makes substitution explicit
            is
                // “and” allows proving things together
                d1: * $\vdash$ t1: T’ $\to$ T and
                d2: * $\vdash$ t2: T’ by inversion on d
                // “inversion” does a single case analysis

                d1’: * $\vdash$ t1’: T’ $\to$ T
                  by induction hypothesis on d1, e1
                proof by rule T-App on d1’, d2
            end case

            case rule ... // case E-App2 is similar

            case rule
                v2: t2 value
                -------------------------- E-AppAbs
                _: ($\mathtt{\lambda}$ x:T’. t11[x]) t2 $\to$ t11[t2]
                where t := ($\mathtt{\lambda}$ x:T’. t11[x]) t2
                 and t’ := t11[t2]
                // “.” can be used in syntax, e.g., in lambdas
            is
                d1: * $\vdash$ $\mathtt{\lambda}$ x:T’.t11[x] : T’’$\to$T and
                d2: * $\vdash$ t2 : T’’ by inversion on d
                d11: *, x:T’ $\vdash$ t11[x] : T
                     by inversion on d1
                     where T’’ := T’
                // inversions can cause substitutions too

                proof by substitution on d11, d2
            end case
        end case analysis
    end theorem

Figure 2: Comparing Fig. 4 from [2] (left) to more idiomatic expression in
SASyLF 1.5.0 (right).

The new proof has italicized comments highlighting the main differences.
Another difference is that the names of nonterminals and rules is closer to
that used in Pierce’s TAPL [14].

The change that makes the new proof _longer_ (otherwise, it is noticeably
shorter) is the addition of optional “where” clauses [3]. This addition has an
important explanatory value: it makes explicit how meta-variables (such as
`T’’`) are changed by the pattern match. We found that students new to proof
mechanization often are unaware of how pattern matching changes the identity
of meta-variables. And not only novices. For instance, the answer to exercise
9.3.9 on pages 506 and 507 the first edition of TAPL incorrectly presumed that
(the equivalent of) `T’` and `T’’` were identical in the E-AppAbs case, when
that identification only happens later when the typing relation for the lambda
expression is inverted.

The other changes here can be seen as conveniences, generalizations and
extensions of the original SASyLF features.

###  2.3 Conjunction and Disjunction

In SASyLF, a theorem or lemma has a single judgment as a result; if two
results are desired they must be packaged together in a single judgment.
Sometimes a choice result is desired; for example in an introductory type
systems course, students prove “progress” with the result that a term is
either a value _or_ can be evaluated in a further step.

Conjunction and disjunction can be done easily through the introduction of new
judgments: A
BA  and  B

AA  or  B

BA  or  B Ignoring contexts for now, nothing more at the meta-level is needed
for conjunction to work. The system as implemented currently creates these
judgments automatically (conjunctions or disjunctions of two or more judgments
at a time) on demand. As a special case, the (new) keyword `contradiction` is
parsed an empty disjunction.111The other use of the new keyword is the
justification “by contradiction on” which refers to an empty case analysis.

A technical difficulty with disjunctions arises when one considers that the
implicit arguments of a rule includes all free meta-variables of the premises
or conclusion. In the case of conjunction, all meta-variables in the
conclusion are present in the premises, but in the case of a disjunction,
meta-variables free in one disjunct but not in another need to be supplied
even when the latter is being used to satisfy the disjunction. For a simple
example, consider a typical “progress” theorem, which proves that a term $t$
is a value or that is evaluates $t\to t^{\prime}$. The question is what should
$t^{\prime}$ be for the disjunction if $t$ is a value?

Since meta-variables in SASyLF are never dependently typed, and they are
described with context-free grammars, the types are always inhabited assuming
that the non-terminal is _productive_ , which is a simple recursive check.
Unproductive nonterminals are arguably errors in the specification, and so
SASyLF was updated to mandate that all non-terminals be productive. That
simple change is enough for the meta-theory to accommodate conjunctions and
disjunctions of judgments without contexts.

If a conjunction is proved by a lemma or theorem (or inversion), the syntax
requires that the separate judgments be split and named separately, as seen in
in Fig. 2 in two cases of inversion. This obviates the need for an explicit
elimination rule for conjunctions. Conjunctions are introduced by simply
listing the two parts as in “`proof by d1, d2`.”

In contrast, using a disjunction needs case analysis, as seen in this excerpt
from the “progress” theorem from the mechanization of iso-recursive subtyping
from the public repository:

>
>     ns1: t1 value or t1 -> t1’
>         by induction hypothesis on d1
>     _: t1 t2 -> t’ by case analysis on ns1:
>         case or e1: t1 -> t1’ is
>             e: t1 t2 -> t1’ t2 by rule E-App1 on e1
>         end case
>         ...
>

The syntax doesn’t require that the whole (implicitly created) rule is given,
it is necessary only to provide the particular disjunct being handled.
Introducing a disjunction is done by proving one of the disjuncts, or a
disjunction of a subset of them.

Joining judgments with contexts interacts with the meta-theory because the
context is not actually part of the judgment. As a result, a rule declaration
can only produce a judgment with an opaque context (e.g., Gamma). The premises
must use this context, possibly adding extra requirements. For example the
typical T-Abs rule has the form *[Right=T-Abs]Γ, x:T ⊢t[x] : T’Γ⊢λx:T . t[x] :
T →T’ The meta-level expression of this rule is *[Right=T-Abs]Πx:t.typing[x,T]
→typing[t[x],T’] typing[lam[T,t],arr[T,T’]] This form uses typing for the LF
type of the typing judgment, square brackets $[\ldots]$ for application of
arguments to an LF function or dependent type, and $\Pi{x:T}.T^{\prime}[x]$
for dependently-typed function types (and traditional function type syntax
$T\to T^{\prime}$ when the result type is independent of the argument type).
The constants lam and arr are the constructors of lambda expressions and arrow
types respectively in the syntax being described. Here we distinguish the (LF)
type of terms t from a meta-variable and implicit argument to the rule
$t$.222Some readers may notice that, against representation norms, we don’t
give $t$ in “eta-expanded” form when we pass it to lam. Internally, the eta-
expanded form is used.

So the question is how do we represent the result of a hypothetical canonical
forms lemma for arrow types?

$\mathtt{t=\lambda x:T.t1[x]\texttt{ and }*,x:T\vdash t1[x]:T^{\prime}}$

In this case, only one judgment uses a context (the equality judgment here
only operates on closed terms), and so we can just pull the entire context out
and generate the conjoined judgment with the single rule:

$\inferrule*[Right={\textup{{Eq+T}}}]{\mathtt{t_{\\_}1=t_{\\_}2}\\\
\mathtt{\Gamma\vdash t_{\\_}3:T}}{\mathtt{t_{\\_}1=t_{\\_}2\texttt{ and
}\Gamma\vdash t_{\\_}3:T}}$

Then our example can be rendered as follows where the LF context is pulled to
the outer level:

$\Pi{x:\mathtt{t}}.\mathtt{typing}[x,T]\to\texttt{Eq+T}[t,\texttt{lam}[T,t_{\\_}1],t_{\\_}1[x],T^{\prime}]$

The excess context will not affect the equality judgment in the premise, since
it does not depend on the context.

A similar approach can be used if multiple judgments use the same context and
the conjunction of the derivations all use the same derivation, but what if we
have a version of the last example where equality needs the context?

$\mathtt{\Gamma\vdash t=\lambda x:T.t1[x]\texttt{ and }\Gamma,x:T\vdash
t1[x]:T^{\prime}}$

In this case, pulling out the context to the top would cause the equality
judgment to depend on the bindings. The solution is to create a special
judgment with a single rule that can add the needed binding just for typing
judgment:

$\inferrule*[Right={\textup{{T*V}}}]{\Pi{x:\mathtt{t}}.\mathtt{typing}[x,T_{\\_}1]\to\texttt{typing}[t_{\\_}2[x],T_{\\_}3]}{\texttt{T*V}[T_{\\_}1,t_{\\_}2,T_{\\_}3]}$

Then the desired conjunction can be represented as

$\texttt{Eq+T*V}[t,\texttt{lam}[T,t_{\\_}1],T,t_{\\_}1,T^{\prime}]$

The same approach can be used to conjoin judgments that use different contexts
as long only one them builds on unknown bindings in the LF context. This
restriction is moot since SASyLF already bans a theorem (or lemma) or judgment
from having two contexts.

Once the meta-theory was handled, what remained was to check the contextual
parts that are not handled by the meta-theory (naming of contexts) and to
provide implicit coercions to hide the existence of the constructed judgments
and rules.

###  2.4 Syntactic Sugar

It is common in presentations of type systems to give multiple letters for use
as meta-variables, for example for types:

$S,T\>{::=}\>\texttt{A}\mid S\to T\mid S+T$

The grammar for SASyLF had “space” for this extension, so it was added. Around
the same time, short-cut definitions were added so that one can write

$\textrm{id}\>{:=}\>\mathtt{\lambda x.x}$

The operator `:=` is used because we are not defining a new non-terminal, but
rather defining a short-hand.

In the same vein, _derived syntax_ can be defined. It differs from the latter
in having non-terminal parameters:

$\mathtt{(t_{\\_}1\texttt{; }t_{\\_}2)\>{:=}\>(\lambda
x:\texttt{Unit}.t_{\\_}2)t_{\\_}1}$

The numbering ensures that the terms are substituted in the correct order. The
left-hand side must be parenthesized to avoid parsing ambiguity, and is
defensible as one is defining the syntax as a whole.

Derived syntax was easy to add to the system, as it simply added some new
productions to the concrete syntax used in the generalized LR parser.

###  2.5 Induction

The fundamental danger with recursion is non-termination, and the
corresponding problem with proofs using induction is circular reasoning. And
so induction can only be permitted if the recursion can be shown to always
terminate. The standard way to prove termination is with a “measure” that is
_reduced_ in every call. The measure needs to be a _well-founded_ partial
order, that is, it has no infinite decreasing chains.

In computer science, _structural_ induction is the fundamental induction
technique in proofs. It uses the structure of terms: an inductive call with
one term is a reduction of the current call if the new term is a sub-term of
the current one. Since all terms are (by definition) finite, this measure is
guaranteed to be well-founded. SASyLF uses structural induction with both
syntax terms and judgments. A premise used in the rule used to prove judgment
instance is a sub-term.

This basic concept is complicated by higher-order terms, from binders and from
assumptions. We generalized SASyLF’s rules of structure induction on HOAS to
follow those of Twelf. The Twelf User Manual [13] describes restrictions
sufficient to ensure soundness.

This discussion of structural induction permits us now to discuss the user-
visible extensions to SASyLF. One of the earliest additions to SASyLF was
mutual induction. Theorems (and lemmas) can be connected into a mutual
induction group through the keyword “`and`” and then (forward) references
within the group are allowed as long as inductive argument is reduced. And
backward references are allowed additionally even if the inductive argument is
unchanged.

An immediate issue is that how does one theorem “know” what the induction
argument of another theorem is? In the original SASyLF, induction was only
indicated in a form of case analysis. But the proof of a mutually inductive
theorem may not need any case analysis, and forcing a case analysis would
needlessly complicate the proof. And so mutual inductive theorems were
assigned their first argument as the inductive argument, by default, if there
is no explicit induction declaration.

Some time after mutual induction was added, new syntax was added to permit
induction to be declared separate from case analysis:

> use induction on $d$

For backward compatibility (for the vanishing small SASyLF community), the
implicit induction on the first argument was preserved. This implicit
induction has been deprecated in SASyLF 1.5.0; all mutually inductive theorems
and all theorems using induction (explicit or implicit) must have an explicit
declaration of induction to avoid a warning.

The new syntax for declaring induction gave “space” to extend structural to
lexicographical induction (as seen in the example proof of “cut-elimination”):

> use induction on A, d1, d2

This powerful induction technique permits induction to seek a reduction in d1
if A stays the same, and further to look for a reduction in d2 if the first
two are unchanged. What makes this reduction measure powerful is that if A is
reduced, then d1 and d2 are unrestricted; they can get arbitrarily bigger.

Another common induction situation is where arguments are swapped in a use of
induction. Proofs of transitivity of algorithmic subtyping often have such a
situation when handling contravariant type constructors such as in function
types. SASyLF was extended to support “unordered” induction (as seen in the
example proof of composition of hierarchical substitution in LF):

> use induction on {$\mathtt{\alpha}$0, $\mathtt{\alpha}$2}, s2

This example uses lexicographical induction in which the first argument is an
unordered induction of the two “simple types” ($\mathtt{\alpha
0},\mathtt{\alpha 2}$), and the second is a substitution judgment (s2).
Unordered induction requires that under some permutation of the elements,
every element reduces or stays the same, with at least one element reducing.
The possibility for permutation makes it strictly more powerful than the
similar induction schema in Twelf, which is just a special case of
lexicographic induction.

The LF hereditary substitution composition example involves mutual induction
as well. All theorems in a mutual induction group must declare induction of
the same form (same number, groupings and type).

###  2.6 Special cases

A useful programming idiom (especially in imperative programming) is to handle
a special case before a more involved computation, because then the more
involved computation does not need to take into the special case that has
already been handled. A similar situation can happen with proofs: there may be
a case for one of the inputs to a theorem that if handled ahead of time, the
rest of the proof can be easier. These special cases are unremarkable in
informal proofs, but don’t fit well into a formulation based on functional
programming.

_Partial case analysis_ in SASyLF 1.5.0 can be used to handle such situations.

>
>     do case analysis on ...:
>       ...
>     end case analysis
>

A partial case analysis on a subject has the same kind of cases and the same
proof obligation as the surrounding context, but it need only handle a subset
of the possible cases. Importantly, the system “remembers” that the cases are
already handled and so later in the same context if there is case analysis on
the same subject, the cases that are already handled can (and indeed must) be
omitted. In particular “by inversion” (only one case) and “by contradiction”
(no cases) may be possible when they would not be, previous to the partial
case analysis.

Partial case analysis was first introduced as a way to reduce case explosion,
but it has served as a useful tool for working around incompleteness in
higher-order unification. The mechanization of recent work on iso-recursive
subtyping [17] gives an example. The canonical forms lemma for arrow type says
that if we have a value of arrow type then the value has the form of a lambda
abstraction. The problem is that the typing judgment includes an “unfolding”
possibility:

$\inferrule*[Right={T-Unfold}]{\mathtt{T=(\mu X.T_{\\_}1[X])}\\\
\mathtt{\Gamma\vdash
t:T}}{\mathtt{\Gamma\vdash\texttt{unfold}\,(T)\,t:T_{\\_}1[T]}}$

Recall that the SASyLF term $\mathtt{T_{\\_}1[T]}$ is represented with LF term
application. The problem is that there is no MGU for the unification problem
$T_{\\_}1[T]\stackrel{{\scriptstyle?}}{{=}}\texttt{arr}[T_{\\_}2,T_{\\_}3]$.
Thus if a SASyLF proof attempts to do a case analysis on a proof of
$\mathtt{\Gamma\vdash t:T_{\\_}2\to T_{\\_}3}$, the possibility of the
T-Unfold rule leads to an “incomplete unification” error.

The work-around, is to “disguise” the arrow type in an equality judgment, do a
partial case analysis handling the problematic rules (such as T-Unfold) and
then afterwards invert the equality judgment and proceed as normal.

###  2.7 Relaxation

The notation that SASyLF supports for using judgments from the LF context only
handles the case where the assumption is the last one added, for example:

$\inferrule*[Right={T-Var}]{}{\mathtt{\Gamma,x:T\vdash x:T}}$

Then “weakening” can be used to add more assumptions after the one used. This
semantics is supported by the meta-theory when creating a judgment instance.

But pattern matching does not proceed as cleanly. In Twelf, pattern matching
cannot reach into the LF context. Instead if one needs to prove a meta-theorem
for which a case can be in the LF context, one needs to place an instance of
the theorem being proved in the context along with the assumption. This idiom
is peculiar to Twelf and not close to how one does the proof on paper.

Instead SASyLF permits case analysis to operate on the context. The problem is
that it uses the rule which positions the assumption at the end of the
context. For example, if we are writing a substitution lemma that does case
analysis on $\mathtt{\Gamma,x:T_{\\_}2\vdash t[x]:T_{\\_}1}$, then as well as
the case that t[x] is x (which is handled without needing to reach into
$\mathtt{\Gamma}$), we have the additional case:

$\inferrule*[Right={T-Var}]{}{\mathtt{\Gamma^{\prime},x^{\prime}:T_{\\_}1,x:T_{\\_}2\vdash
x^{\prime}:T_{\\_}1}}$

The case apparently implies that
$\mathtt{\Gamma=\Gamma^{\prime},x^{\prime}:T_{\\_}1}$, in other words, that
the new assumption we found was at the end of the LF context. In the case of
the simply-typed lambda calculus, this implication is fine since assumptions
can be freely permuted. But in some type systems, the assumptions cannot be
permuted, for example in the presence of type variables, as in
$F_{\\_}{\leq}$.

Indeed, one can construct a “proof” of a contradiction in SASyLF if the
apparent implication is permitted to have validity (see bad38.slf in the
public SASyLF repository). Thus case analysis in the context needs proper
support in the meta-theory. This support is provided in the concept of
“relaxation.”

The simple idea at the kernel of relaxation is that rather than saying that
the current context is _equal_ to the new (smaller) context with the
assumption at the end, the current context _includes_ the new context with the
assumption:

$\mathtt{\Gamma\geq\Gamma^{\prime},x^{\prime}:T_{\\_}1}$

Then any judgment defined in the context on the right can be moved back to
$\Gamma$ through _relaxation_ , a form of weakening, although new assumptions
are not explicitly added. In the process of relaxation, the variable
$\mathtt{x^{\prime}}$ is disguised by being replaced with $\mathtt{t[\ldots]}$
(the parameter `x` is known to be unused and so can be replaced with anything
in scope). Furthermore relaxation gives no status to any intermediate
assumptions (the “$\mathtt{x:T_{\\_}2}$” in the example). In general there
could many assumptions between the one found in the pattern analysis and the
known assumptions at the end.

The semantics we give here is a stop-gap until contexts are properly brought
into the meta-theory (see the “Future Work” section).

###  2.8 Making Substitutions Explicit

As mentioned briefly earlier in this work, and as described in much more
detail in a separate paper [3], “where” clauses make explicit the implicit
substitution of meta-variables. This change is the biggest syntactic change to
the original SASyLF but also completely in line with the purposes of the
system: making proofs explicit, especially for pedagogical purposes. SASyLF
does not require that these “where” clauses are given, unless a certain option
is turned on. (In the IDE, the option is on by default.)

As originally implemented, and as described in the paper cited above, the
extension had no effect on the operation of the rest of SASyLF; it didn’t need
to be part of the “trusted core.” The substitutions found were strictly
_descriptive_.

This aspect is mainly preserved, but in some situations, especially with
inversion, the result of the substitution does not have a user-provided
presentation, _except_ in the “where” clauses. For example (from `good40.slf`
in the public repository):

>
>     theorem gt-anti-refl-use-w2:
>         forall n1
>         forall d: n1 > n1
>         exists contradiction .
>         use induction on n1
>         use inversion of rule gt-more on d
>           where n1 := s n
>         p: n > n by theorem succ-cancels-gt on d
>         proof by induction hypothesis on n, p
>     end theorem
>

This proof of the anti-reflexivity of `gt` is an inductive proof, in that it
makes a recursive call. Unusually, it doesn’t use an explicit case analysis.
Instead it uses inversion on the only rule matching the input. In the process,
we need a name for the natural number preceding `n1`. The “where” clause gives
the name “`n`” for this new variable. This means that the theorem input `d`
has type `s n > s n`. This judgment is passed to the theorem `succ-cancels-gt`
which can strip the `s` from both sides of the inequality. Then the result can
be used in the inductive call (for which `n` is a sub-term of `n1`).

###  2.9 Generalizing Inversion

The example just shown for “where” clauses also demonstrates one of the
generalization of inversion added to SASyLF: inversion can be performed solely
for the “side-effect” of the unification that it performs. The new syntax “use
inversion” is commonly used on equality judgments. Previously, one needed to
perform a case analysis which not only was wordy, but it also increased the
depth of the proof and its visual complexity. Now with “use inversion,” one
can simply invert the equality judgment in place and then assume the equality
in the remainder of the proof. This approach is much closer to how one would
reason informally.

Internally, the “use” syntax is implemented as proving an empty conjunction, a
tautology. This prevents a proof (case) from ending with a “use” line. The
same technique is used for the “use induction” syntax explained earlier.

As can also be seen, inversions can have associated “where” clauses (“further
work” in the “where” clause paper [3]). An interaction with another extension
was the ability to invert “or” judgments (when only one possibility remains,
usually because a partial case analysis eliminated the other possibilities).
The “obvious” syntax for such inversions is the clunky form:

> … by inversion of or on  $d$

The sequence of three two-letter keywords, each starting with “o” is visually
confusing. More on this problem below.

Separately, there was the need to invert syntax: if a non-terminal has only a
single (remaining) possibility, inversion is more attractive than case
analysis. While it is not common to define non-terminals with only a single
possibility, there are good reasons to do so, for example in our mechanization
of LF, we define a constructor identifier as a natural number: “`c ::= n`.”
More commonly, with partial case analysis, all but one possibility could have
already been handled. Again there’s a desire for inversion rather than
requiring a case analysis.

An inversion on syntax doesn’t use rules, and also doesn’t yield any
judgments, and so the syntax is simply:

> use inversion on nt where nt := form

Once this syntax was added, it was a short step further to permit it also for
inversion of judgments, making the identification of the rule optional. In
particular, inversion of an “or” judgment can simply by done “by inversion on”
the judgment instance, which avoids the unpleasing syntax, which is available
in SASyLF 1.5.0 but probably won’t be used too much.

###  2.10 Modules

Requiring all the elements of a proof to be in a single file is limiting.
Originally, SASyLF even required there to be a single syntax section, although
this restriction was lifted. Nonetheless, it’s inconvenient to have to (say)
include a definition of natural numbers (and especially all operations and
theorems about them) in every proof that uses them. It would also be desirable
to have a library of theorems about groups in general that could be applied to
any operation satisfying the group axioms. Thus it has been a long-term goal
to add some form of modules.

A syntax has been defined in which a SASyLF file can include a module header,
including a name, a sequences of requirements (syntax, judgments and lemmas)
and sequence of provided declarations. The requirements are often “abstract,”
that is, not defined. When a module is used, the requirements are substituted
with new elements. However, the syntax has run ahead of the meta-theory:
SASyLF 1.5.0 does not support using modules with requirements. But it does
support the use of modules without requirements and a nascent library has been
defined with modules for natural numbers and Boolean values.

An important design goal is that a proof should be syntactically independent
of the modules it uses: all syntax and judgments defined for the proof need to
be defined locally. So when syntax from a module is used, it must be locally
defined as well. This gives an option for an alternate syntax to be used, for
example:

> syntax n = Natural.n ::= 0 | 1+n

A similar situation applies to judgments:

> judgment nat-ne = Natural.notequal: n != n

Rules and theorems (and lemmas) can be used with name qualification. In case
analysis on an imported judgment, the rule names in the cases do not need to
be qualified (and doing so will occasion a warning).

SASyLF 1.5.0 uses a package system (whose syntax was defined but ignored in
the original SASyLF) and the `Natural` module is actually in the
`org.sasylf.util` package, and so the uses described above are not legal
unless one includes a local renaming of the module:

> module Natural = org.sasylf.util.Natural

An advantage of defining a shorthand is that the IDE will use it with content
assistance: If one types “by theorem Natural.ne-” and presses the content-
assist key (e.g., control-space), the system will suggest three possible
completions with their theorem headers in a helper popup window.

##  3 Future Work

In this section, we describe some of ideas for further extension. We cannot
commit to any of these plans, but all have been discussed to some extent, and
seem compatible with the original goals of SASyLF.

###  3.1 Support for Equality and Reduction in Theorem Output

Currently, if a theorem is able to show that two terms are the same, the only
way to communicate that fact to clients is to use an equality judgment. The
clients will then immediately invert the equality judgment. This extra step
has no counterpart in a textual proof, even one which carefully lists each
step. Rather the definition of equality is assumed. For a while, it seemed
that the best way forward would be to pre-define equality for user-defined
types and add extra support to handle the introduction and elimination. The
handling of contexts complicates the situation, and also the fact that the
judgment may “trespass” on syntax needed for other judgments (e.g., an
equality judgment used precisely to hide equality from the system temporarily
to avoid the incompleteness of higher-order unification).

The syntax of “where” clauses gives a way for equality to be separated from
judgments and given it own space. It seems attractive to permit “where”
clauses to declared in the obligation of a theorem, as in the following
hypothetical example of a uniqueness of addition theorem:

>
>     theorem plus-unique:
>         forall d3: n1 + n2 = n3
>         forall d4: n1 + n2 = n4
>         exists () where n3 := n4
>         ...
>     end theorem
>

Then one could write:

>
>     use theorem plus-unique on p, p’ where n := n’
>

Or perhaps even

> n := n’ by theorem plus-unique on p, p’

The latter syntax would then also be available to inversion as well.

The ability of a theorem to produce equalities would also make it easier for a
theorem to produce other non-judgment results as well, such as “reductions,”
which allow structural induction. For instance

>
>     theorem gt-reduces:
>         forall d: n1 > n2
>         exists () where n1 > n2
>         ...
>     end theorem
>

This theorem would prove that `n2` was a sub-term of `n1`.

Adding non-judgment obligations to theorems would affect the rest of the
justification system. It must be possible, then, for case analysis (both full
and partial) to produce these non-judgment outputs as well. The “`proof`”
syntax would need to include these extra obligations as well. And at the end
of a sequence of derivations, we must not only check the last derivation, but
also check the current substitution to see if the equality (or reduction) is
known. One must also consider whether one can use disjunction with reduction
ot equality.

###  3.2 Wildcards in Premises

The simple ability to give “by unproved” as the justification for any step may
seem trivial at first, but it is a big help for people writing proofs. Rather
than leaving an error in place, the form of the judgment is given. It can be
used and checked at later points. Proof “by unproved” permits proofs to be
constructed from the end, rather than forwards. First one determines what
needs to be proved. Then one determines what rule (or theorem) would produce
the desired result and what premises it would need. These can be defined and
justified “by unproved” and then the rule application can be checked.

Two students in a type systems class using SASyLF with different levels of
experience with provers independently suggested to extend this ability to
apply to partial rule applications. Currently, if anything is wrong with a
rule application, the whole judgment is flagged as an error, and since
unification is used to check the premises and conclusion together, it is hard
to pinpoint an error to a particular spot. The proposal is to permit a premise
to be replaced with `_` and then if the application is otherwise error-free,
only the missing part would be flagged:

>
>     da: Gamma |- t1 t2 : T’ by rule T-App on _, d2
>

The system may even have a suggestion as to the type of the missing
premise(s). This idea seems within the capabilities of the existing engine,
where each kind of justification would need to decide whether to support such
holes. Presumably case analysis and weakening would not need to support holes,
but rule/theorem application and conjunction creation would.333SASyLF 1.5.1
has implemented this requested feature through the “Quick Fix” system.

One of the students also suggested permitting such wildcards within a term in
case one is not quite sure what is proved, as in the following example:

>
>     da: Gamma |- t1 t2 : _ by rule T-App on d1, d2
>

Again the idea is that an error (or warning) would be generated with
information about the missing information. At an extreme level, one could
write:

>
>     da: _ by rule T-App on d1, d2
>

Here the user is not showing any indication of what the result should be at
all. From the first public release, SASyLF already in some cases will infer
the actual result and print it in an error message, depending on the error
encountered. So this ability seems well within the spirit of the tool.

###  3.3 Generalization of Contexts

The basic idea for handling contexts has not changed from the beginning: a
bound variable is associated with a single syntactic production of the
context, and this production is associated with an “assumption” rule of a
judgment that assumes the context.

The fact that an identifier is known to be a bound variable is due to it
occurring inside square brackets in the grammar (only variables may thus
appear), and the nonterminal in which the variable name occurs by itself in a
production indicates the syntactic restriction on the variable.

The production of the context nonterminal for a variable has a single
occurrence of a variable, a single (recursive) instance of the context
nonterminal, optionally some other nonterminal occurrences, and any number of
“noise” terminals.

The context nonterminal must have a single production with only terminals, and
otherwise can only have variable productions, one for each syntactic variable
form.

The assumption rule, unlike all other rules anywhere in the system includes a
single production of the context nonterminal in the conclusion. This
production must be the production for a variable, and must comprise the most
unrestricted form of that production. The assumption rule is permitted no
premises. The rest of the rule can use no nonterminals not occurring in the
context production, and must have at least one use of each nonterminal
occurring as well as exactly one use of the variable.

For instance, in the case of the simply-typed lambda-calculus, one can define:

>
>     syntax
>       t ::= lambda x:T . t[x] // x is a variable
>          | t t
>          | x      // x is of nonterminal t
>
>       G ::= *     // terminals only
>          | G, x:T // variable production for x
>
>     judgment typing: G |- t : T
>     assumes G
>
>       ------------- T-Var
>       G, x:T |- x:T  // verbatim use of variable production
>
>       $\vdots$
>

This information is used in the conversion of forms into LF. Each explicit
binder is converted into two levels of abstraction in LF. So for example the
form

>
>     G, x1: T -> T’ |- ...
>

is converted to

$\Pi{x_{\\_}1:\texttt{t}}.\Pi{d_{\\_}1:\texttt{typing}[x_{\\_}1,\texttt{arr}[T,T^{\prime}]]}.\ldots$

The second abstraction’s formal (here $d_{\\_}1$) is never used in the
internal form, and so one can use LF’s arrow type short-hand:

$\Pi{x_{\\_}1:\texttt{t}}.\,\texttt{typing}[x_{\\_}1,\texttt{arr}[T,T^{\prime}]]\to\ldots$

From this conversion, it can be seen why we need an assumption rule for the
variable production: it is needed for representation of the context.
Similarly, the fact that the assumption rule cannot mention other nonterminals
(not in the variable production) is clear for the same reason of
representation, they would be unbound. Premises for the rule would be
irrelevant since the assumption is a hypothetical, not a proof. The fact that
the context nonterminal needs a terminals-only production reflects the fact
that the empty context has no information. Multiple terminals-only productions
would be confusing since they would not be distinguished in the meta-theory.
But the remaining restrictions in the context and assumption rules are
potential points for extension. Lifting these restrictions would somewhat
increase the expressiveness of SASyLF without requiring any substantial
extensions in the meta-theory. We now turn to a far-reaching extension.

###  3.4 Contexts as Syntax

One of the restrictions that was discussed above is that a nonterminal must
either be identified as a context or as syntax. In the former case, it must
not be an object of “assumes” and it can serve as a binder of variables. In
the latter case, any judgment that mentions it must have a declaration that it
“assumes” the context nonterminal, and aside from highly restricted
“assumption” rules, all uses in conclusions of rules must be unrestricted.

This restriction can be lifted aside from two difficulties, one that could be
handled withing the current meta-theory but the other causing a major change.
The first, minor difficulty is how to handle variable productions, e.g., “`G,
x:T`,” because if the structure is not a context, then the variable is not
bound, and cannot be used. The easy, but unsatisfying answer us that the
variable can be simply ignored; it carries no information. For example suppose
we define a judgment on types that don’t use named variables: `T ground`. Then
with the restriction lifted we could defined a judgment that a context uses
only ground types:

>
>     judgment contextground: G ground
>
>       -------- G-Empty
>       * ground
>
>       G ground
>       T ground
>       --------------- G-Var
>       (G, x:T) ground
>

The main difficulty concerns when a single nonterminal is treated as a context
and as syntax in the same context. Some situations cannot be permitted: since
a judgment that “assumes” a context does not actually receive information
about the context, it cannot use a judgment that treats it as syntax:

>
>     G ground  //! cannot be permitted
>     G, x:T |- t[x] : T’
>     ----------------------------- T-AbsWrong
>     G |- lam x:T . t[] : T -> T’
>

Indeed such combinations if permitted would render weakening and exchange
unsound in general. The other way around is a situation in which a judgment
that does _not_ assume the context has a premise which does. This situation
contains some of the aspects discussed below, but is less interesting because
the context cannot be used by any of the other syntactic members of the
judgment.

The truly difficult mixing comes in a theorem which has premises which assume
the context and those that do not, for instance:

>
>     theorem ground-typing-implies-something:
>         forall d: G |- t : T
>         forall g: G ground
>         exists ...
>     end theorem
>

Since the second premise treats `G` syntactically, the theorem cannot assume
that it is represented in the LF context of the theorem. Instead, `G` must be
an implicit parameter of the theorem. The other premise is represented using
the context as an abstraction, or rather as a series of abstractions depending
on the size of `G`. LF does not have a way to represent a variable-length
series of abstractions. It cannot be represented by a single abstraction with
a compound argument because LF provides no way to extract pieces from compound
values. Preliminary work to extend LF with variable arity [5] was never
completed.

###  3.5 Parameterized Modules

With SASyLF 1.5.0, we finally have support for modules, albeit without
parameters. The syntax and basic idea of module parameters have already been
laid out. The module can “require” parameters, and then another proof can
instantiate the module with parameters

More details need working out before it makes sense to embark on designing a
new set of library modules using parameters: finding the best way to express
something, how can the system be made practical, making sure that the result
has a sound meta-theory. For all these reasons, development of modules has
been slow.

###  3.6 Subtyping in Syntax

In Pierce’s TAPL, values are routinely given as a sub-grammar of terms. SASyLF
does not support this idiom; if the examples from TAPL are typed in, they are
syntactically legal, but generate ambiguous parses wherever something could be
a value or a term. Updating SASyLF to support sub-grammars was identified as a
desirable extension in the first partial solution to the original POPLmark
challenge [4].

In this case, as opposed to some other desirable extensions, the meta-theory
of “refinement types” for LF is already completed [11]. As part of the
formalization, it uses intersection types (or rather “intersection sorts”).
Indeed, due to pattern matching, a meta-variable may found to be an element of
two sub-grammars (sorts) at once. This is rather awkward in SASyLF because the
name of a meta-variable is intrinsically bound up in its type: what do we do
with (say) $\mathtt{t^{\prime}_{\\_}2}$ when it is found to be a value? We
would need to update the system to remember what sorts a nonterminal is
(currently) known to inhabit. The current sorts would affect which productions
are needed for case analysis, perhaps generalizing the information used in
partial case analysis. The implementation of the meta-theory would also
require a major update to support sorts.

###  3.7 Co-induction

Proofs in SASyLF assume that syntax and judgments are finite; that structures
are defined through a least fixed-point of grammar production and rule
application. Generalizing this assumption is useful for the support of
coinduction. Kozen and Silva [10] give a good introduction to how coinduction
should be supported in informal proofs. This article should be a good guide
for extending SASyLF with coinduction, translating the category theory (e.g.,
the article defined a coinductive datatype as an element of the final
coalgebra of a polynomial endofunctor on Set) into practical rules.

The biggest obstacle to supporting coinduction over coinductive datatypes is
the need to support circular/infinite structures. SASyLF would need syntax to
create them, and the internal engine would need a major rewrite to support
these structures, in particular defining unification on coinductive structures
with variables. Furthermore, since these structures are typed in LF, it is
necessary to extend LF to operate on “co-terms.” It is not clear whether LF is
sound on co-terms.

##  4 Related Work

In this section, we review some of the other education proof systems
particularly interested in helping students construct their own proofs.

Lurch [6] is one example of a system with a similar mission as SASyLF, except
in the field of mathematics. It compares most similarly with SASyLF in aiming
to check proofs written in the idioms of paper proofs. It works as a “word
processor” similar to using SASyLF in an IDE. It provides the standard tools
of a rich text editor and indeed recently adds the ability to edit formulas in
a simplified text-based equation system (or even in LaTeX). The particular
ability of Lurch is that when parts of the text are selected as “meaningful,”
Lurch will check them. So if a mathematical statement such as “$\forall
x.x^{2}\geq 0$” is “meaningful”, it will expect this statement to be followed
by a proof, which is checked. It uses colored icons to indicate which
statements are proved, definitely wrong or simply unproved.

AXolotl [7] is a puzzle game for students to learn how to generate proofs
using quantified rules. The researcher (Cerna) recognized that students often
struggle with unification and substitution in rule application and includes
several aids to help students bridge the conceptual gap. Recently the tool has
been ported to work as a mobile application [8].

The Students’ Proof Assistant [15] takes a different approach. Rather than a
stand-alone tool, it is embedded within Isabella/HOL. Unlike the standard
Isabelle proof assistant, it keeps the entire tree of the a proof visible to
the student working on a proof. This feature makes it comparable to SASyLF,
despite the fact that it still supports tactics (being within the Isabelle
system). The researchers agree that it’s important for students learning to
write proofs to see structure of the proof being created.

People experienced in writing proofs can find writing the simple parts of
proofs tedious while people just introduced to proving need to work through
these details because everything is new. Paradoxically, the expert needs more
assistance than the newcomer (albeit only for productivity); in fact the
assistance can be a hindrance to the student learning how to prove.

##  5 Conclusion

In conclusion, SASyLF 1.5.0 carries on the vision of the original SASyLF paper
while firming up the foundation, and providing additional convenience. Some of
that convenience (e.g. “quick fixes” in the IDE) are best not highlighted at
the beginning of a course introducing SASyLF, so as to ensure that important
learning steps are not skipped. We anticipate that SASyLF will continue to
develop as long as it remains useful pedagogically.

## References

  * [1]
  * [2] Jonathan Aldrich, Robert J. Simmons & Key Shin (2008): _SASyLF: an educational proof assistant for language theory_.  In: Workshop on Functional and Declarative Programming in Education (FDPE 2008), ACM Press, New York, pp. 31–40, 10.1145/1411260.1411266.
  * [3] Michael D. Ariotti & John Tang Boyland (2017): _Making Substitutions Explicit in SASyLF_.  In: Logical Frameworks and Meta-Languages: Theory and Practice.  Available at https://lfmtp.org/workshops/2017/inc/papers/paper_2_ariotti.pdf.
  * [4] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie C. Weirich & Stephan A. Zdancewic (2005): _Mechanized metatheory for the masses: The POPLmark challenge_.  In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Lecture Notes in Computer Science 3603, Springer, Berlin, Heidelberg, New York, pp. 50–65, 10.1007/115418684.
  * [5] John Boyland & Tian Zhao (2014): _Variable-Arity Functions: Work in Progress_.  Presented at LFMTP 2014 (Vienna Summer of Logic). Available as http://www.cs.uwm.edu/csfac/boyland/papers/lf+variable.pdf.
  * [6] Nathan Carter & Kenneth Monks (2013): _Lurch: A word processor that can grade students’ proofs_.  In: Work in Progress at CICM, CEUR Workshop Proceedings 1010\.  Available at http://ceur-ws.org/Vol-1010/paper-04.pdf.
  * [7] David Cerna (2019): _AXolotl: A Self-study Tool for First-order Logic_.  Technical Report, JKU RISC.
  * [8] David M. Cerna, Rafael P.D. Kiesel & Alexandra Dzhiganskaya (2020): _A Mobile Application for Self-Guided Study of Formal Reasoning_.  In Pedro Quaresma, Walther Neuper & João Marcos, editors: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313, Open Publishing Association, pp. 35–53, 10.4204/EPTCS.313.3.
  * [9] Arthur Charguéraud (2011): _The Locally Nameless Representation_.  Journal of Automated Reasoning, pp. 1–46, 10.1007/s10817-011-9225-2.
  * [10] Dexter Kozen & Alexandra Silva (2017): _Practical coinduction_.  Mathematical Structures in Computer Science 27(7), p. 1132–1152, 10.1017/S0960129515000493.
  * [11] William Lovas & Frank Pfenning (2008): _A Bidirectional Refinement Type System for LF_.  Electronic Notes in Theoretical Computer Science 196, p. 113–128, 10.1016/j.entcs.2007.09.021.
  * [12] Frank Pfenning & Conal Elliott (1988): _Higher-order abstract syntax_.  In: Proceedings of the ACM SIGPLAN ’88 Conference on Programming Language Design and Implementation, ACM Press, New York, pp. 199–208, 10.1145/53990.54010.
  * [13] Frank Pfenning & Carsten Schürmann (2002): _Twelf User’s Guide, Version 1.4_.  Available at http://www.cs.cmu.edu/~twelf.
  * [14] Benjamin C. Pierce (2002): _Types and Programming Languages_.  The MIT Press, Cambridge, Massachussetts, USA and London, England.
  * [15] Anders Schlichtkrull, Jørgen Villadsen & Andreas Halkjær From (2019): _Students’ Proof Assistant (SPA)_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, Electronic Proceedings in Theoretical Computer Science 290, Open Publishing Association, pp. 1–13, 10.4204/EPTCS.290.1.
  * [16] Masaru Tomita, editor (1991): _Generalized LR Parsing_.  Springer, US.
  * [17] Yaoda Zhou, Bruno C. d. S. Oliveira & Jinxu Zhao (2020): _Revisiting Iso-Recursive Subtyping_.  Proceedings of ACM Programming Languages 4(OOPSLA), 10.1145/3428291.


A note on the Singleton bounds for codes over finite rings*** E-mail
addresses: ysh-tang@163.com(Y. Tang), 693204301@qq.com(H. Xu),
1191398576@qq.com(Z.Sun).

Yongsheng Tang1, Heqian Xu1, Zhonghua Sun2

1School of Mathematics and Statistics, Hefei Normal University, Hefei 230601,
Anhui, P.R.China
2School of Mathematics, Hefei University of Technology, Hefei 230009, Anhui,
P.R.China

Abstract In this paper, we give a notation on the Singleton bounds for linear
codes over a finite commutative quasi-Frobenius ring in the work of Shiromoto
[5]. We show that there exists a class of finite commutative quasi-Frobenius
rings. The Singleton bounds for linear codes over such rings satisfy

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

_keywords_ : Linear codes, General weight, Quasi-Frobenius ring, Singleton
bounds

1 Introduction

Let $R$ be a finite commutative quasi-Frobenius (QF) ring with characteristic
$k$ and cardinality $M,$ where $k=\prod_{i=1}^{s}p_{i}^{t_{i}},$
$M=\prod_{i=1}^{s}p_{i}^{r_{i}t_{i}},$ $p_{i}$ are distinct primes, $r_{i}$
and $t_{i}$ are positive integers (see [4] and [7]). Let $R^{n}$ be the free
$R$-module of rank $n$ consisting of all $n$-tuples of elements of $R.$ A
linear code $C$ of length $n$ over $R$ is a $R$-submodule of $R^{n}.$ An
element of $C$ is called a codeword of $C.$ In this paper, we will use a
general notion of weight, abstracted from the Hamming, the Lee and the
Euclidean weights. For each $c=(c_{1},c_{2},\cdots,c_{n})\in R^{n}$ and $r\in
R,$ the complete weight of $c$ is defined by

$n_{r}(c)=\\{i|c_{i}=r\\}.$

To define a general weight function ${w}(c)$, let $a_{r},$ $(0\neq)r\in R$ be
positive real numbers, and set $a_{0}=0.$ Set

$\displaystyle{w}(c)=\sum\limits_{r\in R}a_{r}n_{r}(c).$ (1)

If we set $a_{r}=1,$ for every $(0\neq)r\in R,$ then ${w}(c)$ is just the
Hamming weight of $c,$ denoted by ${w_{H}}(c).$ Throughout this paper, we
denote

$\displaystyle A={\rm max}\\{a_{r}|r\in R\\}.$ (2)

For a linear code $C$, the general weight distance, denoted by $d(C)$, is
equal to the minimum general weight ${w}(C)$ of the code $C$.

Example 1.1. Let us consider the ring $R=\mathbb{Z}_{6}=\\{0,1,2,3,4,5\\}.$ If
we set $a_{0}=0,a_{1}=a_{5}=1,a_{2}=a_{4}=2$ and $a_{3}=3,$ which yield the
Lee weights of the elements of $\mathbb{Z}_{6}$ (see [6]). Then $A=3.$ While
if we set $a_{0}=0,a_{1}=a_{5}=1,a_{2}=a_{4}=4$ and $a_{3}=9,$ which yield the
Euclidean weights of the elements of $\mathbb{Z}_{6},$ then $A=9.$

Example 1.2. Let us consider the ring
$\mathbb{F}_{2}+u\mathbb{F}_{2}=\\{0,1,u,1+u\\},$ which is a 2-dimensional
algebra over the field $\mathbb{F}_{2}$ with a nilpotent element $u$ where
$u^{2}=0$ (see [1]). If we set $a_{0}=0,a_{1}=a_{1+u}=1$ and $a_{u}=2,$ which
yield the Lee weights of the elements of $\mathbb{F}_{2}+u\mathbb{F}_{2}.$
Then $A=2.$ While if we set $a_{0}=0,a_{1}=a_{1+u}=1$ and $a_{u}=4,$ which
yield the Euclidean weights of the elements of
$\mathbb{F}_{2}+u\mathbb{F}_{2},$ then $A=4.$

The following Singleton bounds on a general weight function for linear code
$C$ over a finite commutative QF ring were obtained in [5].

Theorem 1.3._Let $C$ be a linear code of length $n$ over a finite commutative
QF ring $R.$ Let ${w}(c)$ be a general weight function on $C$, as in (1); and
with maximum $a_{r}$-value $A$, as in (2). Suppose the minimum general weight
of ${w}(c)$ on $C$ is $d(C)$. Then_

$\Big{[}\frac{d(C)-1}{A}\Big{]}\leq n-\log_{|R|}|C|,$

_where $[b]$ is the integer part of $b.$_

The purpose of this paper is to show that there exists a class of finite
commutative QF rings. The Singleton bounds for linear codes over such rings
satisfy

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

2 General Gray map on $R$

Let $R$ be a finite commutative quasi-Frobenius (QF) ring with characteristic
$k$ and cardinality $M,$ where $k=\prod_{i=1}^{s}p_{i}^{t_{i}},$
$M=\prod_{i=1}^{s}p_{i}^{r_{i}t_{i}},$ $p_{i}$ are distinct primes, $r_{i}$
and $t_{i}$ are positive integers. For any element $a\in R,$ a general Gray
map $\varphi$ on $R$ is defined as

$\varphi:R\rightarrow\mathbb{F}_{p_{i}^{e_{i}}}^{A},$
$a\mapsto(a_{1},\ldots,a_{i},a_{i+1},\ldots,a_{A}),$

where $p_{i}^{e_{i}}$ is any divisor of $\prod_{i=1}^{s}p_{i}^{r_{i}t_{i}}$
and $\mathbb{F}_{p_{i}^{e_{i}}}$ is a finite field with $p_{i}^{e_{i}}$
elements. In detail,

  * •

if $a_{0}=0$, ${w}(0)=0,$ then $\varphi(0)=(0,\ldots,0,0,\ldots,0);$

  * •

if $0<a_{r}<A$ and ${w}(a_{r})=i,$ then
$\varphi(a_{r})=(a_{1},\ldots,a_{i},a_{i+1},\ldots,a_{A}),$ where there are
$i$ nonzeros and $A-i$ zeros among $a_{1},\ldots,a_{i},a_{i+1},\ldots,a_{A};$

  * •

if $a_{r}=A$ and ${w}(a_{r})=A,$ then
$\varphi(a_{r})=(a_{1},\ldots,a_{i},a_{i+1},\ldots,a_{A}),$ where $a_{t}\neq
0$ for $t=1,2,\ldots,A.$

The general Gray map $\varphi$ can be extended to $R^{n}$ in an obvious way.

Example 2.1. Let us consider a general Gray map $\varphi$ on $\mathbb{Z}_{6}$
with the Lee weight. From Example 1.1, we have $A=3.$ A general Gray map
$\varphi$ from $\mathbb{Z}_{6}$ to $\mathbb{F}_{m}^{3}$ ( $m=2$ or $3$), can
be defined as
$\varphi(0)=(0,0,0),\varphi(1)=(0,0,a_{11}),\varphi(2)=(0,a_{21},a_{22}),\varphi(3)=(a_{31},a_{32},a_{33}),\varphi(4)=(a_{41},a_{42},0),\varphi(5)=(a_{51},0,0),$
where $a_{ij}\neq 0.$

From the definition of the general Gray map we can obtain the following
theorem.
Theorem 2.2.  _Let the notation be as before. For any finite commutative QF
ring $R,$ there exists a Gray map $\varphi$ from $R^{n}$ to
$\mathbb{F}_{p_{i}^{e_{i}}}^{An}$ and the Gray map $\varphi$ is a distance
preserving map from $(R^{n},$ general weight distance $)$ to
$(\mathbb{F}_{p_{i}^{e_{i}}}^{An},$ Hamming distance $)$._

Proof. From the above definitions, it is clear that
$\varphi(x-y)=\varphi(x)-\varphi(y)$ for $x,y\in R^{n}$. Thus,
$d(x,y)=w(x-y)=w_{H}(\varphi(x-y))=w_{H}(\varphi(x)-\varphi(y))=d_{H}(\varphi(x),\varphi(y))$.
∎

3 Main result

In this section, we will show that there exists a class of finite commutative
QF rings. The Singleton bounds for linear codes over such rings satisfy

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

For our purpose, we firstly introduce the following lemma on the Singleton
bounds for codes over finite fields (see [3]).

Lemma 3.1.  _Let $C$ be a code (possibly nonlinear) of length $n$ over the
finite field $\mathbb{F}_{q}$ with $|C|$ elements and the minimum Hamming
distance $d_{H}(C)$. Then_

$d_{H}(C)\leq n-\log_{q}|C|+1.$

Theorem 3.2. _Let $C$ be a linear code of length $n$ over a finite commutative
QF ring $R.$ Let $w(x)$ be a general weight function on $C$, as in (1); and
with maximum $a_{r}$-value $A$, as in (2). Suppose the minimum weight of
$w(x)$ on $C$ is $d(C)$. Let $p=\emph{min}\\{p_{1},\ldots,p_{s}\\}$ and
$\varphi$ be a distance preserving map from $(R^{n},$ general weight distance)
to $(\mathbb{F}_{p_{i}^{e_{i}}}^{An},$ Hamming distance). Then _

$d(C)\leq An-\log_{p}|C|+1.$

_Furthermore, if $\varphi$ is a bijective map and a distance preserving map
from $(R^{n},$ general weight distance) to $(\mathbb{F}_{p}^{An},$ Hamming
distance), then_

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

Proof. By Theorem 2.2, we have each general Gray image of the code $C$ under
its corresponding general Gray map $\varphi$ is a $p_{i}^{e_{i}}$-ary code
with the same length $An$ and the same minimum Hamming distance
$d_{H}(\varphi(C)).$ By Lemma 3.1, each general Gray image of the code $C$
satisfies

$d_{H}(\varphi(C))\leq An-\log_{p_{i}^{e_{i}}}|\varphi(C)|+1.$

Furthermore

$d(C)=d_{H}(\varphi(C))\leq\textrm{min}\\{An-\log_{p_{i}^{e_{i}}}|\varphi(C)|+1\\}=An-\textrm{max}\\{\log_{p_{i}^{e_{i}}}|\varphi(C)|\\}+1.$

Since $p=\textrm{min}\\{p_{1},\ldots,p_{s}\\}$ and $|\varphi(C)|\leq|C|,$ then
$\textrm{max}\\{\log_{p_{i}^{e_{i}}}|\varphi(C)|\\}=\log_{p}|C|.$ Therefore

$d(C)\leq An-\log_{p}|C|+1.$

On the other hand, if $\varphi$ is a bijection from $R^{n}$ to
$\mathbb{F}_{p}^{An}$, then $\log_{p_{i}^{t_{i}}}|\varphi(C)|$ is maximum,
that is, if $\log_{p_{i}^{e_{i}}}|\varphi(C)|$ attains to be maximum, then
$|R|=p^{A}$ and $|\varphi(C)|=|C|.$ Hence, we have

$d(C)\leq An-\log_{p}|C|+1.$

It follows that

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

This completes the proof. ∎

Remark 3.2 Theorem 3.2 shows that if there exists a bijective map $\varphi$
and the map $\varphi$ is a distance preserving map from $(R^{n},$ general
weight distance) to $(\mathbb{F}_{p}^{An},$ Hamming distance), then the
Singleton bounds for linear codes over $R$ satisfy

$\frac{d(C)-1}{A}\leq n-\log_{|R|}|C|.$

Example 3.3. Consider any linear code $C$ of length $n(\geq 1)$ over the QF
ring $\mathbb{F}_{2}+u\mathbb{F}_{2}=\\{0,1,u,1+u\\}.$ The Lee weights of the
elements of $\mathbb{F}_{2}+u\mathbb{F}_{2}$ is given as follows:
${w}_{L}(0)=0,\ {w}_{L}(1)=1,\ {w}_{L}(u)=2,\ {w}_{L}(1+u)=1.$ For any element
$a+ub\in\mathbb{F}_{2}+u\mathbb{F}_{2}.$ A Gray map $\varphi$ from
$\mathbb{F}_{2}+u\mathbb{F}_{2}$ to $\mathbb{F}_{2}^{2}$ is defined as
$\varphi(a+ub)=(b,a+b)$(see [1] ). The map $\varphi$ can be extended to
$(\mathbb{F}_{2}+u\mathbb{F}_{2})^{n}$ in an obvious way and the extended
$\varphi$ is a bijection from $(\mathbb{F}_{2}+u\mathbb{F}_{2})^{n}$ to
$\mathbb{F}_{2}^{2n}.$ Therefore, we have

$\frac{d(C)-1}{2}\leq n-\log_{4}|C|.$

Example 3.4. Consider any linear code $C$ of length $n(\geq 1)$ over the QF
ring $\mathbb{F}_{2}+u\mathbb{F}_{2}+v\mathbb{F}_{2}+uv\mathbb{F}_{2},$ which
is a characteristic $2$ ring subject to the restrictions $u^{2}=v^{2}=0$ and
$uv=vu.$ Let
$\varphi:(\mathbb{F}_{2}+u\mathbb{F}_{2}+v\mathbb{F}_{2}+uv\mathbb{F}_{2})^{n}\rightarrow\mathbb{F}_{2}^{4n}$
be the map given by $\varphi(a+ub+vc+uvd)=(a+b+c+d,c+d,b+d,d).$ Then $\varphi$
is a bijective map. For any element
$a+ub+vc+uvd\in\mathbb{F}_{2}+u\mathbb{F}_{2}+v\mathbb{F}_{2}+uv\mathbb{F}_{2},$
we define the Lee weight $w_{L}(a+ub+vc+uvd)=w_{H}(a+b+c+d,c+d,b+d,d),$ where
$w_{H}$ denotes the ordinary Hamming weight for binary codes(see [8]).
Therefore, we have

$\frac{d(C)-1}{4}\leq n-\log_{16}|C|.$

4 An application to codes over $\mathbb{Z}_{\ell}$

In this section, we mainly introduce the ring $\mathbb{Z}_{\ell}$ as a good
example of a finite commutative QF ring. Let
$\mathbb{Z}_{\ell}=\\{0,1,,2,\ldots,\ell-1\\}$ denote the ring of integers
modulo $\ell.$ Now we introduce three kinds of weights, namely the Hamming
weight, the Lee weight, and the Euclidean weight. The Hamming weight
${w_{H}}(c)$ of a vector
$c=(c_{1},c_{2},\cdots,c_{n})\in\mathbb{Z}_{\ell}^{n},$ is the number of its
nonzero entries in the vector. The Lee weight for the elements of
$\mathbb{Z}_{\ell}$ is defined as ${w}_{{L}}(a)={\rm min}\\{a,\ \ell-a\\}$ for
all $a\in\\{0,1,\cdots,\ell-1\\}$ (see [6]). The Euclidean weight for the
elements of $\mathbb{Z}_{\ell}$ is defined as ${w}_{E}(a)={w}_{L}(a)^{2}$ for
all $a\in\\{0,1,\cdots,\ell-1\\}.$ Denote the minimum weight of a linear code
$C$ with respect to Hamming, Lee, Euclidean weights by $d_{H}(C)$; $d_{L}(C)$
and $d_{E}(C)$ ; respectively. It is clear that the maximum $a_{r}$ -value is
$1$; $[\ell/2]$ and $[\ell/2]^{2}$; respectively. In the following, we denote
by $\ell_{1}$ and $\ell_{2}$ the following integers, respectively,
$\ell_{1}=[\ell/2]$ and $\ell_{2}=[\ell/2]^{2}.$

The next result follows immediately from Theorem 3.2.
Corollary 4.1. _Let $C$ be a linear code of length $n$ over over
$\mathbb{Z}_{\ell},$ where $\ell=\prod_{i=1}^{s}p_{i}^{a_{i}},$ $p_{i}$ are
distinct primes and $a_{i}$ are positive integers. Let
$p=\emph{min}\\{p_{1},\ldots,p_{s}\\}.$ Then there are the following bounds on
minimum weights: _

$d_{H}(C)\leq n-\log_{p}|C|+1;$ $d_{L}(C)\leq\ell_{1}n-\log_{p}|C|+1;$
$d_{E}(C)\leq\ell_{2}n-\log_{p}|C|+1.$

_Furthermore, if $\varphi$ is a bijective map and a distance preserving map
from $(\mathbb{Z}_{\ell}^{n},$ general weight distance) to
$(\mathbb{F}_{p}^{An},$ Hamming distance), then_

$d_{H}(C)-1\leq n-\log_{\ell}|C|;$ $\frac{d_{L}(C)-1}{\ell_{1}}\leq
n-\log_{\ell}|C|;$

$\frac{d_{E}(C)-1}{\ell_{2}}\leq n-\log_{\ell}|C|.$

Example 4.2. Consider any linear code $C$ of length $n(\geq 1)$ over the QF
ring $\mathbb{Z}_{4}=\\{0,1,2,3\\}.$ The Lee weights of the elements of
$\mathbb{Z}_{4}$ are given as follows: ${w}_{L}(0)=0,\
{w}_{L}(1)={w}_{L}(3)=1,\ {w}_{L}(2)=2.$ Then $A=2.$ There exists a bijective
map $\varphi$ from $\mathbb{Z}_{4}$ to $\mathbb{F}_{2}^{2}.$ In fact,
$\varphi(0)=(0,0)$, $\varphi(1)=(0,1)$, $\varphi(2)=(1,1)$, and
$\varphi(3)=(1,0)$(see [2] ). The map $\varphi$ can be extended to
$\mathbb{Z}_{4}^{n}$ in an obvious way and the extended $\varphi$ is a
bijection from $\mathbb{Z}_{4}^{n}$ to $\mathbb{F}_{2}^{2n}.$ Therefore, we
have

$\frac{d_{L}(C)-1}{2}\leq n-\log_{4}|C|.$

Acknowledgements

This research is supported by Natural Science Foundation of Anhui Province
(No. 1408085QF116), Colleges Outstanding Young Talents Program in 2014, Anhui
Province ( No. [2014]181) and Hefei Normal University Research Project (No.
2015JG09).

## References

  * [1] A. Bonnecaze, P. Udaya, Cyclic codes and self-dual codes over $\mathbb{F}_{2}+u\mathbb{F}_{2}$, _IEEE Trans. Inform. Theory_ 4 (1999) 1250-1255.
  * [2] A.R. Hammons, P.V. Kumar, A.R. Calderbank, N.J.A. Sloane, P. Solé, The $\mathbb{Z}_{4}$-linearity of Kerdock, Preparata, Goethals, and Related Codes, _IEEE Trans. Inform. Theory_ 40 (1994) 301-319.
  * [3] F.J. Macwilliams, N.J.A. Sloane, _The Theory of Error-Correcting Codes_ , North-Holland, Amsterdam New York, 1977.
  * [4] B. R. McDonald, _Finite Rings with Identity_ , Dekker, New York, 1974.
  * [5] K. Shiromoto, Singleton bounds for codes over finite rings, _Journal of Algebraic Combinatorics_ 12 (2000) 95-99.
  * [6] J.H. Van Lint, _Introduction to Coding Theory_ , Third ed., Springer, Berlin, 1999.
  * [7] J. Wood, Duality for modules over finite rings and applications to coding theory, _American Journal of Mathematics_ 121 (1999) 555-575.
  * [8] B. Yildiz, S.Karadeniz, Linear codes over $\mathbb{F}_{2}+u\mathbb{F}_{2}+v\mathbb{F}_{2}+uv\mathbb{F}_{2},$ _Des. Codes Cryptogr._ 54 (2010)61-81.