Are the Image rules sound? [Question]
Closed this issue · 2 comments
@vrahli I was recalling the way that these were originally formulated in MetaPRL, and I remembered that for Img(A; f), they had a constraint that f not have any free variables. Details here: http://www.cin.ufpe.br/~wollic/wollic2006/nogin-kopylov-slides.pdf
Do you know why it is safe to omit this constraint in Nuprl and JonPRL?
We still have a constraint that f is in Base.
Therefore, if f has a free variable x : A, then for all a and b in A,
f[x\a] has to be computationally equivalent to f[x\b].
On Thu, Aug 27, 2015 at 4:19 PM, Jonathan Sterling <notifications@github.com
wrote:
@vrahli https://github.com/vrahli I was recalling the way that these
were originally formulated in MetaPRL, and I remembered that for Img(A; f),
they had a constraint that f not have any free variables. Details here:
http://www.cin.ufpe.br/~wollic/wollic2006/nogin-kopylov-slides.pdfDo you know why it is safe to omit this constraint in Nuprl and JonPRL?
—
Reply to this email directly or view it on GitHub
#219.
@vrahli Ah, perfect, thank you! What a much more elegant way of doing it.