Quantitative aspects of linear and affine closed lambda terms

TL;DR

This paper provides combinatorial counts and generation algorithms for various classes of closed affine and linear lambda-terms and their normal forms, based on size measurements and context data structures.

Contribution

It introduces formulas for counting and generating closed affine and linear lambda-terms and their normal forms using context-based data structures.

Findings

Formulas for counting lambda-terms and normal forms by size.

Algorithms for generating all terms of a given size.

Use of context data structures for term enumeration.

Abstract

Affine $\lambda$-terms are $\lambda$-terms in which each bound variable occurs at most once and linear $\lambda$-terms are $\lambda$-terms in which each bound variables occurs once. and only once. In this paper we count the number of closed affine $\lambda$-terms of size $n$, closed linear $\lambda$-terms of size $n$, affine $\beta$-normal forms of size $n$ and linear $\beta$-normal forms of ise $n$, for different ways of measuring the size of $\lambda$-terms. From these formulas, we show how we can derive programs for generating all the terms of size $n$ for each class. For this we use a specific data structure, which are contexts taking into account all the holes at levels of abstractions.

Equations

$$(‘l0\text{leavevmode}(‘l0\text{leavevmode}‘l0))(‘l0\text{leavevmode}‘l(‘l0\text{leavevmode}0))(‘l0\text{leavevmode}‘l(0\text{leavevmode}‘l0))((‘l0\text{leavevmode}‘l0)\text{leavevmode}‘l0)(‘l(‘l0\text{leavevmode}0)\text{leavevmode}‘l0)(‘l(0\text{leavevmode}‘l0)\text{leavevmode}‘l0)‘l(‘l0\text{leavevmode}(‘l0\text{leavevmode}0))‘l(‘l0\text{leavevmode}(0\text{leavevmode}‘l0))$$

$$‘l((‘l0\text{leavevmode}‘l0)\text{leavevmode}0)‘l(‘l(‘l0\text{leavevmode}0)\text{leavevmode}0)‘l(‘l(0\text{leavevmode}‘l0)\text{leavevmode}0)‘l(0\text{leavevmode}(‘l0\text{leavevmode}‘l0))‘l(0\text{leavevmode}‘l(‘l0\text{leavevmode}0))‘l(0\text{leavevmode}‘l(0\text{leavevmode}‘l0))‘l((‘l0\text{leavevmode}0)\text{leavevmode}‘l0)‘l((0\text{leavevmode}‘l0)\text{leavevmode}‘l0)$$

$$‘lx.x\text{leavevmode}(‘lx.x\text{leavevmode}‘lx.x)‘lx.x\text{leavevmode}‘ly.(‘lx.x\text{leavevmode}y)‘lx.x\text{leavevmode}‘ly.(y\text{leavevmode}‘lx.x)(‘lx.x\text{leavevmode}‘lx.x)\text{leavevmode}‘lx.x$$

$$‘ly.(‘lx.x\text{leavevmode}y)\text{leavevmode}‘lx.x‘ly.(y\text{leavevmode}‘lx.x)\text{leavevmode}‘lx.x‘ly.(‘lx.x\text{leavevmode}(‘lx.x\text{leavevmode}y))‘ly.(‘lx.x\text{leavevmode}(y\text{leavevmode}‘lx.x))$$

$$‘ly.((‘lx.x\text{leavevmode}‘lx.x)\text{leavevmode}y)‘ly.(‘lz.(‘lx.x\text{leavevmode}z)\text{leavevmode}y)‘ly.(‘lz.(z\text{leavevmode}‘lx.x)\text{leavevmode}y)‘ly.(y\text{leavevmode}(‘lx.x\text{leavevmode}‘lx.x))$$

$$‘ly.(y\text{leavevmode}‘lz.(‘lx.x\text{leavevmode}z))‘ly.(y\text{leavevmode}‘lz.(z\text{leavevmode}‘lx.x))‘ly.((‘lx.x\text{leavevmode}y)\text{leavevmode}‘lx.x)‘ly.((y\text{leavevmode}‘lx.x)\text{leavevmode}‘lx.x)$$

$$(‘l0\text{leavevmode}‘l‘l1)(‘l0\text{leavevmode}‘l‘l‘l0)(‘l‘l0\text{leavevmode}‘l‘l0)(‘l‘l1\text{leavevmode}‘l0)(‘l‘l‘l0\text{leavevmode}‘l0)‘l(‘l‘l1\text{leavevmode}0)‘l(‘l‘l‘l0\text{leavevmode}0)‘l(0\text{leavevmode}‘l‘l1)$$

$$\text{leavevmode}‘l(0\text{leavevmode}‘l‘l‘l0)‘l(‘l0\text{leavevmode}‘l1)‘l(‘l1\text{leavevmode}‘l0)‘l‘l(‘l0\text{leavevmode}1)‘l‘l(1\text{leavevmode}‘l0)‘l(‘l0\text{leavevmode}‘l‘l0)‘l(‘l‘l0\text{leavevmode}‘l0)‘l‘l(‘l‘l0\text{leavevmode}0)$$

$$\text{leavevmode}‘l‘l(0\text{leavevmode}‘l‘l0)‘l‘l‘l(0\text{leavevmode}1)‘l‘l‘l(1\text{leavevmode}0)‘l‘l‘l‘l2‘l‘l(‘l0\text{leavevmode}‘l0)‘l‘l‘l(‘l0\text{leavevmode}0)‘l‘l‘l(0\text{leavevmode}‘l0)‘l‘l‘l‘l‘l1‘l‘l‘l‘l‘l‘l0$$

$${\mathbf{m}}^{\uparrow i}=\mathbf{n}‘:{\mathbb{N}}^p\text{leavevmode}\mathrm{where}\text{leavevmode}{n}_j=m_j\text{leavevmode}\mathrm{if}\text{leavevmode}j\ne i\text{leavevmode}\mathrm{and}\text{leavevmode}{n}_i=m_i+1$$

$$x:\mathbf{m}=x:(m_0,...)=(x,m_0,...)$$

$$\mathsf{tail}(x:\mathbf{m})=\mathbf{m}.$$

$$c_{1}=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-3.0pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.49028pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{@}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-8.2889pt\raise-32.69386pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}{\hbox{\kern 15.37918pt\raise-32.69386pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.46947pt\raise-32.69386pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{0}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad c_{2}=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&&\\\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-7.09029pt\raise-16.84665pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 15.1778pt\raise-16.84665pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.0667pt\raise-16.84665pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{0}}$}}}}}}}{\hbox{\kern-8.2889pt\raise-34.4983pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad\qquad\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.56378pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 9.56378pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.56378pt\raise-15.5272pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{c_{1}}$}}}}}}}{\hbox{\kern 13.45268pt\raise-15.5272pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 26.34158pt\raise-15.5272pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{c_{2}}$}}}}}}}\ignorespaces}}}}\ignorespaces=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&\\&&&&&&\\&&&&&&\\&&&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 42.46947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-3.0pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.96947pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.35837pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 64.53616pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 78.82506pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 100.89175pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-3.0pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.49028pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 30.96947pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.35837pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 60.44588pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 82.71396pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 95.60286pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{0}}$}}}}}}}{\hbox{\kern-8.2889pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}{\hbox{\kern 15.37918pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.46947pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{0}$}}}}}}}{\hbox{\kern 46.35837pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 59.24727pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}\ignorespaces}}}}\ignorespaces$$

$$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.09029pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\\\crcr}}}\ignorespaces{\hbox{\kern-7.09029pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\color[rgb]{0,0,1}`l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-6.56378pt\raise-15.5272pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{c_{2}}$}}}}}}}\ignorespaces}}}}\ignorespaces=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\&&\\\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\color[rgb]{0,0,1}`l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-3.0pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.49028pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-7.09029pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 15.37918pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.46947pt\raise-32.79108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}{\hbox{\kern-8.2889pt\raise-50.44273pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{2}}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad\qquad\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&\\&&&\\&&&&&&\\&&&&&&\\&&&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 42.46947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\color[rgb]{0,.5,0}`l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-3.0pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 42.67085pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-3.0pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.96947pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.55975pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 64.93893pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 79.22783pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 101.29453pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-3.0pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.49028pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 30.96947pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.55975pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 60.84865pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 83.11673pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 96.00563pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}{\hbox{\kern-8.2889pt\raise-66.38716pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{2}}$}}}}}}}{\hbox{\kern 15.37918pt\raise-66.38716pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.46947pt\raise-66.38716pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{0}$}}}}}}}{\hbox{\kern 46.55975pt\raise-66.38716pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 59.65004pt\raise-66.38716pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\color[rgb]{1,0,0}\Box_{1}}$}}}}}}}\ignorespaces}}}}\ignorespaces=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 8.2889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&\\&&&\\&&&&&&\\&&&&&&\\&&&&\\&&&&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 42.46947pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\color[rgb]{0,.5,0}`l}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-3.0pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 42.67085pt\raise-15.94443pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-3.0pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.2889pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.96947pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.55975pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 63.74033pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 76.83061pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 98.89731pt\raise-31.88885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-3.0pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 11.49028pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{@\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern 30.96947pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.55975pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 59.65004pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{`l\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 80.71951pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 93.60841pt\raise-48.7355pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{1}}$}}}}}}}{\hbox{\kern-8.2889pt\raise-66.42882pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Box_{2}}$}}}}}}}{\hbox{\kern 15.37918pt\raise-66.42882pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 28.46947pt\raise-66.42882pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{0}$}}}}}}}{\hbox{\kern 46.55975pt\raise-66.42882pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 60.38617pt\raise-66.42882pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{\color[rgb]{1,0,0}S}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{{\hbox{\lx@xy@droprule}}}\ignorespaces{}{{\hbox{\lx@xy@droprule}}}{{\hbox{\lx@xy@droprule}}}{\hbox{\kern-3.0pt\raise-82.96991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 15.37918pt\raise-82.96991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 30.96947pt\raise-82.96991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 46.55975pt\raise-82.96991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 61.24033pt\raise-82.96991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\color[rgb]{1,0,0}0}$}}}}}}}\ignorespaces}}}}\ignorespaces$$

$$l_{0,\mathbf{m}}^{‘n}=l_{0,\mathbf{m}}^0=l_{0,\mathbf{m}}^1=[m_0=1\wedge \underset{j=1}{\overset{p-1}{\bigwedge }}{m}_j=0]$$

$$\sum _{\mathbf{q}‘(+)\mathbf{r}=\mathbf{m}}\sum _{k=0}^n{l}_{k,\mathbf{q}}{l}_{n-1-k,\mathbf{r}}$$

$$\sum _{i=0}^{p-1}(m_i+1)l_{n-i,{\mathbf{m}}^{\uparrow i}}^{‘n}$$

$$l_{n+1,0:\mathbf{m}}^{‘n}$$

$$l_{n+1,(h+1):\mathbf{m}}^{‘n}$$

$$l_{n+1,0:\mathbf{m}}^0$$

$$l_{n+1,(h+1):\mathbf{m}}^0$$

$$l_{n+1,0:\mathbf{m}}^1$$

$$l_{n+1,(h+1):\mathbf{m}}^1$$

$$a_{n+1,0:\mathbf{m}}^{‘n}$$

$$a_{n+1,(h+1):\mathbf{m}}^{‘n}$$

$$a_{n+1,0:\mathbf{m}}^0$$

$$a_{n+1,(h+1):\mathbf{m}}^0$$

$$0,1,2,8,29,140,661,3622,19993,120909,744890,4887401,32795272,...$$

$$\mathcal{A}(z,u)=u+z(\mathcal{A}(z,u){)}^2+z\frac{\partial \mathcal{A}(z,u)}{\partial u}+z\mathcal{A}(z,u).$$

$$a_{n+1,0:\mathbf{m}}^1$$

$$a_{n+1,(h+1):\mathbf{m}}^1$$

$$0,0,1,2,3,9,30,81,242,838,2799,9365,33616,122937,449698,1696724,6558855,...$$

$$\hat{\mathcal{A}}(z,u)=zu+z(\hat{\mathcal{A}}(z,u){)}^2+z\frac{\partial \hat{\mathcal{A}}(z,u)}{\partial u}+z\hat{\mathcal{A}}(z,u).$$

Full text

Keywords: Lambda calculus, combinatorics, functional programming

1 Introduction

The $`l$-calculus [1] is a well known formal system designed by Alonzo Church [8] for studying the concept of function. It has three kinds of basic operations: variables, application and abstraction (with an operator $`l$ which is a binder of variables). We assume the reader familiar with the $`l$-calculus and with de Bruijn indices.111If the reader is not familiar with the $`l$-calculus, we advise him to read the introduction of [15], for instance.

In this paper we are interested in terms in which bound variables occur once. A closed $`l$-term is a $`l$-term in which there is no free variable, i.e., only free variables. An affine $`l$-term (or BCK term) is a $`l-$term in which bound variables occur at most once. A linear $`l$-term (or BCI term) is a $`l$-term in which bound variables occur once and only once.

In this paper we propose a method for counting and generating (including random generation) linear and affine closed $`l$-terms based on a data structure which we call SwissCheese because of its holes. Actually we count those $`l$-terms up-to $`a$-conversion. Therefore it is adequate to use de Bruijn indices [11], because a term with de Bruijn indices represents an $`a$-equivalence class. An interesting aspect of these terms is the fact that they are simply typed [17, 16]. For instance, generated by the program of Section 5 6, there are $16$ linear terms of natural size $8$:

[TABLE]

[TABLE]

written with explicit variables

[TABLE]

[TABLE]

[TABLE]

[TABLE]

and there are $25$ affine terms of natural size $7$:

[TABLE]

[TABLE]

[TABLE]

The Haskell programs of this development are on GitHub: https://github.com/PierreLescanne/CountingGeneratingAfffineLinearClosedLambdaterms.

Notations

In this paper we use specific notations.

Given a predicate $p$, the Iverson notation written $[p(x)]$ is the function taking natural values which is $1$ if $p(x)$ is true and which is [math] if $p(x)$ is false.

Let $\mathbf{m}`:\mathbb{N}^{p}$ be the $p$-tuple $(m_{0},...,m_{p-1})$. In Section 5, we consider also infinite tuples. Thus $\mathbf{m}`:\mathbb{N}^{`w}$ is the sequence $(m_{0},m_{1},...)$. Notice in the case of infinite tuples, we are only interested in infinite tuples equal to [math] after some index.

• •

$p$ is the length of $\mathbf{m}$, which we write also $\mathsf{length}\leavevmode\nobreak\ \mathbf{m}$

• •

The $p$-tuple $(0,...,0)$ is written $0^{p}$. $0^{`w}$ is the infinite tuple made of [math]’s.

• •

The increment of a $p$-tuple at $i$ is:

[TABLE]

• •

Putting an element $x$ as head of a tuple is written

[TABLE]

tail removes the head of a tuple:

[TABLE]

• •

$`(+)$ is the componentwise addition on tuples.

2 SwissCheese

The basic concept is this of $\mathbf{m}$-SwissCheese or Swisscheese of characteristic $\mathbf{m}$ or simply SwissCheese if there is no ambiguity on $\mathbf{m}$. A $\mathbf{m}$-SwissCheese or a SwissCheese of characteristic $\mathbf{m}$, where $\mathbf{m}$ is of length $p$) is, a $`l$-term with holes at $p$ levels, which are all counted, using $\mathbf{m}$. The $p$ levels of holes are $\Box_{0}$,… $\Box_{p-1}$. A hole $\Box_{i}$ is meant to be a location for a variable at level $i$, that is under $i$ $`l$’s. According to the way bound variables are inserted when creating abstractions (see below), we consider linear or affine SwissCheeses. The holes have size [math]. An $\mathbf{m}$-SwissCheese or a SwissCheese of characteristic $\mathbf{m}$ has $m_{0}$ holes at level [math], $m_{1}$ holes at level $1$, … $m_{p-1}$ holes at level $p-1$. Let $l_{n,\mathbf{m}}$ (resp. $a_{n,\mathbf{m}}$) count the linear (resp. the affine) $\mathbf{m}$-SwissCheese of size $n$. $l_{n,\mathbf{m}}=l_{n,\mathbf{m}^{\prime}}$ and $a_{n,\mathbf{m}}=a_{n,\mathbf{m}^{\prime}}$ if $\mathbf{m}$ is finite, $\mathsf{length}\leavevmode\nobreak\ \mathbf{m}\geq n$, $m_{i}=m^{\prime}_{i}$ for $i\leq\mathsf{length}\leavevmode\nobreak\ \mathbf{m}$, and $m^{\prime}_{i}=0$ for $i>\mathsf{length}\leavevmode\nobreak\ \mathbf{m}$. $l_{n,0^{n}}$ (resp. $a_{n,0^{n}}$) counts the closed linear (resp. the closed affine) $`l$-terms.

2.1 Growing a SwissCheese

Given two SwissCheeses, we can build a SwissCheese by application like in Fig 1.

In Fig. 1, $c_{1}$ is a $(0,1,0,0,0)$-SwissCheese, $c_{2}$ is a $(1,1,0,0,0)$-SwissCheese and $c_{1}@c_{2}$ is a $(1,2,0,0,0)$-SwissCheese. Said otherwise, $c_{1}$ has characteristic $(0,1,0,0,0)$, $c_{2}$ has characteristic $(1,1,0,0,0)$ and $c_{1}@c_{2}$ has characteristic $(1,2,0,0,0)$. According to what we said, $c_{1}@c_{2}$ has characteristic $(1,2)$ as well as characteristic $(1,2,0,0,...)$ (a tuple starting with $1$, followed by $2$, followed by infinitely many [math]’s). We could also say that $c_{1}$ has characteristic $(0,1)$ and $c_{2}$ has characteristic $(1,1)$ making $@$ a binary operation on SwissCheeses of length $2$ whereas previously we have made $@$ a binary operation on SwissCheeses of length $5$. In other words, when counting SwissCheeses of characteristic $\mathbf{m}$, the trailing [math]’s are irrelevant. In actual computations, we make the lengths of characteristics consistent by adding trailing [math]’s to too short ones.

Given a SwissCheese, there are two ways to grow a SwissCheese to make another SwissCheese by abstraction.

We put a $`l$ on the top of a $\mathbf{m}$-SwissCheese $c$. This increases the levels of the holes: a hole $\Box_{i}$ becomes a hole $\Box_{i+1}$. $`lc$ is a $(0:\mathbf{m})$-SwissCheese. See Fig 2 on the left. This way, no index is bound by the top $`l$, therefore this does not preserve linearity (it preserves affinity however). Therefore this construction is only for building affine SwissCheeses, not for building linear SwissCheeses. In Figure 2 (left), we colour the added $`l$ in blue and we call it abstraction with no binding. 2. 2.

In the second method for growing a SwissCheese by abstraction, we select first a hole $\Box_{i}$, we top the SwissCheese by a $`l$, we increment the levels of the other holes and we replace the chosen hole by $S^{i}0$. In Figure 2 (right), we colour the added $`l$ in green and we call it abstraction with binding.

2.2 Measuring SwissCheese

We considers several ways of measuring the size of a SwissCheese derived from what is done on $`l$-terms. In all these sizes, applications $@$ and abstractions $`l$ have size $1$ and holes have size [math]. The differences are in the way variables are measured.

• •

Variables have size [math], we call this variable size [math].

• •

Variables have size $1$, we call this **variable size $1$ **.

• •

Variables (or de Bruijn indices) $S^{i}0$ have size $i+1$, we call this natural size.

3 Counting linear closed terms

We start with counting linear terms since they are slightly simpler. We will give recursive formulas first for the numbers $l^{`n}_{n,\mathbf{m}}$ of linear SwissCheeses of natural size $n$ with holes set by $\mathbf{m}$, then for the numbers $l^{0}_{n,\mathbf{m}}$ of linear SwissCheeses of size $n$, for variable size [math], with holes set by $\mathbf{m}$, eventually for the numbers $l^{1}_{n,\mathbf{m}}$ of linear SwissCheeses of size $n$, for variable size $1$, with holes set by $\mathbf{m}$. When we do not want to specify a chosen size, we write only $l_{n,\mathbf{m}}$ without superscript.

3.1 Natural size

First let us count linear SwissCheeses with natural size. This is given by the coefficient $l^{`n}$ which has two arguments: the size $n$ of the SwissCheese and a tuple $\mathbf{m}$ which specifies the number of holes of each level. In other words we are interested in the quantity $l_{n,\mathbf{m}}^{`n}$. We assume that the length of $\mathbf{m}$ is $p$, greater than $n$.

$\mathbf{n=0}$

whatever size is considered, there is only one SwissCheese of size [math] namely $\Box_{0}$. This means that the number of SwissCheeses of size [math] is $1$ if and only if $\mathbf{m}=(1,0,0,...)$:

[TABLE]

$\mathbf{n\neq 0}$** and application**

if a $`l$-term of size $n$ has holes set by $\mathbf{m}$ and is an application, then it is obtained from a $`l$ term of size $k$ with holes set by $\mathbf{q}$ and a $`l$ term of size $n-k-1$ with holes set by $\mathbf{r}$, with $\mathbf{m}=\mathbf{q}`(+)\mathbf{r}$:

[TABLE]

$\mathbf{n\neq 0}$** and abstraction with binding**

consider a level $i$, that is a level of hole $\Box_{i}$. In this hole we put a term $S^{i-1}\,0$ of size $i$. There are $m_{i}$ ways to choose a hole $\Box_{i}$. Therefore there are $m_{i}\,l^{`n}_{n-i-1,\mathbf{m}}$ SwissCheeses which are abstractions with binding in which a $\Box_{i}$ has been replaced by the de Bruijn index $S^{i-1}\,0$ among $l^{`n}_{n,0:\mathbf{m^{\downarrow i}}}$ SwissCheeses, where $\mathbf{m^{\downarrow i}}$ is $\mathbf{m}$ in which $m_{i}$ is decremented. We notice that this refers only to an $\mathbf{m}$ starting with [math]. Hence by summing over $i$ and adjusting $\mathbf{m}$, this part contributes as:

[TABLE]

to $l^{`n}_{n+1,0:\mathbf{m}}$.

We have the following recursive definitions of $l^{`n}_{n,\mathbf{m}}$:

[TABLE]

Numbers of closed linear terms with natural size are given in Figure 3.

3.2 Variable size [math]

The only difference is that the inserted de Bruijn index has size [math]. Therefore we have $m_{i}\,l^{0}_{n-1,\mathbf{m}}$ where we had $m_{i}\,l^{`n}_{n-i-1,\mathbf{m}}$ for natural size. Hence the formulas:

[TABLE]

The sequence $l^{0}_{n,0^{n}}$ of the numbers of closed linear terms is $0,1,0,5,0,60,0,1105,0,27120,0,828250,$ which is sequence A062980 in the On-line Encyclopedia of Integer Sequences with [math]’s at even indices.

3.3 Variable size $1$

The inserted de Bruijn index has size $1$. We have $m_{i}\,l^{1}_{n-2,\mathbf{m}}$ where we had $m_{i}\,l^{`n}_{n-i-1,\mathbf{m}}$ for natural size.

[TABLE]

As noticed by Grygiel et al. [13] (§ 6.1) There are no linear closed $`l$-terms of size $3k$ and $3k+1$. However for the values $3k+2$ we get the sequence: $1,5,60,1105,27120,...$ which is again sequence A062980 of the On-line Encyclopedia of Integer Sequences.

4 Counting affine closed terms

We have just to add the case $n\neq 0$* and abstraction without binding*. Since no index is added, the size increases by $1$. The numbers are written $a^{`n}_{n,\mathbf{m}}$, $a^{0}_{n,\mathbf{m}}$, $a^{1}_{n,\mathbf{m}}$, and $a_{n,\mathbf{m}}$ when the size does not matter. There are $(0:\mathbf{m})$-SwissCheeses of size $n$ that are abstraction without binding. We get the recursive formulas:

4.1 Natural size

[TABLE]

The numbers of closed affine size with natural size are given in Figure 4.

4.2 Variable size [math]

[TABLE]

The sequence $a^{0}_{n,0^{`w}}$ of the numbers of affine closed terms for variable size [math] is

[TABLE]

It does not appear in the On-line Encyclopedia of Integer Sequences. It corresponds to the coefficients of the generating function $\mathcal{A}(z,0)$ where

[TABLE]

4.3 Variable size $1$

[TABLE]

The sequence $a^{1}_{n,0^{`w}}$ of the numbers of affine closed terms for variable size $1$ is

[TABLE]

This is sequence A281270 in the On-line Encyclopedia of Integer Sequences. However it corresponds to the coefficient of the generating function $\hat{\mathcal{A}}(z,0)$ where $\hat{\mathcal{A}}(z,u)$ is the solution of the functional equation:

[TABLE]

Notice that this corrects the wrong assumptions of [13] (Section 6.2).

5 Generating functions

Consider families $F_{\mathbf{m}}(z)$ of generating functions indexed by $\mathbf{m}$, where $\mathbf{m}$ is an infinite tuple of naturals. In fact, we are interested in the infinite tuples $\mathbf{m}$ that are always [math], except a finite number of indices, in order to compute $F_{0^{`w}}(z)$, which corresponds to closed $`l$-terms. Let $\mathbf{u}$ stands for the infinite sequences of variables $(u_{0},u_{1},...)$ and $\mathbf{u}^{\mathbf{m}}$ stands for $(u_{0}^{m_{0}},u_{1}^{m_{1}},...,u_{n}^{m_{n}},...)$ and $\mathsf{tail}\,(\mathbf{u})$ stand for $(u_{1},...)$. We consider the series of two variables $z$ and $\mathbf{u}$ or double series associated with $F_{\mathbf{m}}(z)$:

[TABLE]

Natural size

$L^{`n}_{\mathbf{m}}(z)$ is associated with the numbers of closed linear SwissCheeses for natural size:

[TABLE]

$L^{`n}_{0^{`w}}$ is the generating function for the closed linear $`l$-terms. $\mathcal{L}^{`n}(z,\mathbf{u})$ is the double series associated with $L^{`n}_{\mathbf{m}}(z)$ and is solution of the equation:

[TABLE]

$\mathcal{L}^{`n}(z,0^{`w})$ is the generating function of closed linear $`l$-terms.

For closed affine SwissCheeses we get:

[TABLE]

$A^{`n}_{0^{`w}}$ is the generating function for the closed linear $`l$-terms. $\mathcal{A}^{`n}(z,\mathbf{u})$ is the double series associated with $A^{`n}_{\mathbf{m}}(z)$ and is solution of the equation:

[TABLE]

$\mathcal{A}^{`n}(z,0^{`w})$ is the generating function of closed affine $`l$-terms.

Variable size [math]

$L^{0}_{\mathbf{m}}$ is associated with the numbers of closed linear SwissCheeses for variable size [math]:

[TABLE]

$L^{0}_{0^{`w}}$ is the generating function for the closed linear $`l$-terms. $\mathcal{L}^{0}(z,\mathbf{u})$ is the double series associated with $L^{0}_{\mathbf{m}}(z)$ and is solution of the equation:

[TABLE]

$\mathcal{L}^{0}(z,0^{`w})$ is the generating function of closed linear $`l$-terms.

For closed affine SwissCheeses we get:

[TABLE]

$A^{0}_{0^{`w}}$ is the generating function for the affine linear $`l$-terms. $\mathcal{A}^{0}(z,\mathbf{u})$ is the double series associated with $A^{0}_{\mathbf{m}}(z)$ and is solution of the equation:

[TABLE]

$\mathcal{A}^{0}(z,0^{`w})$ is the generating function of closed linear $`l$-terms.

Variable size $1$

The generating functions for $l^{1}_{n,\mathbf{m}}$ are:

[TABLE]

Then we get as associated double series :

[TABLE]

6 Effective computations

The definition of the coefficients $a^{`n}_{\mathbf{m}}$ and others is highly recursive and requires a mechanism of memoization. In Haskell, this can be done by using the call by need which is at the core of this language. Assume we want to compute the values of $a^{`n}_{\mathbf{m}}$ until a value upBound for $n$. We use a recursive data structure:

data Mem = Mem [Mem] | Load [Integer]

in which we store the computed values of a function

a :: Int -> [Int] -> Integer

In our implementation the depth of the recursion of Mem is limited by upBound, which is also the longest tuple $\mathbf{m}$ for which we will compute $a^{`n}_{\mathbf{m}}$. Associated with Mem there is a function

access :: Mem -> Int -> [Int] -> Integer access (Load l) n [] = l !! n access (Mem listM) n (k:m) = access (listM !! k) n m

The leaves of the tree memory, corresponding to Load, contains the values of the function:

memory :: Int -> [Int] -> Mem memory 0 m = Load [a n (reverse m) | n<-[0..]] memory k m = Mem [memory (k-1) (j:m) | j<-[0..]]

The memory relative to the problem we are interested in is

theMemory = memory (bound) []

and the access to theMemory is given by a specific function:

acc :: Int -> [Int] -> Integer acc n m = access theMemory n m

Notice that a and acc have the same signature. This is not a coincidence, since acc accesses values of a already computed. Now we are ready to express a:

a 0 m = iv (head m == 1 && all ((==) 0) (tail m)) a n m = aAPP n m + aABSwB n m + aABSnB n m

aAPP counts affine terms that are applications:

aAPP n m = sum (map (((q,r),(k,nk))->(acc k q)*(acc nk r)) (allCombinations m (n-1)))

where allCombinations returns a list of all the pairs of pairs $(\mathbf{m}^{\prime},\mathbf{m}^{\prime\prime})$ such $\mathbf{m}=\mathbf{m}^{\prime}`(+)\mathbf{m}^{\prime\prime}$ and of pairs $(k,nk)$ such that $k+nk=n$. aABSwB counts affine terms that are abstractions with binding.

aABSwB n m | head m == 0 = sum [aABSAtD n m i |i<-[1..(n-1)]] | otherwise = 0

aABSAtD counts affine terms that are abstractions with binding at level $i$:

aABSAtD n m i = (fromIntegral (1 + m!!i))*(acc (n-i-1) (tail (inc i m) ++ [0]))

aABSnB counts affine terms that are abstractions with no binding:

aABSnB n m | head m == 0 = (acc (n-1) (tail m ++ [0])) | otherwise = 0

Anyway the efficiency of this program is limited by the size of the memory, since for computing $a^{`n}_{n,0^{n}}$, for instance, we need to compute $a^{`n}_{\mathbf{r}}$ for about $n!$ values.

7 Generating affine and linear terms

By relatively small changes it is possible to build programs which generate linear and affine terms. For instance for generating affine terms we get.

amg :: Int -> [Int] -> [SwissCheese] amg 0 m = if (head m == 1 && all ((==) 0) (tail m)) then [Box 0] else [] amg n m = allAPP n m ++ allABSwB n m ++ allABSnB n m

allAPP :: Int -> [Int] -> [SwissCheese] allAPP n m = foldr (++) [] (map (((q,r),(k,nk))-> appSC (cartesian (accAG k q) (accAG nk r)) (allCombinations m (n-1)))

allABSAtD :: Int -> [Int] -> Int -> [SwissCheese] allABSAtD n m i = foldr (++) [] (map (abstract (i-1)) (accAG (n - i - 1) (tail (inc i m) ++ [0])))

allABSwB :: Int -> [Int] -> [SwissCheese] allABSwB n m | head m == 0 = foldr (++) [] [allABSAtD n m i |i<-[1..(n-1)]] | otherwise = []

allABSnB :: Int -> [Int] -> [SwissCheese] allABSnB n m | head m == 0 = map (AbsSC . raise) (accAG (n-1) (tail m ++ [0])) | otherwise = []

memoryAG :: Int -> [Int] -> MemSC memoryAG 0 m = LoadSC [amg n (reverse m) | n<-[0..]] memoryAG k m = MemSC [memoryAG (k-1) (j:m) | j<-[0..]]

theMemoryAG = memoryAG (upBound) []

accAG :: Int -> [Int] -> [SwissCheese] accAG n m = accessSC theMemoryAG n m

From this, we get programs for generating random affine terms or random linear terms as follows: if we want a random closed linear term of a given size $n$, we throw a random number, say $p$, between $1$ and $l_{n,0^{n}}$ and we look for the $p^{th}$ in the list of all the closed linear terms of size $n$. Haskell laziness mimics the unranking. Due to high requests in space, we cannot go further than the random generation of closed linear terms of size $23$ and closed affine terms of size $19$ . There are similar programs for generating all the terms of size $n$ for variable size [math] and variable size $1$.

8 Normal forms

From the method used for counting affine and linear closed terms, it is easy to deduce method for counting affine and linear closed normal forms. Like before, we use SwissCheeses. In this section we consider only natural size.

8.1 Natural size

Affine closed normal forms

Let us call $anf^{`n}_{n,\mathbf{m}}$ the numbers of affine SwissCheeses with no $`b$-redex and $ane^{`n}_{n,\mathbf{m}}$ the numbers of neutral affine SwissCheeses, i.e., affine SwissCheeses with no $`b$-redexes that are sequences of applications starting with a de Bruijn index. In addition we count:

• •

$anf^{`n}`lw_{n,m}$ the number of affine SwissCheeses with no $`b$-redex which are abstraction with a binding of a de Bruijn index,

• •

$anf^{`n}`ln_{n,m}$ the number of affine SwissCheeses with no $`b$-redex which are abstraction with no binding.

[TABLE]

where

[TABLE]

and

[TABLE]

and

[TABLE]

There are two generating functions, $\mathcal{A}^{nf}$ and $\mathcal{A}^{ne}$, which are associated to $anf^{`n}_{n,\mathbf{m}}$ and $anf^{`n}_{n,\mathbf{m}}$:

[TABLE]

Linear closed normal forms

Let us call $lnf^{`n}_{n,\mathbf{m}}$ the numbers of linear SwissCheeses with no $`b$-redex and $lne^{`n}_{n,\mathbf{m}}$ the numbers of neutral linear SwissCheeses, linear SwissCheeses with no $`b$-redexes that are sequences of applications starting with a de Bruijn index. In addition we count $lnf^{`n}`lw_{n,m}$ the number of linear SwissCheeses with no $`b$-redex which are abstraction with a binding of a de Bruijn index.

[TABLE]

where

[TABLE]

and

[TABLE]

with the two generating functions:

[TABLE]

We also deduce programs for generating all the closed affine or linear normal forms of a given size from which we deduce programs for generating random closed affine or linear normal forms of a given size. For instance, here are three randoms linear closed normal forms (using de Bruijn indices) of natural size $28$:

[TABLE]

8.2 Variable size [math]

Linear closed normal forms

A little like previously, let us call $lnf^{0}_{n,\mathbf{m}}$ the numbers of linear SwissCheeses with no $`b$-redex and $lne^{0}_{n,\mathbf{m}}$ the numbers of neutral linear SwissCheeses, linear SwissCheeses with no $`b$-redexes that are sequences of applications starting with a de Bruijn index. In addition we count $lnf^{0}`lw_{n,m}$ the number of linear SwissCheeses with no $`b$-redex which are abstraction with a binding of a de Bruijn index. We assume that the reader knows now how to proceed.

[TABLE]

where

[TABLE]

[TABLE]

and the two generating functions:

[TABLE]

With no surprise we get for $lnf^{0}_{n,0^{n}}$ the sequence:

[TABLE]

mentioned by Zeilberger in [19] and listing the coefficients of the generating function $\mathcal{L}^{nf,0}(z,0^{`w})$.

We let the reader deduce how to count closed affine normal forms for variable size [math] and closed linear and affine normal forms for variable size $1$ alike. Notice that the Haskell programs are on the GitHub site.

9 Related works and Acknowledgement

There are several works on counting $`l$-terms, for instance on natural size [3, 2], on variable size $1$ [5, 10, 18], on variable size [math] [14], on affine terms with variable size 1 [7, 6], on linear $`l$-terms [21, 19, 20], also on a size based binary representation of the $`l$-calculus [15] (see [12] for a synthetic view of both natural size and binary size).

The basic idea of this work comes from a discussion with Maciej Bendkowski, Olivier Bodini, Sergey Dovgal and Katarzyna Grygiel, I thank them as I thank Noam Zeilberger for interactions.

10 Conclusion

This presentation shares similarity with this of  [14, 15, 4]. Instead of considering the size $n$ and the bound $m$ of free indices like in expressions of the form:

[TABLE]

here we replace $m$ by the characteristic $\mathbf{m}$. We can imagine a common framework. On another hand, as noticed by Paul Tarau, this approach has features of dynamic programming [9], which makes it somewhat efficient.

Data

In the appendix, we give the first values of $l^{`n}_{n,0^{n}}$, $a^{`n}_{n,0^{n}}$, and $anf^{`n}_{n,0^{n}}$.