dvanhorn

$ mono fstar.exe 
Missing method get_argv in assembly /Users/dvanhorn/Documents/play/fstar/fstar-0.5-alpha/bin/basic.dll, type Microsoft.FSharp.Compatibility.OCaml.SysModule
Unexpected exception :( 
System.IO.FileNotFoundException: Could not load file or assembly 'FSharp.PowerPack.Compatibility, Version=2.0.0.0, Culture=neutral, PublicKeyToken=a19089b1c74d0809' or one of its dependencies.
File name: 'FSharp.PowerPack.Compatibility, Version=2.0.0.0, Culture=neutral, PublicKeyToken=a19089b1c74d0809'
  at Microsoft.FStar.FStar.process_args () [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.do_main[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 Missing method flush in assembly /Users/dvanhorn/Documents/play/fstar/fstar-0.5-alpha/bin/fstar.exe, type Microsoft.FSharp.Compatibility.OCaml.PervasivesModule

Unhandled Exception: System.IO.FileNotFoundException: Could not load file or assembly 'FSharp.PowerPack.Compatibility, Version=2.0.0.0, Culture=neutral, PublicKeyToken=a190

dvanhorn

#lang racket

;; 0CFA in the AAM style on some hairy Church numeral churning

;; + compilation phase
;; + lazy non-determinism
;; + specialized step & iterator 0m34.248s vs 0m16.339s
;; + compute store ∆s 0m16.339s vs 0m1.065s (!!!)

;; An Exp is one of:

dvanhorn

#lang racket

;; 0CFA in the AAM style on some hairy Church numeral churning

;; + compilation phase
;; + lazy non-determinism
;; + specialized step & iterator 0m34.248s vs 0m16.339s

;; An Exp is one of:
;; (var Lab Exp)

dvanhorn

#lang racket

;; 0CFA in the AAM style, but with a compilation phase, on
;; some hairy Church numeral churning

;; Moral: a simple compilation strategy can eliminate a lot 
;; of analysis-time interpretive overhead.  (40sec vs 9sec)
 
;; appl : (∀ (X) ((X -> (Setof X)) -> ((Setof X) -> (Setof X))))
(define ((appl f) s)

dvanhorn

#lang racket
(provide compile parse)
(require (for-template (except-in racket exp do compile))
         (for-template "runtime.rkt"))

;; 0CFA in the AAM style, but with a compilation phase that
;; occurs at Racket compile time, on some hairy Church 
;; numeral churning

;; Moral: Doesn't seem to buy you much over a runtime compile

dvanhorn

#lang racket

;; 0CFA in the AAM style, but with a compilation phase, on
;; some hairy Church numeral churning

;; Moral: a simple compilation strategy can eliminate a lot 
;; of analysis-time interpretive overhead.  (40sec vs 9sec)

;; (X -> Set X) -> (Set X) -> (Set X)
(define ((appl f) s)

dvanhorn

#lang racket

;; 0CFA in the AAM style on some hairy Church numeral churning
;; using lazy non-determinism (wait until your in demand before
;; forking).

;; Improvement over eager non-determism: 45s vs 32.

;; (X -> Set X) -> (Set X) -> (Set X)
(define ((appl f) s)

dvanhorn

#lang racket

;; 0CFA in the AAM style on some hairy Church numeral churning

;; Moral: per machine-state store polyvariance is not viable,
;; but with widening it's not so bad.

;; (X -> Set X) -> (Set X) -> (Set X)
(define ((appl f) s)
  (for/fold ([i (set)])

dvanhorn

module Ch1 where

-- My (DVH) solutions the Vectors and Finite Sets chapter of
-- Dependently Typed Programming: an Agda introduction, Feb 21, 2011
-- edition, by Conor McBride.

-- I'm sure there are plenty of improvements to be made, so comments
-- are very welcome.  Please send to dvanhorn at ccs dot neu dot edu.

-- Thanks,

dvanhorn

Memoization is fundamentally a top-down computation and dynamic
programming is fundamentally bottom-up.  In memoization, we observe
that a computational *tree* can actually be represented as a
computational *DAG* (the single most underrated data structure in
computer science); we then use a black-box to turn the tree into a
DAG.  But it allows the top-down description of the problem to remain
unchanged.

In dynamic programming, we make the same observation, but construct
the DAG from the bottom-up.  That means we have to rewrite the