Browse Source

Almost finish writing assignment 1

master
L.E.R 10 months ago
parent
commit
8e415b9fbd
5 changed files with 785 additions and 0 deletions
  1. 261
    0
      .gitignore
  2. 11
    0
      .vscode/settings.json
  3. 99
    0
      hw1/defs.tex
  4. BIN
      hw1/wr1.pdf
  5. 414
    0
      hw1/wr1.tex

+ 261
- 0
.gitignore View File

@@ -22,3 +22,264 @@ cabal.project.local~
.ghc.environment.*
*.exe
## Core latex/pdflatex auxiliary files:
*.aux
*.lof
*.log
*.lot
*.fls
*.out
*.toc
*.fmt
*.fot
*.cb
*.cb2
.*.lb
## Intermediate documents:
*.dvi
*.xdv
*-converted-to.*
# these rules might exclude image files for figures etc.
# *.ps
# *.eps
# *.pdf
## Generated if empty string is given at "Please type another file name for output:"
.pdf
## Bibliography auxiliary files (bibtex/biblatex/biber):
*.bbl
*.bcf
*.blg
*-blx.aux
*-blx.bib
*.run.xml
## Build tool auxiliary files:
*.fdb_latexmk
*.synctex
*.synctex(busy)
*.synctex.gz
*.synctex.gz(busy)
*.pdfsync
## Build tool directories for auxiliary files
# latexrun
latex.out/
## Auxiliary and intermediate files from other packages:
# algorithms
*.alg
*.loa
# achemso
acs-*.bib
# amsthm
*.thm
# beamer
*.nav
*.pre
*.snm
*.vrb
# changes
*.soc
# comment
*.cut
# cprotect
*.cpt
# elsarticle (documentclass of Elsevier journals)
*.spl
# endnotes
*.ent
# fixme
*.lox
# feynmf/feynmp
*.mf
*.mp
*.t[1-9]
*.t[1-9][0-9]
*.tfm
#(r)(e)ledmac/(r)(e)ledpar
*.end
*.?end
*.[1-9]
*.[1-9][0-9]
*.[1-9][0-9][0-9]
*.[1-9]R
*.[1-9][0-9]R
*.[1-9][0-9][0-9]R
*.eledsec[1-9]
*.eledsec[1-9]R
*.eledsec[1-9][0-9]
*.eledsec[1-9][0-9]R
*.eledsec[1-9][0-9][0-9]
*.eledsec[1-9][0-9][0-9]R
# glossaries
*.acn
*.acr
*.glg
*.glo
*.gls
*.glsdefs
# gnuplottex
*-gnuplottex-*
# gregoriotex
*.gaux
*.gtex
# htlatex
*.4ct
*.4tc
*.idv
*.lg
*.trc
*.xref
# hyperref
*.brf
# knitr
*-concordance.tex
# TODO Comment the next line if you want to keep your tikz graphics files
*.tikz
*-tikzDictionary
# listings
*.lol
# makeidx
*.idx
*.ilg
*.ind
*.ist
# minitoc
*.maf
*.mlf
*.mlt
*.mtc[0-9]*
*.slf[0-9]*
*.slt[0-9]*
*.stc[0-9]*
# minted
_minted*
*.pyg
# morewrites
*.mw
# nomencl
*.nlg
*.nlo
*.nls
# pax
*.pax
# pdfpcnotes
*.pdfpc
# sagetex
*.sagetex.sage
*.sagetex.py
*.sagetex.scmd
# scrwfile
*.wrt
# sympy
*.sout
*.sympy
sympy-plots-for-*.tex/
# pdfcomment
*.upa
*.upb
# pythontex
*.pytxcode
pythontex-files-*/
# tcolorbox
*.listing
# thmtools
*.loe
# TikZ & PGF
*.dpth
*.md5
*.auxlock
# todonotes
*.tdo
# vhistory
*.hst
*.ver
# easy-todo
*.lod
# xcolor
*.xcp
# xmpincl
*.xmpi
# xindy
*.xdy
# xypic precompiled matrices
*.xyc
# endfloat
*.ttt
*.fff
# Latexian
TSWLatexianTemp*
## Editors:
# WinEdt
*.bak
*.sav
# Texpad
.texpadtmp
# LyX
*.lyx~
# Kile
*.backup
# KBibTeX
*~[0-9]*
# auto folder when using emacs and auctex
./auto/*
*.el
# expex forward references with \gathertags
*-tags.tex
# standalone packages
*.sta

+ 11
- 0
.vscode/settings.json View File

@@ -0,0 +1,11 @@
{
"latex-workshop.latex.recipes": [
{
"name": "pdflatex*2",
"tools": [
"pdflatex",
"pdflatex"
]
}
]
}

+ 99
- 0
hw1/defs.tex View File

@@ -0,0 +1,99 @@
%% FILENAME: defs.tex
%% AUTHOR: Cameron Swords
\usepackage{amsmath, listings, amsthm, amssymb, proof, xspace}
%%------------------------------------------------------------------------
%% DEFINITION HELPERS
%%------------------------------------------------------------------------
\newcommand{\alt}{~~|~~}
\newcommand{\comp}[1]{\llbracket #1 \rrbracket}
\newcommand{\inlinexp}[1]{
{\footnotesize
\[\begin{array}{l}
#1
\end{array}\]}}
\newcommand{\inlinexpa}[2]{
{\footnotesize
\[\begin{array}{#1}
#2
\end{array}\]}}
\newcommand{\infr} [3] [] {\infer[\textsc{#1}]{#3}{#2}}
\newcommand{\iand} {\qquad}
\newcommand{\Ctxt} {\mathcal{E}}
\newcommand{\InCtxt} [1] {\Ctxt[#1]}
%%------------------------------------------------------------------------
%% REDUCTION RELATION MACROS
%%------------------------------------------------------------------------
\newcommand{\subst} [3] {#3 [#2 / #1]}
\newcommand{\dstep} [2] {#1 ~\Downarrow~ #2}
\newcommand{\rstep} [2] {#1 ~\rightarrow~ #2}
\newcommand{\ssosredex} {\rightarrow}
\newcommand{\ctxtreduce} {\mapsto}
\newcommand{\sstep} [3] [] {#2 &\ssosredex& #3 &\textsc{#1}}
\newcommand{\ctxtstep} [3] [] {#2 &\ctxtreduce& #3 &\textsc{#1}}
%%------------------------------------------------------------------------
%% TYPE DEFINITION MACROS
%%------------------------------------------------------------------------
\newcommand{\funct} [2] {#1\nobreak\rightarrow\nobreak#2}
\newcommand{\boolt} {\mathtt{bool}}
\newcommand{\typeEnv} {\Gamma}
\newcommand{\entails} {\vdash}
\newcommand{\judgment} [3] {#1 \entails #2 : #3}
\newcommand{\envent} [2] {\judgment{\typeEnv}{#1}{#2}}
\newcommand{\extenvent} [4] {\judgment{\typeEnv, #1 : #2}{#3}{#4}}
\newcommand{\envlookup} [3] {\infr{#1(#2) = #3}{\judgment{#1}{#2}{#3}}}
%%------------------------------------------------------------------------
%% EXPRESSION MACROS
%%------------------------------------------------------------------------
%% lambda
\newcommand{\lamdefe} [2] {\lambda #1.~#2}
\newcommand{\lamdefea} [2] {\begin{array}{l}\lambda#1.\\\hspace*{.5em}#2\\\end{array}}
%% let
\newcommand{\letdefe} [3] {\letbind{#1}{#2}~\letin{#3}}
\newcommand{\letdefarre} [3] {\begin{array}{l}\letbind{#1}{#2}\\\letin{#3})\\\end{array}}
\newcommand{\letbind} [2] {\mathsf{let}~\lbind{#1}{#2}}
\newcommand{\letbindp} [2] {\mathsf{let}~(\lbind{#1}{#2})}
\newcommand{\lbind} [2] {#1=#2}
\newcommand{\letin} [1] {\mathsf{in}~#1}
%% if
\newcommand{\ife} [3] {\ifline{#1}~\thenline{#2}~\elseline{#3}}
\newcommand{\ifea} [3] {\begin{array}{l}\ifline{#1}\\\thenline{#2}\\\elseline{#3}\end{array}}
\newcommand{\ifop} {\mathsf{if}}
\newcommand{\ifline} [1] {\ifop~ #1}
\newcommand{\thenline} [1] {\mathsf{then}~#1}
\newcommand{\elseline} [1] {\mathsf{else}~#1}
%% opers
\newcommand{\binopdef} {\mathit{binop}}
\newcommand{\unopdef} {\mathit{unop}}
\newcommand{\binope} [2] {\binopdef~#1~#2}
\newcommand{\unope} [1] {\unopdef~#1}
\newcommand{\andop} {\mathsf{and}}
\newcommand{\orop} {\mathsf{or}}
\newcommand{\notop} {\mathsf{not}}
\newcommand{\ande} [2] {\mathsf{and}~#1~#2}
\newcommand{\ore} [2] {\mathsf{or}~#1~#2}
\newcommand{\note} [1] {\mathsf{not}~#1}
%% values
\newcommand{\falsev} {\mathsf{false}}
\newcommand{\truev} {\mathsf{true}}

BIN
hw1/wr1.pdf View File


+ 414
- 0
hw1/wr1.tex View File

@@ -0,0 +1,414 @@
\documentclass[a4paper]{article}
\usepackage{geometry}
\usepackage{graphicx}
\usepackage{natbib}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{paralist}
\usepackage{epstopdf}
\usepackage{tabularx}
\usepackage{longtable}
\usepackage{multirow}
\usepackage{multicol}
\usepackage[hidelinks]{hyperref}
\usepackage{fancyvrb}
\usepackage{algorithm}
\usepackage{algorithmic}
\usepackage{float}
\usepackage{listings}
\usepackage[svgname]{xcolor}
\usepackage{enumerate}
\usepackage{array}
\usepackage{times}
\usepackage{url}
\usepackage{fancyhdr}
\usepackage{comment}
\usepackage{environ}
\usepackage{times}
\usepackage{textcomp}
\usepackage{caption}
\urlstyle{rm}
\setlength\parindent{0pt} % Removes all indentation from paragraphs
\theoremstyle{definition}
\newtheorem{definition}{Definition}[]
\newtheorem{conjecture}{Conjecture}[]
\newtheorem{example}{Example}[]
\newtheorem{theorem}{Theorem}[]
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\floatname{algorithm}{Procedure}
\renewcommand{\algorithmicrequire}{\textbf{Input:}}
\renewcommand{\algorithmicensure}{\textbf{Output:}}
\newcommand{\abs}[1]{\lvert#1\rvert}
\newcommand{\norm}[1]{\lVert#1\rVert}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\br}[1]{\{#1\}}
\DeclareMathOperator*{\argmin}{arg\,min}
\DeclareMathOperator*{\argmax}{arg\,max}
\renewcommand{\qedsymbol}{$\blacksquare$}
\definecolor{dkgreen}{rgb}{0,0.6,0}
\definecolor{gray}{rgb}{0.5,0.5,0.5}
\definecolor{mauve}{rgb}{0.58,0,0.82}
\newcommand{\Var}{\mathrm{Var}}
\newcommand{\Cov}{\mathrm{Cov}}
\newcommand{\vc}[1]{\boldsymbol{#1}}
\newcommand{\xv}{\vc{x}}
\newcommand{\Sigmav}{\vc{\Sigma}}
\newcommand{\alphav}{\vc{\alpha}}
\newcommand{\muv}{\vc{\mu}}
\newcommand{\red}[1]{\textcolor{red}{#1}}
\def\x{\mathbf x}
\def\y{\mathbf y}
\def\w{\mathbf w}
\def\v{\mathbf v}
\def\E{\mathbb E}
\def\V{\mathbb V}
% TO SHOW SOLUTIONS, include following (else comment out):
\newenvironment{soln}{
\leavevmode\color{blue}\ignorespaces
}{}
\hypersetup{
% colorlinks,
linkcolor={red!50!black},
citecolor={blue!50!black},
urlcolor={blue!80!black}
}
\geometry{
top=1in, % <-- you want to adjust this
inner=1in,
outer=1in,
bottom=1in,
headheight=3em, % <-- and this
headsep=2em, % <-- and this
footskip=3em,
}
\lstset{
basicstyle=\ttfamily,
columns=fullflexible,
breaklines=true,
keepspaces=true,
postbreak=\raisebox{0ex}[0ex][0ex]{\color{red}$\hookrightarrow$\space}
}
%%------------------------------------------------------------------------
%% DEFINITION HELPERS
%%------------------------------------------------------------------------
\input{defs.tex}
\pagestyle{fancyplain}
\lhead{\fancyplain{}{Homework 1: Written Assignment}}
\rhead{\fancyplain{}{CS 538 Theory and Design of Programming Languages}}
\cfoot{\thepage}
\title{\textsc{CS 538, Spring 2019}} % Title
%%% NOTE: Replace 'NAME HERE' etc., and delete any "\red{}" wrappers (so it won't show up as red)
\author{
Everette Rong \\
yrong9@wisc.edu \\
rong@cs.wisc.edu \\
% \red{$>>$ID HERE$<<$}\\
}
\date{}
\begin{document}
\maketitle
\begin{center}
\Huge
HW1: Written Assignment 1
\end{center}
\section{Calculator language: Syntax (10)}
Translate this English description of the language into a grammar.
\begin{soln}
\begin{lstlisting}
digit = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
num = digit { digit }
bool = "tt" | "ff" (* boolean constants *)
int = [ "-" ] num (* positive/negative int *)
ae = int (* integer constants *)
| ae "+" ae (* addition *)
| ae "*" ae (* multiplication *)
| "if" be "then" ae "else" ae (* if-then-else *)
be = bool (* boolean constants *)
| be "&&" be (* logical and *)
| be "||" be (* logical or *)
| ae "==" ae (* equals *)
| ae "<" ae (* less than *)
\end{lstlisting}
\end{soln}
\section{Calculator language: Operational semantics (10)}
\begin{enumerate}
\item Give a small-step operational semantics for our calculator language.
\begin{soln}
Preliminaries:
\begin{itemize}
\item Both addition and multiplication will be calculated from left to right.
\item $add$ and $times$ mean the actual mathematical calculation of $+$ and $*$.
\item $\land$ and $\lor$ mean the actual logical operation of $and$ and $or$.
\item $-$ on the top means there is no step.
\item $e_i$ means the corresponding expression (int ($ae$) or bool ($be$)) in those steps.
\item $n_i$ represents an int constant, and $b_i$ represents a bool constant.
\end{itemize}
If-then-else (\textit{lazy-if}):
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{be_1}{be_1'}}
{\rstep{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2)}{(\text{if } be_1' \text{ then } ae_1 \text{ else } ae_2)}}
\\
\\
\infr[(2)]
{b_1 == tt}
{\rstep{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2)}{ae_1}}
\\
\\
\infr[(3)]
{b_1 == ff}
{\rstep{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2)}{ae_2}}
\end{array}
\]
Integer Addition:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1 + e_2}{e_1' + e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{n_1 + e_2}{n_1 + e_2'}}
\\
\\
\infr[$n_3 = add(n_1, n_2)$ (3)]
{-}
{\rstep{n_1 + n_2}{n_3}}
\end{array}
\]
Similarly, Integer Multiplication:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1 * e_2}{e_1' * e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{n_1 * e_2}{n_1 * e_2'}}
\\
\\
\infr[$n_3 = times(n_1, n_2)$ (3)]
{-}
{\rstep{n_1 * n_2}{n_3}}
\end{array}
\]
Boolean Logical And:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1 \ \&\&\ e_2}{e_1'\ \&\&\ e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{e_1\ \&\&\ e_2}{e_1\ \&\&\ e_2'}}
\\
\\
\infr[$b_3 = (b_1 \land b_2)$ (3)]
{-}
{\rstep{b_1\ \&\&\ b_2}{b_3}}
\end{array}
\]
Boolean Logical Or:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1\ ||\ e_2}{e_1'\ ||\ e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{e_1\ ||\ e_2}{e_1\ ||\ e_2'}}
\\
\\
\infr[$b_3 = (b_1 \lor b_2)$ (3)]
{-}
{\rstep{b_1\ ||\ b_2}{b_3}}
\end{array}
\]
Integer Equal:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1 == e_2}{e_1' == e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{e_1 == e_2}{e_1 == e_2'}}
\\
\\
\infr[$b_3 = (b_1 == b_2)$ (3)]
{-}
{\rstep{b_1 == b_2}{b_3}}
\end{array}
\]
Integer Less than:
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{e_1}{e_1'}}
{\rstep{e_1 < e_2}{e_1' < e_2}}
\\
\\
\infr[(2)]
{\rstep{e_2}{e_2'}}
{\rstep{e_1 < e_2}{e_1 < e_2'}}
\\
\\
\infr[$b_3 = (b_1 < b_2)$ (3)]
{-}
{\rstep{b_1 < b_2}{b_3}}
\end{array}
\]
\end{soln}
\item
\begin{itemize}
\item Give an alternative operational semantics for if-then-else that evaluates both bodies before evaluating
the guard
\begin{soln}
If-then-else (\textit{eager-if}):
\[
\begin{array}{rcll}
\infr[(1)]
{\rstep{ae_1}{ae_1'}}
{\rstep{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2)}{(\text{if } be_1 \text{ then } ae_1' \text{ else } ae_2)}}
\\
\\
\infr[(2)]
{\rstep{ae_2}{ae_2'}}
{\rstep{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2)}{(\text{if } be_1 \text{ then } ae_1 \text{ else } ae_2')}}
\\
\\
\infr[(3)]
{b_1 == tt}
{\rstep{(\text{if } be_1 \text{ then } n_1 \text{ else } n_2)}{n_1}}
\\
\\
\infr[(4)]
{b_1 == ff}
{\rstep{(\text{if } be_1 \text{ then } n_1 \text{ else } n_2)}{n_2}}
\end{array}
\]
\end{soln}
\item What are some reasons to prefer \textit{lazy-if} over \textit{eager-if} ?
\begin{soln}
In \textit{lazy-if}, we don't need to calculate both expression before we can get the final result. We always evaluate one bool condition, and one arithmatic expression.
\textit{Eager-if} on the other hand, requires us to always evaluate one bool condition and two arithmatic expressions. \\
Also, \textit{lazy-if} won't stuck in an expression that will never be reached, while \textit{eager-if} would always stuck if any expression is problematic.
\end{soln}
\end{itemize}
\end{enumerate}
\section{Lambda calculus (5)}
Evaluate each of the following programs until it reaches a value, or returns to the original program. Show
each step in the evaluation.
\begin{enumerate}
\item $(\lambda f \cdot \lambda x \cdot f x) (\lambda x \cdot x + 1) 5$\\
\begin{soln}
$= (\lambda x \cdot (\lambda a \cdot a+1)\ x)\ 5$ \\
$= (\lambda x \cdot x + 1)\ 5 $ \\
$= 5+1$ \\
$= 6$
\end{soln}
\item $(\lambda f \cdot \lambda x \cdot \lambda y \cdot f\ y\ x)\ (\lambda x \cdot \lambda y \cdot x-y)\ 5\ 3$ \\
\begin{soln}
$=(\lambda x \cdot \lambda y \cdot (\lambda a \cdot \lambda b \cdot a-b)\ y\ x)\ 5\ 3$ \\
$=(\lambda y \cdot (\lambda x \cdot \lambda a \cdot x - a)\ y\ 5)\ 3$ \\
$=(\lambda x \cdot \lambda y \cdot x - y)\ 3\ 5$ \\
$=3 - 5$ \\
$=-2$
\end{soln}
\item $(\lambda x \cdot x\ x)\ (\lambda x \cdot x\ x)$ \\
\begin{soln}
$=(\lambda x \cdot x\ x)\ (\lambda x \cdot x\ x)$ \\
$=(\lambda x \cdot x\ x)\ (\lambda x \cdot x\ x)$ \\
$=...$
\end{soln}
\end{enumerate}
\section{Recursion (5)}
Use the program construct $fix f. e$ we introduced to write a lambda calculus function that takes in a natural
number $n$ and returns the $n-th$ Fibonacci number $fib(n)$.
\begin{soln}
$$
fib = fix\ f.\ \lambda n.\ \text{ if } n = 1 \text{ then } 1 \text{ else } (\text{ if } n = 2 \text{ then } 1 \text{ else } f(n-1)+f(n-2))
$$
\end{soln}
\clearpage % do not erase this!
\bibliographystyle{apalike}
%----------------------------------------------------------------------------------------
\end{document}

Loading…
Cancel
Save