banacorn

有哪些東西要安裝？

Windows 64-bit 一鍵安裝包：http://www.cs.uiowa.edu/~astump/agda/ （備用連結（比較快）） 本安裝檔包含 GHC 7.8、Agda 2.4 以及 Emacs

1. Haskell

• ghc 與 ghci ，GHC 提供的 Haskell 編譯器與交互式直譯器
• 建議版本為 **GHC 7.8 （較舊版本例如 **7.6 也可以接受，而更新的版本 prelude 所提供的函數型別會與教學使用的有些落差）

2. Agda

banacorn

let first p xs =
  let length = Array.length xs in
  (* mutable aray index *)
  let i = ref 0 in
  (* there are no loop breaks in OCaml anyway *)
  let break = ref false in
  while not (!break) && !i < length do 
    if p (xs.(!i)) then break := true else i := (!i) + 1
  done;
  !i 

banacorn

-- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!"

-- Chapter 1 - http://learnyouahaskell.com/introduction
-- Chapter 2 - http://learnyouahaskell.com/starting-out
-- Chapter 3 - http://learnyouahaskell.com/types-and-typeclasses
-- Chapter 4 - http://learnyouahaskell.com/syntax-in-functions
-- Chapter 5 - http://learnyouahaskell.com/recursion
-- Chapter 6 - http://learnyouahaskell.com/higher-order-functions

-- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise

banacorn

Intrinsically-typed de Bruijn representation of simply typed lambda calculus
============================================================================

\begin{code}
open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

banacorn

//
// Types
//
type t;

type eventName = string;
type listener('a) = 'a => unit;
type listener2('a, 'b) = ('a, 'b) => unit;
type listener3('a, 'b, 'c) = ('a, 'b, 'c) => unit;

banacorn

{-# OPTIONS --without-K #-}

module A where

infixl 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

J : (A : Set) (C : (x y : A) → x ≡ y → Set)
    → ((x : A) → C x x refl)

banacorn

Reducing expressions in CP

Background

CP is a process calculus presented by Philip Wadler in his paper "Propositions as sessions" (https://dl.acm.org/citation.cfm?id=2364568), as an attempt to bridge π-calculus with Linear logic.

Process calculus (like CP) provides a mean of modelling and describing the interactions and communications between a bunch of independent processes. The interaction between these processes are often described with some reduction rules.

banacorn

Goal: show that TSP is NP-complete

• TSP is NP
• TSP is NP-Hard

TSP is NP

• Algorithm: given a tour, sum the weights, and see if it exceeds the bound
• The verifier runs in polynomial time

banacorn

$ apm rebuild
Rebuilding modules ✗
gyp info it worked if it ends with ok
gyp verb cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node',
gyp verb cli   '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/.bin/node-gyp',
gyp verb cli   'rebuild' ]
gyp info using node-gyp@3.4.0
gyp info using node@8.9.3 | darwin | x64
gyp verb command rebuild []
gyp verb command clean []

banacorn

Build

stack build --stack-yaml stack-8.4.3.yaml

REPL

You may need to edit .ghci first: