a Lambda Calculus to Lazy K translator

Run the translator with

swipl lambda_to_lazyk.swi

and give a lambda expresssion to the compile pred.

?- compile(x -> y -> y @ x).
S(K(S(I)))(K)

• fundamental syntax

  ->

  abstraction (right associative)

  @

  application (left associative)

• syntax sugars

  lists

  [x, y, ...] = cons @ x @ (cons @ y @ ... nil)

  numbers

  4 = succ @ (succ @ (succ @ (succ @ zero)))

  strings

  ​"abc"​ = [97, 98, 99]

• data representation

  boolean

  true/0, false/0

  number

  zero/0, succ/1

  list

  nil/0, cons/2

• predicates

  unary

  zerop/1, nullp/1

  binary

  ge/2, gt/2, eq/2, neq/2, le/2, lt/2

• operations

  arithmetic

  add/2, sub/2, mult/2, exp/2, mod/2, div/2

  boolean

  not/1, and/2, or/2, xor/2

  list

  car/1, cdr/1, nthcdr/2, nth/2, map/2, append/2, reverse/1

• others

  control

  if/3,

  higher order

  fix/1, compose/2

  utils

  int_to_str/1

Define macros with define pred

?- define(twice, f -> x -> f @ (f @ x)).
true.

so that you can use the definition in the expressions.

?- compile(twice @ (x -> x) @ (x -> y -> y @ x)).
S(S(K(S))(K))(I)(I)(S(K(S(I)))(K))

?- compile(x -> reverse @ "!dlroW ,olleH").

?- define(thirty_seven, succ @ (exp @ (mult @ 2 @ 3) @ 2)). % equals to 37 but optimized in code size
?- define(limit, mult @ thirty_seven @ ((x -> x @ x) @ 3)). % equals to 999
?- define(solve_1, x -> if @ (zerop @ (mult @ (mod @ x @ 3) @ (mod @ x @ 5))) @ x @ 0).
?- define(solve, fix @ (f -> x -> if @ (zerop @ x) @ 0 @ (add @ (solve_1 @ x) @ (f @ (pred @ x))))).
?- compile(x -> int_to_str @ (solve @ limit)).