The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

I guess I was wondering if anyone had considered performance implications (is it
more efficient to substitute than to use let as a kind of explicit
substitution?) or philosophical perspectives (is it better to use let as a
object-level representation of substitution than to treat substitution as a
meta-level operation?).

Just recently I wrote a few words on different ways of representation:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html

The bottom line is that philosophical and other representations (e.g., logical frameworks,

or for the purpose of automation) have conflicting design principles, but are related to each other.

The philosophical approach (bottom-up representation) aims at finding very general

principles/rules (e.g., Andrews' Q0), even at the cost of efficiency.

The top-down representation makes metatheorems symbolically representable,

and provability relations explicit (within the formal language).

For example, Q0 is a Hilbert-style system, in which metatheorems are inexpressible

and which is not suited for automation.

(Somebody argued in this context that Metamath is Hilbert-style, which I find problematic,

as Metamath's formal language is that of a logical framework, starting already at the meta-level

with much more powerful expressiveness. The point of Q0 as a Hilbert-style system

–  at the object language level! – is that Andrews can reduce all rules to a single one

(substitution: Rule R), obtaining all of mathematics with very little means.

With the very strong expressiveness of the meta-level this is much easier,

although less elegant.)

In my chart at

http://www.owlofminerva.net/files/fom.pdf

the conflicting design principles are reflected by the two different branches emerging from

Church's Simple Theory of Types:

1. Andrews' Q0 (focusing on expressiveness), and

2. Gordon's HOL (focusing on automation).

In the text linked above I argue that the top-down representations obtain their legitimacy

through the bottom-up (philosophical) representation.

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Am 26.05.2018 um 19:44 schrieb William J. Bowman <wjb AT williamjbowman.com>:

I agree that the additional judgment in ΠΣ appears at least as complicated as
substitution.
The definition of "Oleg" in McBride's thesis (chapter 2.1, page 20) is a better
comparison to CIC, I think, and *seems to me* somewhat simpler for omitting
substitution.

I guess I was wondering if anyone had considered performance implications (is it
more efficient to substitute than to use let as a kind of explicit
substitution?) or philosophical perspectives (is it better to use let as a
object-level representation of substitution than to treat substitution as a
meta-level operation?).

–
William J. Bowman

On Sat, May 26, 2018 at 06:14:36PM +0200, Matthieu Sozeau wrote:

Right, it's possible to phrase it like this. I understand ΠΣ's motivation
for turning these x := v into equalities x = v for reflection/conversion
but I'm not wondering how an intensional type theory like CIC would benefit
from this. The additional complication in the reduction rules looks
equivalent to me to the definition of substitution.
Note that the delta/let reduction rule of CIC is performing immediate
substitution.
-- Matthieu

On Sat, May 26, 2018 at 5:19 PM William J. Bowman <wjb AT williamjbowman.com>
wrote:

Matthieu,

Yes that should be one of the closure rules.
I suppose this means let is head normal when its body has no more
reductions;
alternatively, we could have:

x := v |- B -> B’
-------------------  (when x ∉ FreeVars(B'))
let x = v in B -> B’

McBride's thesis has a reduction rule like this, and the ΠΣ calculus
Thorsten
mentioned does something similar via an auxiliary relation that normalizes
let
bindings.

--
William J. Bowman

On Fri, May 25, 2018 at 10:44:55AM +0200, Matthieu Sozeau wrote:

Hi,

 What is the reduction rule for let, e.g. for weak head reduction?
If you assume reduction under a local context of definitions, then you

get

something like:

x := v |- B -> B’
-------------------
Let x = v in B -> let x = v in B’

B' might still contain references to x, so you will need to consider

let's

as head normal somehow, no?
— Matthieu

Le jeu. 24 mai 2018 à 19:31, William J. Bowman <wjb AT williamjbowman.com>

a

écrit :

McBride and McKinna observe that when you have let and δ reduction,
including substitution is unnecesary.
(The View From The Left, https://dl.acm.org/citation.cfm?id=967496)
Instead, we can replace dependent typing rules such as:

 ...
 ------------------
 Γ ⊢ e₁ e₂ : B[e₂/x]

By

 ...
 ------------------
 Γ ⊢ e₁ e₂ : let x = e₂ in B

And replace substitution in reduction, such as β, by:

 Γ ⊢ (λ x.e) v → let x = v in e

Why does CIC include both let + δ reduction *and* substitution?

--
William J. Bowman
Northeastern University
College of Computer and Information Science