jameshfisher

Having read a few proofs that the halting problem is undecidable, I found that they were quite inaccessible, or that they glossed over important details. To counter this, I've attempted to re-hash the proof using a familiar language, JavaScript, with numerous examples along the way.

This famous proof tells us that there is no general method to determine whether a program will finish running. To illustrate this, we can consider programs as JavaScript function calls, and ask whether it is possible to write a JavaScript function which will tell us

startling

-- | Some functions on directed graphs.
module Language.Coatl.Graph where
-- base
import Data.Maybe
-- containers
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
-- mtl

washort

Parsley Tutorial

From Regular Expressions To Grammars

Parsley is a pattern matching and parsing tool for Python programmers.

gnuvince

type nat = Zero | Succ of nat

let rec int_of_nat x =
  match x with
    | Zero -> 0
    | Succ x' -> 1 + int_of_nat x'

let rec nat_of_int x =
  match x with
    | 0 -> Zero

devyn

import Prelude hiding (toInteger)
import Data.List

data Value = StringValue  String
           | IntegerValue Integer
           | NameValue    String
           | FuncValue    [String] AST
           | NilValue
           deriving Show

DanielCollins

(define (unify a b)
  (cond ((and (pair? a)
              (pair? b)) (cons (unify (car a) (car b))
                               (unify (cdr a) (cdr b))))

        ((symbol? a) b) ; here i just return b, because a symbol matches anything. a more complex system would have a third argument
                        ; , the environment, that tracks existing bindings for a, and prevents conflicts. then, instead of returning b
                        ; we could update the environment with the binding for a = b, or issue a failure (in kanren language, #u)

        ((eq? a b) b)   ; a and b trivially unify without updating any bindings. here I just return their mutual value