| #
f535214b |
|
14-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add theory presenting abstract view of computation states
Concretely these states are encoded λ-calculus terms, but we can present
the universal Phi function in terms of states with a nice API on them:
mk_initial_state : num -> num -> state
terminated : state -> bool
step1 : state -> state
comp_count : state -> num option
cs_to_num : state -> num
where comp_count is the number of steps needed to take a state to
termination, and cs_to_num extracts a result from a terminated state.
|