Created
December 10, 2021 11:30
-
-
Save jfdm/87660df789183663f3de381ef7cce5f2 to your computer and use it in GitHub Desktop.
Reduction Sequence for Foldr In Olaf
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| def xs : (List Nat) := | |
| (extend 1 | |
| (extend 2 | |
| empty[Nat])) | |
| def myAdd : (Nat -> (Nat -> Nat)) | |
| := (fun x : Nat, y : Nat => (add x y)) | |
| def rec foldr : ((Nat -> (Nat -> Nat)) -> (Nat -> ((List Nat) -> Nat))) | |
| := (fun f : (Nat -> (Nat -> Nat)), acc : Nat, xs : (List Nat) | |
| => match xs as | |
| { empty => acc | |
| | extend y ys => (apply (apply f y) (apply (apply (apply foldr f) acc) ys)) | |
| }) | |
| main := (apply (apply (apply foldr myAdd) 0) xs) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| $ ./build/exec/olaf examples/example3.olaf | |
| -- LOG : Parsed | |
| -- LOG : Checked | |
| -- LOG : Running | |
| (let (extend 1 (extend 2 empty)) in { (let (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) in { (let (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) in { (apply (apply (apply (var Here) (var (T Here)) ) 0 ) (var (T (T Here))) )})})}) | |
| = Reduce Let Binding | |
| (let (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) in { (let (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) in { (apply (apply (apply (var Here) (var (T Here)) ) 0 ) (extend 1 (extend 2 empty)) )})}) | |
| = Reduce Let Binding | |
| (let (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) in { (apply (apply (apply (var Here) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 1 (extend 2 empty)) )}) | |
| = Reduce Let Binding | |
| (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 1 (extend 2 empty)) ) | |
| = Simplify Application Function | |
| (apply (apply (apply (\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})}) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 1 (extend 2 empty)) ) | |
| = Simplify Application Function | |
| (apply (apply (\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) (var (T (T (T Here)))) ) (var Here) ) )})})}) 0 ) (extend 1 (extend 2 empty)) ) | |
| = Simplify Application Function | |
| (apply (\(List Nat) -> {(match (var Here) { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )})}) (extend 1 (extend 2 empty)) ) | |
| = Reduce Application | |
| (match (extend 1 (extend 2 empty)) { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )}) | |
| = Reduce Match List Cons | |
| (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) 1 ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 2 empty) ) ) | |
| = Simplify Application Function | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 2 empty) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (apply (apply (\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})}) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (extend 2 empty) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (apply (\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) (var (T (T (T Here)))) ) (var Here) ) )})})}) 0 ) (extend 2 empty) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\(List Nat) -> {(match (var Here) { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )})}) (extend 2 empty) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (match (extend 2 empty) { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )}) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) 2 ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) empty ) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) empty ) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) (apply (apply (apply (\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})}) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) empty ) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) (apply (apply (\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) (var (T (T (T Here)))) ) (var Here) ) )})})}) 0 ) empty ) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) (apply (\(List Nat) -> {(match (var Here) { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )})}) empty ) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) (match empty { 0 | (apply (apply (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) (var (T Here)) ) (apply (apply (apply (rec(\(Nat->(Nat->Nat)) -> {(\Nat -> {(\(List Nat) -> {(match (var Here) { (var (T Here)) | (apply (apply (var (T (T (T (T Here))))) (var (T Here)) ) (apply (apply (apply (var (T (T (T (T (T Here)))))) (var (T (T (T (T Here))))) ) (var (T (T (T Here)))) ) (var Here) ) )})})})})) (\Nat -> {(\Nat -> {(add (var (T Here)) (var Here))})}) ) 0 ) (var Here) ) )}) ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (apply (\Nat -> {(add 2 (var Here))}) 0 ) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) (add 2 0) ) | |
| = Simplify Application Variable | |
| (apply (\Nat -> {(add 1 (var Here))}) 2 ) | |
| = Reduce Application | |
| (add 1 2) | |
| = Reduce Binary Operation | |
| 3 | |
| -- LOG : Finished |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment