Skip to content

Instantly share code, notes, and snippets.

@pema99
Created May 14, 2021 15:54
Show Gist options
  • Save pema99/d17ece0d58663765f1c46550f5a8a21a to your computer and use it in GitHub Desktop.
Save pema99/d17ece0d58663765f1c46550f5a8a21a to your computer and use it in GitHub Desktop.
Lambda calculus parsing and reduction - Using my own parsing combinator lib
module LambdaCalc
open Combinator
open Common
open Util
// Lambda calc AST
type Expr =
| Id of string
| Abs of string * Expr
| App of Expr * Expr
let rec prettyPrint expr =
match expr with
| Id id -> sprintf "%s" id
| Abs (id, e) -> sprintf "(\\%s. %s)" id (prettyPrint e)
| App (l, r) -> sprintf "%s %s" (prettyPrint l) (prettyPrint r)
// Parsing
let whitespace =
many (oneOf [' '; '\r'; '\n'; '\t']) *> just ()
let isAlpha c =
(c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
let isAlphaNumeric c =
isAlpha c || (c >= '0' && c <= '9')
let identP =
whitespace *>
(eatWhile1 isAlphaNumeric |>> List.toArray |>> System.String)
<* whitespace
let exprP, exprPImpl = declParser()
let varP =
identP |>> Id
let sigP =
whitespace *> (one '\\' *> identP <* one '.') <* whitespace
let absP =
(sigP <+> exprP) |>> Abs
let nonAppP =
between (one '(') exprP (one ')')
<|> absP
<|> varP
exprPImpl :=
whitespace *>
(chainL1 (whitespace *> nonAppP) (just (curry App)))
<* whitespace
// Reduction
let rec freeVars expr =
match expr with
| Id id -> [ id ]
| Abs (x, t) -> List.filter ((<>) x) (freeVars t)
| App (t, s) -> freeVars t @ freeVars s
let rec subst expr x r =
match expr with
| Id _ ->
if expr = x then r
else expr
| App (t, s) ->
App (subst t x r, subst s x r)
| Abs (id, t) ->
let stale = List.exists ((=) id) (freeVars r)
if Id id = x || stale then expr
else Abs (id, subst t x r)
let rec beta expr =
match expr with
| App (Abs (x, t), s) -> subst t (Id x) s
| App (t, s) -> App (beta t, beta s)
| Abs (x, t) -> Abs (x, beta t)
| a -> a
let rec reduce expr =
let redex = beta expr
if redex = expr then redex
else reduce redex
// CLI
while true do
printf "Input expression: "
let dataSrc = mkMultiLineParser (System.Console.ReadLine())
let result, state = exprP dataSrc
let expr =
match result with
| Success v -> v
| _ -> failwith (sprintf "Parsing failure. State: %A" state)
printfn "Reduced: %s" (prettyPrint (reduce expr))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment