petit-lambda

Feature

• You can trace reduction process of lambda calculus step by step.
• Output format of trace can be selected, including LaTex source code.

Example

input file(tracelatex.lmd)

- a sample generating latex file - suppress redundant messages set response off - generate trace output as latex source code set tracer latex - specify the file name to be the destination of trace. The trace will be appended if the file already exist. set traceoutput tracelatex.tex - reduce expressions in applicative order. set order applicative -> \documentclass{jarticle} -> \title{Latexo—ΝƒTƒ“ƒvƒ‹} -> \author{‘ε˜a’JŒ‰} -> \begin{document} -> \maketitle def One = ^x.^y.x y def Times = ^l.^r.^x.l (r x) -> \subsection*{\(Times One One\)‚ΜŠΘ–ρ‰ί’φ} reduce Times One One -> \end{document}

Execute

bash$ ./petitlambda tracelatex.lmd

Output(tracelatex.tex)

\documentclass{jarticle} \title{Latexo—ΝƒTƒ“ƒvƒ‹} \author{‘ε˜a’JŒ‰} \begin{document} \maketitle \subsection*{\(Times One One\)‚ΜŠΘ–ρ‰ί’φ} \begin{eqnarray*} &&\underline{Times}~One~One\\ && =~(\lambda l.\lambda r.\lambda x.l~(r~x))~\underline{One}~One\\ && =~(\lambda l.\lambda r.\lambda x.l~(r~x))~(\lambda x.\underline{\lambda y.x~y})~One\\ && \rightarrow_{\eta} \underline{(\lambda l.\lambda r.\lambda x.l~(r~x))~(\lambda x.x)}~One\\ && \rightarrow_{\beta} (\lambda r.\lambda x.\underline{(\lambda x.x)~(r~x)})~One\\ && \rightarrow_{\beta} (\lambda r.\underline{\lambda x.r~x})~One\\ && \rightarrow_{\eta} (\lambda r.r)~\underline{One}\\ && =~(\lambda r.r)~(\lambda x.\underline{\lambda y.x~y})\\ && \rightarrow_{\eta} \underline{(\lambda r.r)~(\lambda x.x)}\\ && \rightarrow_{\beta} \lambda x.x \end{eqnarray*} \end{document}

the result of typeset

Package

Install

For cygwin and solaris-sparc, executable file is included in the package.

For other platform, on command line, do

install

Execute

Document