jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.
https://jonsterling.github.io/agda-calf/
Apache License 2.0
55 stars 2 forks source link

Rename `step`? #37

Open HarrisonGrodin opened 1 year ago

HarrisonGrodin commented 1 year ago

Abstract cost metrics don't really correspond to a notion of "stepping". Would it make sense to rename step to reflect this abstraction? (RaML uses tick, but it suffers from the same issue.) Some ideas:

(To be read: "X c cost, then run e", for verb X = spend, pay, charge, incur, ...)

kaonn commented 1 year ago

I'm drawn to incur or charge since that's how I usually verbalize step.

HarrisonGrodin commented 1 year ago

I like those, too. Spend/pay seem to imply that the program already has some resource that it can get rid of, vs charge/incur seem to imply that as you run the program, you're accumulating some cost to be paid.

Instinct would be charge?