518 lines
15 KiB
HTML
Executable File
518 lines
15 KiB
HTML
Executable File
<?xml version="1.0" encoding="utf-8"?>
|
||
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
|
||
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
|
||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
|
||
<head>
|
||
<!-- 2025-12-28 Sun 20:37 -->
|
||
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
|
||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||
<title>afp_lec_1</title>
|
||
<meta name="generator" content="Org Mode" />
|
||
<style type="text/css">
|
||
#content { max-width: 60em; margin: auto; }
|
||
.title { text-align: center;
|
||
margin-bottom: .2em; }
|
||
.subtitle { text-align: center;
|
||
font-size: medium;
|
||
font-weight: bold;
|
||
margin-top:0; }
|
||
.todo { font-family: monospace; color: red; }
|
||
.done { font-family: monospace; color: green; }
|
||
.priority { font-family: monospace; color: orange; }
|
||
.tag { background-color: #eee; font-family: monospace;
|
||
padding: 2px; font-size: 80%; font-weight: normal; }
|
||
.timestamp { color: #bebebe; }
|
||
.timestamp-kwd { color: #5f9ea0; }
|
||
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
|
||
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
|
||
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
|
||
.underline { text-decoration: underline; }
|
||
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
|
||
p.verse { margin-left: 3%; }
|
||
pre {
|
||
border: 1px solid #e6e6e6;
|
||
border-radius: 3px;
|
||
background-color: #f2f2f2;
|
||
padding: 8pt;
|
||
font-family: monospace;
|
||
overflow: auto;
|
||
margin: 1.2em;
|
||
}
|
||
pre.src {
|
||
position: relative;
|
||
overflow: auto;
|
||
}
|
||
pre.src:before {
|
||
display: none;
|
||
position: absolute;
|
||
top: -8px;
|
||
right: 12px;
|
||
padding: 3px;
|
||
color: #555;
|
||
background-color: #f2f2f299;
|
||
}
|
||
pre.src:hover:before { display: inline; margin-top: 14px;}
|
||
/* Languages per Org manual */
|
||
pre.src-asymptote:before { content: 'Asymptote'; }
|
||
pre.src-awk:before { content: 'Awk'; }
|
||
pre.src-authinfo::before { content: 'Authinfo'; }
|
||
pre.src-C:before { content: 'C'; }
|
||
/* pre.src-C++ doesn't work in CSS */
|
||
pre.src-clojure:before { content: 'Clojure'; }
|
||
pre.src-css:before { content: 'CSS'; }
|
||
pre.src-D:before { content: 'D'; }
|
||
pre.src-ditaa:before { content: 'ditaa'; }
|
||
pre.src-dot:before { content: 'Graphviz'; }
|
||
pre.src-calc:before { content: 'Emacs Calc'; }
|
||
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
|
||
pre.src-fortran:before { content: 'Fortran'; }
|
||
pre.src-gnuplot:before { content: 'gnuplot'; }
|
||
pre.src-haskell:before { content: 'Haskell'; }
|
||
pre.src-hledger:before { content: 'hledger'; }
|
||
pre.src-java:before { content: 'Java'; }
|
||
pre.src-js:before { content: 'Javascript'; }
|
||
pre.src-latex:before { content: 'LaTeX'; }
|
||
pre.src-ledger:before { content: 'Ledger'; }
|
||
pre.src-lisp:before { content: 'Lisp'; }
|
||
pre.src-lilypond:before { content: 'Lilypond'; }
|
||
pre.src-lua:before { content: 'Lua'; }
|
||
pre.src-matlab:before { content: 'MATLAB'; }
|
||
pre.src-mscgen:before { content: 'Mscgen'; }
|
||
pre.src-ocaml:before { content: 'Objective Caml'; }
|
||
pre.src-octave:before { content: 'Octave'; }
|
||
pre.src-org:before { content: 'Org mode'; }
|
||
pre.src-oz:before { content: 'OZ'; }
|
||
pre.src-plantuml:before { content: 'Plantuml'; }
|
||
pre.src-processing:before { content: 'Processing.js'; }
|
||
pre.src-python:before { content: 'Python'; }
|
||
pre.src-R:before { content: 'R'; }
|
||
pre.src-ruby:before { content: 'Ruby'; }
|
||
pre.src-sass:before { content: 'Sass'; }
|
||
pre.src-scheme:before { content: 'Scheme'; }
|
||
pre.src-screen:before { content: 'Gnu Screen'; }
|
||
pre.src-sed:before { content: 'Sed'; }
|
||
pre.src-sh:before { content: 'shell'; }
|
||
pre.src-sql:before { content: 'SQL'; }
|
||
pre.src-sqlite:before { content: 'SQLite'; }
|
||
/* additional languages in org.el's org-babel-load-languages alist */
|
||
pre.src-forth:before { content: 'Forth'; }
|
||
pre.src-io:before { content: 'IO'; }
|
||
pre.src-J:before { content: 'J'; }
|
||
pre.src-makefile:before { content: 'Makefile'; }
|
||
pre.src-maxima:before { content: 'Maxima'; }
|
||
pre.src-perl:before { content: 'Perl'; }
|
||
pre.src-picolisp:before { content: 'Pico Lisp'; }
|
||
pre.src-scala:before { content: 'Scala'; }
|
||
pre.src-shell:before { content: 'Shell Script'; }
|
||
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
|
||
/* additional language identifiers per "defun org-babel-execute"
|
||
in ob-*.el */
|
||
pre.src-cpp:before { content: 'C++'; }
|
||
pre.src-abc:before { content: 'ABC'; }
|
||
pre.src-coq:before { content: 'Coq'; }
|
||
pre.src-groovy:before { content: 'Groovy'; }
|
||
/* additional language identifiers from org-babel-shell-names in
|
||
ob-shell.el: ob-shell is the only babel language using a lambda to put
|
||
the execution function name together. */
|
||
pre.src-bash:before { content: 'bash'; }
|
||
pre.src-csh:before { content: 'csh'; }
|
||
pre.src-ash:before { content: 'ash'; }
|
||
pre.src-dash:before { content: 'dash'; }
|
||
pre.src-ksh:before { content: 'ksh'; }
|
||
pre.src-mksh:before { content: 'mksh'; }
|
||
pre.src-posh:before { content: 'posh'; }
|
||
/* Additional Emacs modes also supported by the LaTeX listings package */
|
||
pre.src-ada:before { content: 'Ada'; }
|
||
pre.src-asm:before { content: 'Assembler'; }
|
||
pre.src-caml:before { content: 'Caml'; }
|
||
pre.src-delphi:before { content: 'Delphi'; }
|
||
pre.src-html:before { content: 'HTML'; }
|
||
pre.src-idl:before { content: 'IDL'; }
|
||
pre.src-mercury:before { content: 'Mercury'; }
|
||
pre.src-metapost:before { content: 'MetaPost'; }
|
||
pre.src-modula-2:before { content: 'Modula-2'; }
|
||
pre.src-pascal:before { content: 'Pascal'; }
|
||
pre.src-ps:before { content: 'PostScript'; }
|
||
pre.src-prolog:before { content: 'Prolog'; }
|
||
pre.src-simula:before { content: 'Simula'; }
|
||
pre.src-tcl:before { content: 'tcl'; }
|
||
pre.src-tex:before { content: 'TeX'; }
|
||
pre.src-plain-tex:before { content: 'Plain TeX'; }
|
||
pre.src-verilog:before { content: 'Verilog'; }
|
||
pre.src-vhdl:before { content: 'VHDL'; }
|
||
pre.src-xml:before { content: 'XML'; }
|
||
pre.src-nxml:before { content: 'XML'; }
|
||
/* add a generic configuration mode; LaTeX export needs an additional
|
||
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
|
||
pre.src-conf:before { content: 'Configuration File'; }
|
||
|
||
table { border-collapse:collapse; }
|
||
caption.t-above { caption-side: top; }
|
||
caption.t-bottom { caption-side: bottom; }
|
||
td, th { vertical-align:top; }
|
||
th.org-right { text-align: center; }
|
||
th.org-left { text-align: center; }
|
||
th.org-center { text-align: center; }
|
||
td.org-right { text-align: right; }
|
||
td.org-left { text-align: left; }
|
||
td.org-center { text-align: center; }
|
||
dt { font-weight: bold; }
|
||
.footpara { display: inline; }
|
||
.footdef { margin-bottom: 1em; }
|
||
.figure { padding: 1em; }
|
||
.figure p { text-align: center; }
|
||
.equation-container {
|
||
display: table;
|
||
text-align: center;
|
||
width: 100%;
|
||
}
|
||
.equation {
|
||
vertical-align: middle;
|
||
}
|
||
.equation-label {
|
||
display: table-cell;
|
||
text-align: right;
|
||
vertical-align: middle;
|
||
}
|
||
.inlinetask {
|
||
padding: 10px;
|
||
border: 2px solid gray;
|
||
margin: 10px;
|
||
background: #ffffcc;
|
||
}
|
||
#org-div-home-and-up
|
||
{ text-align: right; font-size: 70%; white-space: nowrap; }
|
||
textarea { overflow-x: auto; }
|
||
.linenr { font-size: smaller }
|
||
.code-highlighted { background-color: #ffff00; }
|
||
.org-info-js_info-navigation { border-style: none; }
|
||
#org-info-js_console-label
|
||
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
|
||
.org-info-js_search-highlight
|
||
{ background-color: #ffff00; color: #000000; font-weight: bold; }
|
||
.org-svg { }
|
||
</style>
|
||
|
||
<link rel="stylesheet" href="/assets/styles/style.css" />
|
||
<link rel="stylesheet" href="/assets/styles/bigger-picture.min.css" />
|
||
<link rel="stylesheet" href="/assets/styles/media.css" />
|
||
|
||
<script src="/assets/scripts/script.js" defer></script>
|
||
<script src="/assets/scripts/search.js" defer></script>
|
||
<script src="/assets/scripts/bigger-picture.min.js" defer></script>
|
||
<script src="/assets/scripts/svg-pan-zoom.min.js" defer></script>
|
||
<script src="/assets/scripts/gallery-init.js" defer></script>
|
||
</head>
|
||
<body>
|
||
<div id="preamble" class="status">
|
||
|
||
<div class="banner-header">
|
||
<div class="banner-left">
|
||
<a href="/20241210233721-brain_moc.html"> <img src="/assets/gr.png" alt="Site Logo" class="banner-logo" /> </a>
|
||
<div id="updated">Updated: 2025-12-28 Sun 19:48</div>
|
||
</div>
|
||
|
||
<div class="banner-search">
|
||
<input id="search-box"
|
||
type="search"
|
||
placeholder="Search notes…"
|
||
aria-label="Search notes"
|
||
autocomplete="off" />
|
||
<div id="search-results"></div>
|
||
</div>
|
||
|
||
<button id="close-all">Close All</button>
|
||
</div>
|
||
</div>
|
||
<div id="stack-root">
|
||
<div class="stack-track">
|
||
<article class="stack-pane pane-root" data-url="/20250121110241-afp_lec_1.html">
|
||
<div id="content" class="content">
|
||
<div class="title-section">
|
||
<div class="title-controls">
|
||
<button class="pane-fullscreen" aria-label="Fullscreen">F</button>
|
||
<button class="pane-edit" aria-label="Edit pane">E</button>
|
||
<button class="pane-close" aria-label="Close pane">×</button>
|
||
</div>
|
||
<h1 class="title">afp<sub>lec</sub><sub>1</sub></h1>
|
||
<div class="title-metadata">
|
||
<span class="metadata-item">
|
||
<span class="metadata-label">planted:</span>
|
||
<span class="metadata-value">2025-01-21</span>
|
||
</span>
|
||
<span class="metadata-item">
|
||
<span class="metadata-label">last tended to:</span>
|
||
<span class="metadata-value">2025-12-28</span>
|
||
</span>
|
||
</div>
|
||
</div>
|
||
<p>
|
||
<span class="timestamp-wrapper"><span class="timestamp"><2025-01-21 Tue> </span></span>
|
||
<a href="file:///home/zaine/master-folder/Uni/ADVFUNC/afp-learning-2024-2025/files/LectureNotes/files/introduction.lagda.md">Week 1 Handout</a>
|
||
</p>
|
||
<div id="outline-container-orgebf3ae1" class="outline-2">
|
||
<h2 id="orgebf3ae1"><a href="#orgebf3ae1">Week 1 lec 1</a></h2>
|
||
<div class="outline-text-2" id="text-orgebf3ae1">
|
||
<p>
|
||
if you want to put a hole in the file (ie the { }1 ) then put a ? and load the file
|
||
</p>
|
||
|
||
<p>
|
||
types are default called ’sets’ in agda but we will call them types.
|
||
</p>
|
||
|
||
<p>
|
||
data Bool : Type where
|
||
true false : Bool
|
||
</p>
|
||
|
||
<p>
|
||
Here we create a type called Bool
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
data Maybe (A : Type) : Type where
|
||
nothing : Maybe A
|
||
just : A → Maybe A
|
||
</p>
|
||
|
||
<p>
|
||
Given the type A we produce another type
|
||
Then we have two constructors, we can actually call them whatever we want, the only rule is that it shouldnt have spaces in the middle. For example, instead of nothing we can call ’nothing’ as ’Nothingljfsdsdj’.
|
||
</p>
|
||
|
||
<p>
|
||
The below is known as coercion or the disjoint union
|
||
Considering Blah = Either ℕ Bool
|
||
left 0: Blah
|
||
right false: Blah
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
data ℕ : Type where
|
||
zero : ℕ
|
||
suc : ℕ → ℕ
|
||
</p>
|
||
|
||
<p>
|
||
– 4 = suc (suc (suc (suc zero)))
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
data List (A : Type) : Type where
|
||
[] : List A
|
||
<span class="underline">::</span> : A → List A → List A
|
||
</p>
|
||
|
||
<p>
|
||
Below is a function that maps a type to a type:
|
||
myList : Type -> Type
|
||
myList = List
|
||
</p>
|
||
|
||
<p>
|
||
– N -> Type … this is called ’Dependant Type’ which depends on elements of another type.
|
||
When it comes to types, its often the case where the language we use doesnt exactly define the type we want it to. For example in haskell, the binary tree, when we want to use the binary search tree its a little difficult. In agda we can define a precise type; including the binary search tree. In summary agda can write precise types.
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
if<sub>then</sub><sub>else</sub>_ : {A : Type} → Bool → A → A → A
|
||
if true then x else y = x
|
||
if false then x else y = y
|
||
</p>
|
||
|
||
<p>
|
||
this above is known as mixfix operation, we use the _ to denote where the arguments of the function are going to be places
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
<span class="underline">+</span> : ℕ → ℕ → ℕ
|
||
zero + y = y
|
||
suc x + y = suc (x + y)
|
||
</p>
|
||
|
||
<p>
|
||
here we can pattern match on any of x or y
|
||
in haskell, recursion can be done and there arent restrictions on it. in Agda we have structural recursion as there is a termination on recursion. Structural recursion is when you follow the structure of the definition, for example in suc x + y, we get suc (x + y), we keep removing the x from suc until we are left with 0. scrcpy
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
</p>
|
||
|
||
<p>
|
||
<span class="underline">*</span> : ℕ → ℕ → ℕ
|
||
zero * y = zero
|
||
suc x * y = x * y + y
|
||
</p>
|
||
|
||
<p>
|
||
for suc x * y:
|
||
(1 + x) * y
|
||
y + x * y
|
||
</p>
|
||
|
||
<p>
|
||
in infixr, the r means the brackets are explicitly on the right, if we use infixl then its on the left:
|
||
x + y + z
|
||
x + (y + z) : r
|
||
(x + y) + z : l
|
||
</p>
|
||
|
||
<p>
|
||
– research implicit arguements.
|
||
</p>
|
||
|
||
|
||
<p>
|
||
reverse : {A : Type} → List A → List A
|
||
reverse [] = []
|
||
reverse (x :: xs) = reverse xs ++ [ x ]
|
||
</p>
|
||
|
||
<p>
|
||
although this program works, its inefficient.
|
||
</p>
|
||
|
||
<p>
|
||
rev-append : {A : Type} → List A → List A → List A
|
||
rev-append [] ys = ys
|
||
rev-append (x :: xs) ys = rev-append xs (x :: ys)
|
||
</p>
|
||
|
||
<p>
|
||
rev : {A : Type} → List A → List A
|
||
rev xs = rev-append xs []
|
||
</p>
|
||
|
||
<p>
|
||
the revappend is a helper function. you can see theres no ++ (concatenation) involved.
|
||
</p>
|
||
</div>
|
||
</div>
|
||
<div id="outline-container-org31acea8" class="outline-2">
|
||
<h2 id="org31acea8"><a href="#org31acea8">Week 1 lec 2</a></h2>
|
||
<div class="outline-text-2" id="text-org31acea8">
|
||
<p>
|
||
N-Induction : (P: N -> Type)
|
||
-> P 0
|
||
-> ((k:N) -> Pk (P (suc k))
|
||
choose k = 0
|
||
</p>
|
||
|
||
<p>
|
||
P0 : P0
|
||
f0 p1 : P1
|
||
f1 p2 : p2
|
||
</p>
|
||
|
||
<p>
|
||
-> (n:N) -> Pn
|
||
</p>
|
||
|
||
<p>
|
||
This is proof by induction,
|
||
</p>
|
||
|
||
<p>
|
||
ℕ-induction P p0 f 0 = P0
|
||
ℕ-induction P p0 f(suc n) = goal
|
||
where
|
||
ℍ : Pn
|
||
ℍ = ℕ-induction P p0 f n
|
||
</p>
|
||
|
||
<p>
|
||
ℕ-induction P p0 f 3 =
|
||
f3(f2(f1 p0))
|
||
essentially this is a for loop.
|
||
</p>
|
||
|
||
<p>
|
||
–
|
||
indstep : (k:N) -> k≣k -> suc k ≣ suc k
|
||
indstep k e = e
|
||
</p>
|
||
|
||
<p>
|
||
ℕ-refl n = ℕ-induction (λx -> x≣x) * (λke -> e)
|
||
</p>
|
||
|
||
<p>
|
||
introduction and elimination rules
|
||
</p>
|
||
|
||
|
||
<p>
|
||
–
|
||
List-induction : { x : Type }
|
||
-> (P : List X -> Type)
|
||
-> P []
|
||
-> ((x:X)(xs:List X) -> Pxs -> P(x::xs))
|
||
</p>
|
||
|
||
<p>
|
||
-> (xs : List X ) -> P xs
|
||
</p>
|
||
|
||
<p>
|
||
List-induction
|
||
</p>
|
||
</div>
|
||
</div>
|
||
<div id="outline-container-org225bc78" class="outline-2">
|
||
<h2 id="org225bc78"><a href="#org225bc78">Keybindings:</a></h2>
|
||
<div class="outline-text-2" id="text-org225bc78">
|
||
<ul class="org-ul">
|
||
<li>C-c C-l : to load the agda file</li>
|
||
<li>SPC-w for the windows</li>
|
||
<li>C-c C-c : case split (agda mode) (put x, or b or whatever the first one is, then use this - very useful).</li>
|
||
<li>C-c C-SPC: give: tries to fill the hole</li>
|
||
<li>C-shift - : undo</li>
|
||
<li>C-c C-r : refine</li>
|
||
<li>C-c C-, : show the context</li>
|
||
</ul>
|
||
|
||
<p class="backlinks-section" id="backlinks">
|
||
Backlinks
|
||
</p>
|
||
<ul class="org-ul backlinks-list">
|
||
<li><a href="20250120111047-afp_week1.html#ID-6c272430-aff5-468b-90d3-5ff3a96152cf">afp<sub>week1</sub></a></li>
|
||
</ul>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div></article></div></div>
|
||
<div id="postamble" class="status">
|
||
<footer>
|
||
<div class="copyright-container">
|
||
<div class="copyright">
|
||
Copyright © 2022-2025 Zaine Qayyum. All rights reserved unless otherwise noted.</div></div>
|
||
<div class="generated">
|
||
Created with <a href="https://www.gnu.org/software/emacs/">Emacs</a> 30.2 (<a href="https://orgmode.org">Org</a> mode 9.7.11) on <a href="https://www.archlinux.org/">Arch</a> <a href="https://www.gnu.org">GNU</a>/<a href="https://www.kernel.org/">Linux</a>
|
||
</div>
|
||
</footer>
|
||
</div>
|
||
</body>
|
||
</html>
|