Yuchao Lyu

Zhumo Yu

Ye Yang

Yuxiang Liu

Xinxin Zhao

Xinmei Liu

Svetlana Mintova

Zifeng Yan

Guofeng Zhao

Metal and acid sites instantaneously prepared over Ni/SAPO-11bifunctional catalyst

Keywords: Nickel, SAPO-11, Synthesis, Bifunctional catalyst, Hydroisomerization

The Ni/SAPO-11 bifunctional catalyst for hydroisomerization of n-hexane was prepared via a novel synthesis method. It involved grinding of nickel source with amorphous precursors used for SAPO-11 followed by crystallization at 473 K for 24 h, thus avoiding the use of extra solvents in the synthesis. The highly dispersed nickel species and acid sites in the Ni/SAPO-11 bifunctional catalyst were instantaneouslyformed. The Ni/SAPO-11 catalyst contains framework nickel, nickel monoxide (NiO) and nickel aluminate spinel. The nickel monoxide with a size of 2-4 nm provides (de)hydrogenation function after reduction, while the framework nickel supplies more acid sites leading to an enhancedisomerization activity.

The Ni/SAPO-11 catalyst shows a great synergeticeffect between the metallic nickel and acid sites with a high metal-to-acid sites ratio (C Ni /C A ) and close proximity. A single metallic nickel site is able to balance ca. 5 acid sites (C Ni /C A ≈0.19) over the Ni/SAPO-11 catalyst in n-hexane hydroisomerization.The high dispersion of nickel over the catalyst provides relatively excessive metal sites (C Ni /C A >0.19), leaving the rate limiting reaction to occur on the acid sites. The Ni/SAPO-11 catalyst exhibits comparable n-hexane conversion (71.2%) and iso-hexane yield (66.7%) to the classical Pt/SAPO-11 catalyst.With enhancing acidity, the Ni/SAPO-11 catalyst exhibits one of the highest iso-hexane yields reported in the n-hexane hydroisomerization, which render the new material as a promising candidate for the hydroisomerization catalysts.

Introduction

Hydroisomerization of light n-alkanes is an important catalytic process to obtain clean gasoline with high octane number [1][2][3]. Increasing proportion of the isomerized gasoline in the gasoline pool contributes to the products upgrading and environmental protection [2,4,5].The current catalysts used in the hydroisomerization process are bifunctional, namely containing acid sites for skeletal isomerization and metal sites for (de)hydrogenation [6,7].Noble metals (platinum, palladium) are widely used in the bifunctional catalysts [2,[8][9][10], butsuffer fromlimited availability and high costs. The widely used Pt-promoted chlorinated alumina catalysts cause serious corrosion problems and environmental pollution due to the need of continuous chlorine addition [11]. Therefore, the development of non-noble metal (nickel) based hydroisomerization catalysts is an appealing task. Several attempts have been made to prepare non-noble metal catalysts, and it has been shown that large metal particles are formed caused by a severe sintering which is unavoidable especially at high metal loading [12,13]. This problem restricts the optimization of the existing non-noble catalysts.

Therefore, it is vital to look for a novel strategy for preparation of the non-noble metalswith reducedparticle sizesfor hydroisomerization catalysts.

In order to reduce the particle size of metal species in catalysts, strengthening of the interactions between the metal species and support to inhibit the metals aggregation is of critical importance [14,15]. Using the impregnation method with solvents with weak polarities is an effective way to achieve this goal [16][17][18][19]. In the previous work [13], ethanol was used as solvent to support nickel on SAPO-11 and to produce Ni/SAPO-11 catalyst.The particle size of nickel monoxide (20 nm) was much smaller than that over the catalyst prepared with water as solvent (50 nm). Compared with the conventional impregnation method, a stronger metal-support interaction can be obtained through equilibrium adsorption method. The metal species were deposited through adsorption and reaction with receptor sites developed on thesupport [20]. Goula et al. [21] prepared Ni/Al 2 O 3 by equilibrium adsorption method for the biogas dry reforming reaction. They found that a smaller metal particle size of 8 nm was obtained through this method compared with metal particles of 13 nm of the catalysts prepared by the impregnation method;the former catalystshowed enhanced catalytic performance. Controllable absorption method could also be used to strengthen the metal-support interaction in Ni/Al 2 O 3 catalysts. Optimal absorption conditionswere identified using point of zero charge, pH precipitation and adsorption experiments [22]. The Ni/Al 2 O 3 catalyst prepared under such conditions presented a stronger metal-support interaction and higher metal dispersion than the catalyst prepared by impregnation.Many other trialsincluding introduction of additives [23][24][25] or changing metal precursors [10,26,27] to inhibit the aggregation of metal species have been performed. However, most of these methods lead to more complex synthesis procedures, violating the green synthesis of the catalyst. Besides, the main focus is on metal dispersion without paying due attention to acidity. Even more the acid sites on supports during the impregnation or adsorption of metal precursor are modified.This is not a favorable situation for bifunctional catalysts whose performance depends not only on the metal sites, but also on the acidity and metal-acid balance.

In the present work, direct synthesis method was used forinstantaneouslysynthesis of highly-dispersed nickel species and acid sites over the Ni/SAPO-11 hydroisomerization catalyst. The synthesis method involved initial grinding of SAPO-11 precursorswith nickel source without extra solvents followed by crystallization. This method leads to significant reduction of waste and solvent use as well as the synthesis procedure is shortened significantly. It differs from the solvent-free methodthat requires pre-reaction of the raw materials and washing of intermediates with ethanol [28,29]. The features of metal andacid sites over the Ni/SAPO-11 catalyst were investigated systematically. The catalytic performance was assessed by hydroisomerization of n-hexane, and active site for (de)hydrogenation reaction was disclosed. The metal-acid balance and reaction pathway were also discussed.

Experimental

Materials

Pseudo-boehmite (70.0 wt.% Al 2 O 3 ) was purchased from Yantai Henghui Petrochemical Co., Ltd. Phosphoric acid (85.0wt.% H 3 PO 4 ) was purchased from XiRong Petrochemical Co., Ltd. Di-propylamine (DPA, ≥99.0 wt.% C 6 H 15 N) and Nickel (II) nitrate hexahydrate (Ni(NO 3 ) 2 • 6H 2 O) were purchased from Sinopharm Chemical Reagent Co., Ltd. Silica sol (30.0 wt.% SiO 2 ) was purchased from Qingdao Haiyang Petrochemical Co., Ltd.All chemicals were used without purification.

Sample synthesis

Direct synthesis of Ni/SAPO-11(s) was carried out using a mixture with the following molar ratio: 1.0 P 2 O 5 : 1.9 DPA: 0.4 SiO 2 : 0.19Ni(NO 3 ) 2 • 6H 2 O:1.0 Al 2 O 3 . In a typical run, 4.38 g of pseudo-boehmite, 6.92 gof H 3 PO 4 , 5.76 g DPA, 2.4 g of silica sol and 1.65 g of Ni(NO 3 ) 2 •6 H 2 O were mixed in a mortar. After grinding for 10 min, the mixture was transformed to an autoclave and heated at 473 Kfor 24 h. The solid product was washed with deionized water, dried at 373 K for 12 h and calcined at 773 K in a muffle oven for 6 h.

Varying the amount of nickel addition, catalysts with different nickel loading were prepared.When H-Beta zeolite was added into the initial synthesis gel of the Ni/SAPO-11(s), the final product was abbreviated as Ni/SAPO-11-β(s). The mass ratio of H-Beta relative to the alumina source used for the SAPO-11 (pseudo-boehmite) was 0.1. As a reference, SAPO-11(s) without nickel was also prepared by the same procedure.

For comparison, two samples via incipient impregnation method abbreviated as Ni/SAPO-11(im) and Pt/SAPO-11(im) were prepared as follow: SAPO-11 was immersed in aqueous solutions of Ni(NO 3 ) 2 • 6H 2 O or H 2 PtCl 6 . After the impregnation, the material was dried at 383 K for 2 h and then calcined in air at 673 K for 4 h. The loading of nickel in the Ni/SAPO-11(im) sample was 4.0 wt.% that was the same as for the Ni/SAPO-11(s) sample; the loading of Pt was 0.3 wt.%. The SAPO-11 used for the impregnation was synthesized according to the procedure reported before [13].

Characterization

X-ray diffraction (XRD) patterns of samples were collected with X' Pert PRO MPD diffractometer (PANalytical B.V. Netherlands) with Cu Kα radiation (λ = 0.15418 nm) operated at 40 kV and 40 mA. Transmission electron microscopy (TEM) and elemental mapping of nickel were performed using a FEI Titan G2 80-200 TEM/STEM. The elemental mapping was obtained by energy dispersive X-ray spectroscopy using the super-X detector.

X-ray photoelectron spectroscopy (XPS) was carried out using a PHI 500 spectrometer with Al Kα radiation. The binding energywas calibrated by measuring the C1s peak at 284.8 eV.

Practical metal loading and chemical compositions of the samples were measured by X-ray fluorescence (XRF, ZSX-100e using Rh and Au excitation tubes). X-ray absorption fine structure (XAFS) spectra were obtained at the 1W1B station in the BSRF (Beijing Synchrotron Radiation Facility, People's Republic of China) operated at 2.5 GeV with a maximum current of 250 mA. X-ray absorption spectroscopy (XAS) measurements at the Ni K-edge were performed in fluorescence mode using a Lytle detector. All samples were pelletized as disks of 13 mm diameter with 1 mm thickness using graphite powder as a binder.Temperature programmed reduction of hydrogen (H 2 -TPR) and temperature programmed desorption of ammonia (NH 3 -TPD) were carried out on a dynamic chemisorption analyzer (Micromeritics AutoChem 2920). The IR spectra of catalysts were recorded by a Nicolet-6700 FTIR spectrometer. The acidity of the catalysts was evaluated using pyridine as a probe molecule followed by FTIR. All samples were evacuated at 573 K for 3 h, followed by adsorption of pyridine at room temperature and desorption of pyridine in a vacuum at 423 K. Finally the spectra were recorded at room temperature.H 2 chemisorption measurements were carried out on a Micromeritics AutoChem 2920; the accessible metal sites (C Ni ) of the catalysts after reduction were studied. Prior to the chemisorption at ambient temperature, the samples were pretreated in hydrogen atmosphere at 823 K for 2 h and purged at this temperature in an argon flow for 2 h to avoid the presence of residual absorbed hydrogen. The ratio (C Ni /C A ) of metal sites (C Ni ) relative to the acid sites (C A ) was calculated according to the method disclosed before [30][31][32]. Ultraviolet-visible (UV-vis) diffuse reflectance spectra were recorded on a UV-2600 UV-vis spectrophotometer using BaSO 4 as a reference. The turnover frequency (TOF) per acid site, labeled as TOF n-C6 , was calculated using the following equation:

TOF n-C6 = Rate of converted n-hexane (molg cat -1 h -1 )
Number of acid sites (molg cat -1 )

Catalytic Tests

The hydroisomerization of n-hexane (n-C 6 ) was selected as a model reaction to assess the catalytic performance of the catalysts. The catalytic tests were carried out at a pressure of 2.0 MPa, a weight hourly space velocity (WHSV) of 1.0 h -1 , and a H 2 /n-C 6 molar ratio of 4.0.

Prior to the reaction, the catalyst was reduced in situ under a hydrogen flow at 823 K for 2 h and then cooled to reaction temperature. The reaction products were analyzed on-line by a gas chromatograph (Agilent 7820) equipped with a flame ionization detector.The n-hexane conversion might be increased due to the thermal behavior of the reaction at high temperature.

The thermal reaction of the current feed was carried out at the highest temperature (653 K) in the present work. The n-hexane conversion was less than 1.0 %, indicating that in all cases investigated, thermal reaction did not bias the hydroisomerization results. with the SAPO-11(s), which implies a small difference in grain size between the two samples.

Results and discussion

Crystalline phases

Thus, the increased crystallinity of the Ni/SAPO-11(s) might be due to the effective structure directing effect of amine complex of nickel formed by nickel and di-propylamine in the synthesis gel of Ni/SAPO-11(s). Similar phenomenon was observed in the synthesis of aluminophosphates molecular sieves with nickel or cobalt complex of diethylenetriamine as a structure directing agent [35,36].In this case, part of nickel ultimately resided in tetrahedral sites in the framework of SAPO-11 [36], which is confirmed by the slight shifting of the diffraction peak to a lower angle for the Ni/SAPO-11(s) (0.03 degree) compared with the SAPO-11(s) (Fig. 1(b)). The substitution of smaller tetrahedrally coordinated skeletal atoms (Al 0.51 Å or P 0.38 Å in crystal form) with heteroatoms of nickel that has a larger size (0.69 Å) as ions in crystalline environment, yields an increased lattice parameter value [37].

State of nickel Species

UV-vis diffuse reflectance spectra of the calcined catalysts are shown in Fig. 2; the spectrum of pure NiO is added as a reference.The UV-vis spectra of the Ni/SAPO-11(im) catalyst andthe bulk NiO are very similar in bands positions, consisting of absorption bands at 280, 380, 420, 640 and 720 nm.This implies thatthe nickel in the Ni/SAPO-11(im) exists as NiO [38]. For the Ni/SAPO-11(s), apart from the absorption bands assigned to the NiO, the new one at 257 nm is attributed to the electron transfer from O 2-(2p) to tetrahedral Ni 2+ (3d) in framework of the SAPO-11 [39][40][41]; the peak at 400 nm (Fig. 2 (b)) is assigned to the octahedrally coordinated nickel species in nickel aluminate spinel [42,43]. with the XPS spectrum of bulk NiO reported in literature [44]. However, the electronic structure is more complex. The two peaks at 853.8 and 855.4 eV in the Ni 2p 3/2 region after deconvolution can be explained in terms of a simplified model of final state effects in which photoemission is potentially accompanied by rearrangement of electrons in the valence band [45]. They shifted to higher binding energy (854. [48]. The small peaks at 859.0 (Ni 2p 3/2 ) and 876.9 eV (Ni 2p 1/2 ) can be assigned to tetrahedral Ni 2+ in the framework of SAPO-11 [46], which is also supportedby the UV-vis results. Additionally,the elemental maps of nickel (Fig. 6(f)) also show that nickel species aggregated in some regions, showing an uneven distribution on the surface of the Ni/SAPO-11(im). The catalyst prepared by the direct method presents a uniform distribution of nickel (Fig. 6(c)).

The higher dispersion of nickel species could be ascribed to the spatial effect of the raw material used for the preparation of the SAPO-11 support. All the raw materials including the nickel source (nickel nitrate) were mixed with the precursor of SAPO-11 before the crystallization was performed in order to inhibit the contact between the nickel species. The Ni/SAPO-11(s) and SAPO-11(s) exhibit similar compositions in terms of Si, P and Al (Table S2). The increased Brønsted acid sites over the Ni/SAPO-11(s) catalyst are mainly contributed by the incorporation of divalent nickel ions into the SAPO-11 framework that introduces more negative charges, thus generating more Brønsted acid sites.The Ni 2+ was most likely to substitute for Al 3+ to form bridged NiP-OH structures in the Ni/SAPO-11(s) sample [58]. Similar phenomenon was observed in the metal-substituted AlPO 4 molecular sieves [59]. The Brønsted acid sites from bridged MeP-OH (Me 2+ ) in the MeAPO-11 sample are proposed to be strong [59]and this will be confirmed by the NH 3 -TPD (see Fig. S3). The acid distribution of all catalysts is summarized in Table S3.

Metal sites for (de)hydrogenation reaction

Three types of nickel species in the Ni/SAPO-11(s) catalyst are identified as described above. Given that only NiO could be reduced into metallic nickel during the reduction step and nickel aluminate spinel is inactive in n-hexane hydroisomerization, the reactions were carried out over SAPO-11(s), unreduced and reduced Ni/SAPO-11(s) samples at 593 K (Fig. 9). Compared with the SAPO-11(s), there is only a slight increase in the n-hexane conversion and iso-hexane (i-C 6 ) yield over the unreduced catalyst. This increase is attributed to the contribution of weak (de)hydrogenation function of NiO and enhanced isomerization function by framework nickel species. In contrast, the n-C 6 conversion and i-C 6 yield over reducedNi/SAPO-11(s) catalyst are much higher than that over the unreduced Ni/SAPO-11(s).

This indicates that the active sites for (de)hydrogenation are provided predominantly by metallic nickel rather than by the framework nickel species.

Catalytic test

The results from the catalytictests of samples Ni/SAPO-11(s) and Ni/SAPO-11(im) are shown in Fig. 10; the Pt/SAPO-11(im) sample is used only for comparison (reference sample).

The Ni/SAPO-11(s) shows much higher n-hexaneconversion than the Ni/SAPO-11(im) in the whole reaction temperature range (Fig. 10 (a)). Compared with the reference Pt/SAPO-11(im), the Ni/SAPO-11(s) shows aslightly lower n-hexane conversion at temperature below 613 K.

As the temperature increased, they exhibit almost the same n-hexane conversion, suggesting the high activity of the Ni/SAPO-11(s) catalyst. The iso-hexane selectivity decreases with n-hexane conversion over all the catalysts (Fig. 10 (c)),indicating the increased rate of side reaction at higher n-hexane conversion.The Ni/SAPO-11(s) and Pt/SAPO-11(im)catalysts show similar iso-hexane selectivity. Both samples have much higher iso-hexane selectivity than the Ni/SAPO-11(im)which show a significant increase in cracking with n-hexane conversion (Fig. 10 (d)). In all cases, the iso-hexane selectivity follows the order: Ni/SAPO-11(s) ≈ Pt/SAPO-11(im)> Ni/SAPO-11(im). The yield of iso-hexane over the Ni/SAPO-11(s) is slightly lower than that over the Pt/SAPO-11(im) at temperature below 613 K, while it exceeds the latter as the temperature increases continuously (Fig. 10 (b)). Most interestingly, the Ni/SAPO-11(s) and Pt/SAPO-11(im) catalysts have nearly the same maximum iso-hexane yield at ca. 66.7 % at 613 K. In contrast, the Ni/SAPO-11(im) has the lowest iso-hexane yield at all the temperatures tested. Therefore, the Ni/SAPO-11(s) catalyst prepared by the novel direct synthesis method has comparable performance to the noble metalcatalyst Pt/SAPO-11(im) in terms of n-hexane conversion and iso-hexane selectivity. This resultsuggests that the Ni/SAPO-11(s) is a promising candidate for hydroisomerization catalysts.

A detailed products distribution for the Ni/SAPO-11(s), Ni/SAPO-11(im) and Pt/SAPO-11(im) at similar n-hexane conversion is shown in ). It might be attributed to the poor balance between (de)hydrogenation and acid functions which will be discussed later. High catalytic stability is also indispensable for practical application of the hydroisomerization catalyst. The stability of the Ni/SAPO-11(s) was studied preliminarily at 613 K and the result is shown in Fig. S6. The n-hexane conversion and iso-hexane yield exhibit a slight decrease during the initial 2 h and then remain almost constant. The iso-hexane selectivity experiences no significant change in spite of a slight increase in the initial 2 h. The results indicate that the Ni/SAPO-11(s) catalyst prepared via the novel method has a promising stability in the hydroisomerization of n-hexane.

Synergetic effect of metal and acid sites

The classical mechanism describing the alkanes hydroisomerization involves the following successive chemical steps: (i) dehydrogenation of alkanes into alkenes on metal sites, (ii) skeletal rearrangement of the alkenes on acid sites and (iii) hydrogenation of the branched alkenes to corresponding branched alkanes [32]. Thus, the catalytic behavior of the hydroisomerization catalyst is closely related to features of (de)hydrogenation sites and acid sites as well as the balance between them. TheNi/SAPO-11(s) in comparison to the Ni/SAPO-11(im)exhibits enhanced activity, which is attributed to more accessible metal and acid sites. The Ni/SAPO-11(s) catalyst also demonstrates higher iso-hexane selectivity than the Ni/SAPO-11(im). The better metal-acid balance for the Ni/SAPO-11(s), which is confirmed by its higher C Ni /C A ratio (0.224) than that over the Ni/SAPO-11(im) (0.158, Table 1), is the first explanation for this phenomenon. Under such circumstance, each alkene intermediate comes into fewer acid sites during its diffusion from one Ni site to another [61].

Thus, the subsequent cracking reaction on acid sites is suppressed, resulting in high iso-hexane selectivity. In contrast, owing to the small amount of metal sites in the Ni/SAPO-11(im) catalyst, the alkene intermediates will confront acid sites that are relatively excessive and then crack into smaller molecules, thus reducing the iso-hexane selectivity.Another explanation could be the proximity between metal and acid sites. For an ideal isomerization catalyst, metal and acid sites should be close enough so that the number of acid sties between two metal sites is low enough to catalyze only one step of skeletal rearrangement [62]. It helps to reduce the probability of cracking the alkene intermediates during the diffusion from acid sites to the nearest metal sites. The Ni/SAPO-11(s) catalyst has better metal-acid balance and closer metal-acid proximity which is contributed by the small metal particles. It seems to have higher level of ideality in terms of synergetic effect between metal and acid sites, which can be evidenced by the reaction pathway and products distribution as discussed later.

Conclusions

The Ni/SAPO-11(s) hydroisomerization catalyst with high dispersion of nickel species was prepared via the novel direct synthesis method; the nickel species and acid sites were instantaneouslyformedin the catalyst. Three types of nickel species in the catalyst were identified. The metallic nickel is the main active site for (de)hydrogenation and framework nickel supplies more acid sites for the n-hexane hydroisomerization. A great balance between the metal and the acid sites wasachieved via the direct synthesis method. The isomerization of alkene intermediates on the acid sites is the rate limiting step. The Ni/SAPO-11(s) catalyst exhibits one of the highest iso-hexane yields reported in the hydroisomerization of n-hexane.

The novel directsynthesis method opens a new door for preparation of metal supported catalysts.

Fig. 1

 1 Fig. 1 shows XRD patterns of the calcinedNi/SAPO-11(s), Ni/SAPO-11(im) and

Fig. 1 .

 1 Fig. 1. XRD patternsof(a) as synthesized SAPO-11(s), calcined Ni/SAPO-11(s)and Ni/SAPO-11(im) in the

Fig. 2 .

 2 Fig. 2. UV-vis diffuse reflectance spectra of the calcined Ni/SAPO-11(s), Ni/SAPO-11(im) and bulk NiO

Fig. 3 .

 3 Fig. 3. XPS spectra of the Ni2p core levelfor calcined Ni/SAPO-11(s),Ni/SAPO-11(im) and bulk NiO

Fig. 4 .

 4 Fig. 4. XANES spectra at the Ni K-edge of (a) NiO reference, (b) Ni/SAPO-11(s) and (c) Ni foil reference.

Fig. 5 .

 5 Fig. 5. TEM images of the calcinedNi/SAPO-11(s) (left) and Ni/SAPO-11(im) (right)catalysts

Fig. 7 .3. 4 Acidity

 74 Fig. 7. H 2 -TPR profiles ofsamples Ni/SAPO-11(s), Ni/SAPO-11(im) andSAPO-11(s)

  The Ni/SAPO-11(s) catalyst shows more acid sites than the Ni/SAPO-11(im).The amount of weak acid sites for Ni/SAPO-11(s) and SAPO-11(s) is similar, while the Ni/SAPO-11(s) contains more medium and strong acid sites. The Py-IR spectra collected after desorption at different temperatures (Fig. S4) implythatthe increased acid sites in the Ni/SAPO-11(s)are mainly composed of strong Brønsted acid sites.

Fig. 8 .

 8 Fig.8. FT-IR spectra recorded under pyridine adsorption on SAPO-11(s), and reduced Ni/SAPO-11(s)

Fig. 9 .

 9 Fig. 9. Catalytic performanceof SAPO-11(s), unreduced and reduced Ni/SAPO-11(s) catalysts

Fig. 10 .

 10 Fig. 10. Catalytic performance of samples Ni/SAPO-11(s), Ni/SAPO-11(im) and Pt/SAPO-11(im) (reference): n-C 6 conversion (a) and i-C 6 yield (b) versus temperature, selectivity to i-C 6 (c) and cracking products (< C 6 ) (d) versus n-C 6 conversion

Fig. 11 . 6 conversionsFig. 12 .Fig. 13 .

 1161213 Fig.11. The product distribution of n-hexane hydroisomerization over Ni/SAPO-11(s), Ni/SAPO-11(im)

  , the peak at 856.3 eV of Ni 2p 3/2 , together with the one at 873.6 eV of Ni 2p 1/2 indicate the existence of octahedral Ni 2+ in the NiO that strongly interacts with the SAPO-11[46,47]. The peaks at 857.6 and 875.3 eV, which are in the range of Ni 2p 3/2 and Ni 2p 1/2 , respectively, are assigned to nickel aluminate spinel

3 and 856.1 eV) for the Ni/SAPO-11(im) due to the interaction between NiO and the support. In contrast, for the Ni/

Table 1

 1 Nickel content, nickel sites (C Ni ), acid cites (C A ) and the C Ni /C A ratio over the Ni/SAPO-11(s) and

	Ni/SAPO-11(im) catalysts
	Sample	Ni content (wt %)	C Ni (μmol/g)	C A (μmol/g)	C Ni /C A
	Ni/SAPO-11(s)	4.0	55.4	247.6	0.224
	Ni/SAPO-11(im)	4.0	28.0	176.9	0.158

Table 2 .

 2 The selectivity to iso-hexane over the Ni/SAPO-11(s), Ni/SAPO-11(im) and Pt/SAPO-11(im) is 95.1, 84.4 and 95.7%, respectively. The Ni/SAPO-11(s) catalyst and the Pt/SAPO-11(im) referencecatalyst exhibit similar selectivity to methyl pentanes (MP),92.8% and 94.6%, respectively.While the

	and DMB selectivity, and they attributed this behavior to the metal-acid balance[60]. The
	Ni/SAPO-11(im) shows the highest selectivity to cracking products(15.6 %) vs the other
	catalysts Ni/SAPO-11(s)(4.9%) and Pt/SAPO-11(im) (4.3%

selectivity to methyl pentanes over Ni/SAPO-11(im) is only 81.3%. Ni/SAPO-11(s) and Ni/SAPO-11(im) show slightly higher selectivity to dimethyl butanes (DMB), 2.3 and 3.1%, respectively than that for the Pt/SAPO-11(im) (1.1%). This result indicates that nickel based hydroisomerization catalysts (Ni/SAPO-11(s) and Ni/SAPO-11(im)) favor the formation of di-branched isomers that have higher octane number than the mono-branched ones. It is consistent with the previous report by Eswaramoorthi and Lingappan, who found that the addition of nickel to Pt/H-β or Pt/H-mordenite catalysts increased the n-hexane conversion

Table 2

 2 S MP , S DMB , S t , andS C correspond to the selectivity to methyl pentanes, dimethyl butanes, iso-hexanes and cracking products, respectively.

	Pt/SAPO-11(im) catalysts at the n-hexane conversion of 51.5 (±2.0)%.

Products distribution of n-hexane hydroisomerization over Ni/SAPO-11(s), Ni/SAPO-11(im) and

a

Acknowledgements

This work was supported by the "Fundamental Research Funds for theCentral Universities (Grant No. 16CX06012A)", the "Shandong Province Natural Science Foundation of China" (Grant No. 2013ZRE28069), and the "National Natural Science Foundation of China" (Grant No. 21376267).


Simone Martini
email: simone.martini@unibo.it

The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation

Keywords: 2012 ACM Subject Classification Social and professional topics → History of programming languages; Software and its engineering → General programming languages Semantics of programming languages, history of programming languages, mathematical theory of computation Digital Object Identifier 10.4230/OASIcs.Gabbrielli.2020.8

Despite the insight of some of the pioneers (Turing, von Neumann, Curry, Böhm), programming the early computers was a matter of fiddling with small architecture-dependent details. Only in the sixties some form of "mathematical program development" will be in the agenda of some of the most influential players of that time. A "Mathematical Theory of Computation" is the name chosen by John McCarthy for his approach, which uses a class of recursively computable functions as an (extensional) model of a class of programs. It is the beginning of that grand endeavour to present programming as a mathematical activity, and reasoning on programs as a form of mathematical logic. An important part of this process is the standard model of programming languages -the informal assumption that the meaning of programs should be understood on an abstract machine with unbounded resources, and with true arithmetic. We present some crucial moments of this story, concluding with the emergence, in the seventies, of the need of more "intensional" semantics, like the sequential algorithms on concrete data structures. The paper is a small step of a larger project -reflecting and tracing the interaction between mathematical logic and programming (languages), identifying some of the driving forces of this process.

to Maurizio Gabbrielli, on his 60th birthday

Introduction

Statements like "the Java programming language is Turing-complete", or "the C program 'int x=0; while 1 {x++;}' is divergent", or even "the halting problem is undecidable for C programs", are common in most textbooks and in the practice of many computer scientists, despite the fact that they are false, for any actual implementation. The finiteness of any such implementation implies that the halting problem is decidable, being the system only a finitestate automaton; that the increment x++ will produce after a finite time an overflow which will be caught by some hardware interrupt; and that any Java implementation cannot compute

8:2

The Standard Model for Programming Languages functions requiring more resources than those of the universe. Of course, the statements become true when they are applied to a model of C or Java programs allowing for true unbounded arithmetic and unbounded (finite) resources. We propose to call standard model of programming languages this (informal) assumption, where programs are interpreted on an abstract machine with unbounded resources, and with true arithmetic. It is so "standard" that its use is almost never esplicitated in the literature (scientific, or in textbooks) -on the contrary, when another model is implied (for instance, one with finite arithmetic), that use is instead acknowledged and remarked. We are so used to the fact that a finite computer program could be regarded as the infinite function it computes, that we tend to forget that this "double view" was not born together with the general purpose electronic computer -it is rather the result of a deliberate research agenda of the end of fifties and the early sixties of the last century, responding both to internal and external forces of the discipline that was going to be called, also thanks to that agenda, Computer Science. It is the beginning of that grand endeavour to present programming as a mathematical activity, and reasoning on programs as a form of mathematical logic. The paper will present some of the moments of this process, where the components of a mathematical theory of computations are introduced as the technical, formal elements of the informal standard model. Before delving into these developments, however, we cannot forget the founding fathers of the discipline, who already realised this double nature of computer programs, but whose insight did not pass, at that time, into the practice of computing.

2

The Pioneers

The two years from 1947 to 1949 are of particular interest for our story. First, it is when Herman Goldstine and John von Neumann wrote the second part [START_REF] Goldstine | Planning and coding of problems for an electronic computing instrument[END_REF] of a series of reports on the "mathematical and logical aspects of an electronic computing instrument". Its aim is to give an account of the "methods of coding and of the philosophy which governs it". A major methodological tool is the use of flow diagrams for expressing the dynamics of a computation. Flow diagrams are made of four distinct classes of boxes: operation, alternative, substitution, and assertion boxes. While boxes of the first two kinds contain operations that the machine will ultimately perform, the contents of an assertion box "are one or more relations." A box of this kind "never requires that any specific calculation be made, it indicates only that certain relations are automatically fulfilled whenever" the control reaches that point 1 . Assertion boxes are "logical expressions" that remain invariant during the computation -their only reason for being present in a diagram is that they are needed (or useful) in establishing that the diagram correctly renders "the numerical procedure by which the planner has decided to solve the problem", which is expressed in the "language of mathematics" 2 . For this reason, coding "has to be viewed as a logical problem and one that represents a new branch of formal logics." While the word "logic" (or "logical") does not necessarily refer to mathematical (formal, or symbolic) logic in the literature of that period 3 , the reference to a "new branch of formal logics" is explicit. Assertions bring mathematical logic into the very notation for writing programs; moreover, references to other notions of formal languages are present in other places of [START_REF] Goldstine | Planning and coding of problems for an electronic computing instrument[END_REF], like the distinction between free and bound variables. "Formal logic" is for Goldstine and von Neumann at the core of programming, as the discipline where assertions may be written and proven. An analogous use of assertions for "checking [the correctness of] a large routine" will be proposed by Alan Turing two years later. In [START_REF] Turing | Checking a large routine[END_REF] 4 he lucidly describes a proof of correctness as consisting of three different steps. First, "the programmer should make assertions about the various states that the machine can reach." Then, "the checker [i.e., the one doing the proof] has to verify that [these assertions] agree with the claims that are made for the routine as a whole." "Finally the checker has to verify that the process comes to an end." Observe the clarity by which full correctness (in today's terms) is spelled out, the distinction between specification ("claims that are made for the routine as a whole") and implementation, and the interplay between these two, where assertions play their role.

Turing brings us back to year 1947, when he also writes a paper with some remarks on mathematical logic in computer programming. In the "Lecture on Automatic Computing Engine" [START_REF] Turing | Lecture to L.M.S[END_REF] he has already clear that programming a computing machine could be done, in principle, with languages much more sophisticated than the machine instructions that were available at the time. Indeed, "in principle one should be able to communicate [with these machines] in any symbolic logic, provided that the machine were given instruction tables which would allow it to interpret that logical system." Like Goldstine and von Neumann, also Turing sees a bright future for mathematical logic (to be understood, in this case, as the discipline of artificial languages): "there will be much more practical scope for logical systems than there has been in the past. " Haskell B. Curry in those same years uses his logical apparatus in order to program the new computing machines. Discussing an inverse interpolation routine and its correctness, in [START_REF] Haskell | On the composition of programs for automatic computing[END_REF] he introduces a notion of type for memory words: those containing instructions (orders), and those containing data (quantities). Starting from this, as reconstructed by [START_REF] De Mol | Haskell before Haskell: an alternative lesson in practical logics of the ENIAC[END_REF], he builds a surprising, non-trivial mathematical theory of programs, containing theorems analogous to the "well-typed expressions do not go wrong"5 of [START_REF] Milner | A theory of type polymorphism in programming[END_REF], and he uses them to define classes of program transformations and compositions which are "safe" for the intended operational semantics. The presence of mathematical logic is so explicit that Curry's reports will get a review on the Journal of Symbolic Logic6 .

A lesser-known contribution is the early work of Corrado Böhm, a few years later. His thesis at ETH Zurich7 esplicitely connects the new computing machines to the mathematical, abstract analysis of Turing, up to the claim that "les calculatrices les plus évoluées sont universelles, au sens spécifié par M. Turing." Under this assumption, Böhm may assume that all the general purpose, stored-program computers "sont, au point de vue logicomathématique, équivalentes entre elles," so that he may choose a specific type of computer (a three-address machine) without any loss of generality. These remarks, and the explicit

8:4

The Standard Model for Programming Languages connection to Turing's theory, that to most of us seem obvious, were not (yet) part of the standard background of the people working in the field of automatic computing machines. Of course, they were known to some of the other giants (von Neumann and his peers in primis; Böhm's advisor Paul Bernays is the probable source who mentioned Turing's work to him), but it will be only much later that Turing will become the iconic figure of father for computer science [START_REF] Daylight | Towards a historical notion of 'Turing -the father of computer science[END_REF] 8 . Another striking observation in Böhm's thesis is that a program is seen under a double interpretation: as a description of the behaviour of a computer, and as the description of a "méthode numérique de calcul." Without forcing the interpretation, we may read this as one of the first explicit references to the duality between an operational description of the behaviour of an (abstract) machine, and the numerical function that results from that sequence of operations.

The far-sight of these pioneers should not obfuscate the fact that the role of logic in the early days of the digital computing machines (both their design and their programming) was modest, if not absent (e.g., [START_REF] Daylight | Towards a historical notion of 'Turing -the father of computer science[END_REF][START_REF] De Mol | Less is more in the fifties. Encounters between logical minimalism and computer design during the 1950s[END_REF]). Programming those machines was more a technological affair, strictly coupled to the technology of the different computers. Despite the genial recognition by Turing that "any symbolic logic" could be used as a programming language, it is only during the fifties, and with graduality, that programming started to be perceived as a "linguistic activity" [START_REF] Nofre | When technology became language: The origins of the linguistic conception of computer programming, 1950-1960[END_REF]. As for the correctness of programs, Knuth's recollection [START_REF] Donald | in memoriam[END_REF] is that at the end of the fifties "the accepted methodology for program construction was [. . . ]: People would write code and make test runs, then find bugs and make patches, then find more bugs and make more patches, and so on. We never realized that there might be a way to construct a rigorous proof of validity." "The early treatises of Goldstine and von Neumann," and of Turing, and Curry, "which provided a glimpse of mathematical program development, had long been forgotten." In summary, while there are important relations with other parts of mathematics, like numerical analysis (e.g., Jim Wilkinson's backward error analysis), or automata theory (from von Neumann, to Kleene's regular events, to Rabin and Scott), or cybernetics, at the macro scale little happens on the explicit border between logic and the new field of computing, which at that same time struggled to be recognised as an autonomous scientific discipline 9 . In this process, the availability of computer-independent ("universal," in the terminology of the time) programming languages allowed the expression of algorithms 8 Describing the relations between Turing's work -and especially the notion of Turing machine, -the modern digital computer, and computer programming, is well outside the scope of this paper. For some of the relations between Turing and von Neumann, see Stanley Frankel's letter to Brian Randell, quoted in [START_REF] Randell | On Alan Turing and the origins of digital computers[END_REF]. An argument on the equivalence of Turing machines and McCulloch and Pitts's neuron nets "supplied with an infinite blank tape," can be found in von Neumann's [START_REF] John Von Neumann | Rigorous theories of control and information[END_REF]. A balanced review of the actual impact of Turing on computer science may found in Section 5 of Liesbeth De Mol's entry on Turing machines for the Stanford Encyclopedia of Philosophy [START_REF] De | Turing Machines[END_REF], from which we quote the following.

"Recent historical research shows also that one should treat the impact of Turing machines with great care and that one should be careful in retrofitting the past into the present." Only "in the 1950s then the (universal) Turing machine starts to become an accepted model in relation to actual computers and is used as a tool to reflect on the limits and potentials of general-purpose computers by both engineers, mathematicians and logicians." See also [22,[START_REF] Daylight | Towards a historical notion of 'Turing -the father of computer science[END_REF]. 9 A struggle that was going to be long. Still in 1967, Perlis, Newell and Simon (all of them will receive the Turing award; Simon will also be a Nobel laureate in Economics) feel the need of a letter to Science [START_REF] Newell | [END_REF] to argue "why there is such a thing like computer science".

in a machine neutral way, thus making algorithms and their properties amenable to a formal study. Programming languages themselves were treated as an object of study, starting from the formal definition of Algol's syntax [START_REF] Backus | The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference[END_REF][START_REF] Backus | Report on the algorithmic language ALGOL 60[END_REF]. For an entrance ticket to "science", however, a complete "theory" was needed, encompassing also semantics of programming languages and their use in program development.

Towards a General theory

The construction of a "mathematical theory of computation," (or a "mathematical science of computation") is the explicit goal of John McCarthy, starting from 1961 (when he was still at MIT) and covering his first period at Stanford, where he moved in 1963. In [START_REF] Mccarthy | A basis for a mathematical theory of computation[END_REF] 10 he sketches an ambitious plan for a general theory, based on mathematical logic, that could serve as a foundation for computation, in such a way that "it is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last." After having dismissed numerical analysis (for being too narrow for a general theory), computability theory (for focussing on undecidability, instead of positive results, and for being uninterested on properties of algorithms), and finite automata theory (for being of no use in the treatment of computers, because they have too many states), it proceeds to list the "practical" (sic) results of the theory. The first is "to develop a universal programming language": Algol is a good step in the right direction, but it has several "weaknesses", among which the impossibility to describe different kinds of data 11 . Second, "to define a theory of the equivalence of computation processes," to be used to define and study equality preserving transformation. Let us esplicitate what McCarthy leaves unsaid: once we have an accepted model for the behaviour of a program, we may study under which transformations of (the syntactical presentation of) the program the behaviour remains invariant (in the model). A third goal goes in the same direction: "To represent computers as well as computations in a formalism that permits a treatment of the relation between a computation and the computer that carries out the computation." The models for both the program and its executing agent should be expressed in the same conceptual framework, in the same theory, so that one may express relations among the two, like the fact that (the model of) the computer that carries out the computation is "sound" with respect to (the model of) the program. Contrasting the lack of interest of recursive function theory for the positive results and for the properties of algorithms, a fourth goal is "to give a quantitative theory of computation [. . . ] analogous to Shannon's measure of information."

The paper does not elaborate further on this point; we may probably ascribe to this goal the development of computational complexity. Finally, a last purpose of a general theory would be "to represent algorithms by symbolic expressions in such a way that significant changes in the behavior represented by the algorithms are represented by simple changes in the symbolic expressions." Once again the point will not be taken up again in the rest of the paper, besides explaining that it is relevant for programs that "learn from experience".

For our purposes, it suffices to stress the reference to the availability of (a model of) the behaviour of a program and to the interplay between the syntactic representation of the algorithm and that behaviour.

8:6

The Standard Model for Programming Languages

The technical contents of the paper, of course, cannot match the grandeur of these goals. The paper introduces a theory of higher order, partial computable functions on arbitrary domains, defined by composition, conditional statements, and general recursion. Moreover, a uniform way to define new data spaces is presented -data space constructors are the Cartesian product, the disjoint union, and the power set, each of them equipped with its canonical maps, which are used to define functions on the new spaces from functions on the base spaces. Base data spaces could be taken as frugal as the single "null set", since natural numbers could be defined from it. The goal is to provide general, abstract mechanisms, instead of choosing an arbitrary new palette of primitive types.

The picture sketched in [START_REF] Mccarthy | A basis for a mathematical theory of computation[END_REF] is further developed in [START_REF] Mccarthy | Towards a mathematical science of computation[END_REF] (to "be considered together with my earlier paper"), which contains a first attempt for an epistemology for (the still unborn) computer science 12 , and introduces again, after the pioneers, the problem of program correctness: "Instead of debugging a program, one should prove that it meets its specifications, and this proof should be checked by a computer program. For this to be possible, formal systems are required in which it is easy to write proofs." Of course, one needs first a semantics for the behaviour of a program. This is an important contribution of the paper: programs expressed as sequences of assignments and conditional go to's are given meaning as recursive functions acting on the set of current values of the variables (the "state vector"). Each statement of the program corresponds to such a recursive function, the meaning of a program being obtained by a suitable composition of these functions, in a compositional approach which will be the cornerstone of formal program semantics. Moreover, the proof technique of "recursion induction," already introduced in [START_REF] Mccarthy | A basis for a mathematical theory of computation[END_REF], is extended, so that it could be applied directly to programs without first transforming them to recursive functions. This last contribution is particularly relevant for our story: the program is implicitly understood as a representative for its meaning, so that one may argue on the program (a finite, textual object) for obtaining results on its model (an infinite function over the set of possible data).

McCarthy will not develop the formal semantics introduced in his two papers, and the creation of a mathematical semantics for programs is usually credited to Robert Floyd [START_REF] Floyd | Assigning meanings to programs[END_REF] 13 and Tony Hoare [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. Both are lucid on the need of a machine independent meaning of programs, and the need of formal theories for reasoning on programs. For Hoare, "computer programming is an exact science in that all the properties of a program and all the consequences of executing it in any given environment can, in principle, be found out from the text of the program itself by means of purely deductive reasoning." Sola scripta are normative for the behaviour of a program: a model for the semantics is implicit and implied.

In those same years, the construction of an explicit semantic model of a programming language is the goal of Christopher Strachey, after ideas of Peter Landin [START_REF] Peter | The mechanical evaluation of expressions[END_REF]. Starting with [START_REF] Strachey | Towards a formal semantics[END_REF], presented at a working conference in 1964, and especially with the (then unpublished) notes of a course at Copenhagen in 1967 [START_REF] Strachey | Fundamental concepts in programming languages[END_REF], Strachey presents a full-blown account 14 of a mathematical semantics of a programming language, introducing the notions of "abstract store" and "environment," for modelling assignments and side-effects. Commands are interpreted 12 "What are the entities with which the science of computation deals? What kinds of facts about these entities would we like to derive? What are the basic assumptions from which we should start?" 13 "An adequate basis for formal definitions of the meanings of programs [. . . ] in such a way that a rigorous standard is established for proofs about computer programs." "Based on ideas of Perlis and Gorn." "That semantics of a programming language may be defined independently of all processors [. . . ] appear[s] to be new, although McCarthy has done similar work for programming languages based on evaluation of recursive functions." 14 See, for instance, Figure 1 of [START_REF] Strachey | Fundamental concepts in programming languages[END_REF], page 17 of the reprinted version.

as functions from stores to stores. The basic semantical domains for values are not discussed, but in a later monograph Strachey will esplicitely refer to "abstract mathematical objects, such as integers," in such a way that "when we write a statement such as x := Sin(y + 3) in ALGOL 60, what we have in mind is the mathematical functions sine and addition. It is true that our machines can only provide an approximation to these functions but the discrepancies are generally small and we usually start by ignoring them. It is only after we have devised a program which would be correct if the functions used were the exact mathematical ones that we start investigating the errors caused by the finite nature of our computer."

We cannot treat in this paper how mathematical logic and programming languages interacted from the end of sixties -a process much less linear than we may think from today's perspective. Even the relations between the notion of "type" in the two fields are not as straightforward as they may seem [START_REF] Martini | Several types of types in programming languages[END_REF][START_REF] Martini | Types in programming languages, between modelling, abstraction, and correctness[END_REF]. An important chapter of that story would be that of logic programming languages (starting from Colmerauer in 1970 and Kowalski in 1974), where logic enters as a first-class actor (see [START_REF] Miller | Reciprocal influences between proof theory and logic programming[END_REF]).

4

The Standard Model

The previous section sketched the gradual proposal of (several) semantics for programming languages that could abstract from specific processors and their limitations. While general semantical theories of programming languages had limited impact outside the research communities, the natural approach to a program as the description of a computation happening on an abstract (and largely unspecified) computational device had a major impact. True arithmetic and (in principle) unbounded resources is all that is required of such an abstract processor, that in the Introduction we identified as the standard model: the naturalness of assuming these simple hypotheses, gave the standard model the momentum it needed to establish itself as a permanent fixture in programming language theory and education 15 . Several reasons cooperate for the establishment of such standard model. One is certainly the need to validate computing as a science --a mathematical theory is always the entrance ticket to science. Several successes of the use of mathematics into computing were already present at the end of the sixties, like the theory of deterministic parsing (LL and LR), the application of formal language theory, complexity theory, and of course numerical analysis. Despite the large body of results (and relevant problems) in these areas, it is mathematical logic that, as we have seen, dominate the field of programming languages, up to the view (or dream) of McCarthy that logic will be for computation what analysis has been for physics. But a theory of program correctness (which, as we have seen, is deeply connected to the emergence of the standard model) is needed also by other reasons, internal to the 15 This is not to say that other perspectives were absent. In a 1965 letter to the Computer Journal [START_REF] Strachey | An impossible program[END_REF] Strachey proves the undecidability of the halting problem for his Algol-like language CPL, assuming (without saying it!) the standard model. Among the reactions to the letter, the one by W.D. Maurer (27 August 1965) clearly doesn't share the "common ground": Strachey's "letter was of particular interest to me because I had, several months ago, proved that it is indeed possible to write such a program," evidently by assuming a finite automaton as a processor. We find different views also among the founders of the mathematical theory of programs. In the same year of Strachey's [START_REF] Strachey | The varieties of programming language[END_REF], Edsger W. Dijkstra writes: "We are considering finite computations only; therefore we may restrict ourselves to computational processes taking place in a finite state machine -although the possible number of states may be very, very large -and take the point of view that the net effect of the computation can be described by the transition from initial to final state." "One often encounters the tacit assumption that [. . . ] the inclusion of infinite computations leads to the most appropriate model." "However, we know that the inclusion of the infinite computation is not a logically painless affair." "It seems more effective to restrict oneself to finite computations." [START_REF] Edsger | A simple axiomatic basis for programming language constructs[END_REF].

Gabbrielli's Festschrift

8:8

The Standard Model for Programming Languages discipline, and probably more important. As an applied discipline -at the end, programs will be used in the real world by real people -computing needs a way to ensure that what it delivers satisfies the requirements on its use. McCarthy's remark on the relations between physics and mathematics seems to suggest that the model here is structural engineering, where mathematical physics laws and empirical knowledge are used together to understand, predict, and calculate the stability, strength and rigidity of structures for buildings. The mathematical theory of computation and its standard model are instrumental for reaching an analogous standard of rigor, so that "when the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics," as Hoare writes in his landmark paper on program correctness [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] 16 . In this, computing has a big advantage over structural engineering -only the very last layer of the deployment of a system ("the reliability of the electronics") is left out of reach of the formal approach. Since all levels in the hierarchy of a computing system are of the same, abstract nature, all levels could be subject (at least conceptually) to the same analysis. When a formally proved chain of compilers will be availabile, a proof that a model of the higher level program satisfies a certain condition, transfers automatically to a proof that a model of the low level program satisfies some other condition, also obtained automatically from the higher level one. No concrete, no iron, no workmanship is involved. In this context, the standard model is to programming languages what movement without friction is to mechanics. And this is why it is so important. It is not that it implies Turingcompleteness that matters, but its simplicity and the fact that, indeed, one may do some mathematics with it. The analogy with the Galilean effort for physics is illuminating -no bodies of different masses reach the ground at the same time when they actually fall from the leaning tower of Pisa, like there is no true unbounded arithmetic inside any laptop; or there is no true isochronous pendulum in nature. Yet, you do not understand a single bit of mechanics if you don't abstract away friction, and don't approximate to small oscillations.

The standard model comes with three features, deeply connected among them. First, compositionality -the meaning of a complex construct is obtained from the meaning of its constituents, by composing them in a way that only depends on the construct under consideration. Second, extensionality -two constructs with the same input-output behaviour (on their intended domains) have also the same meaning. Finally, referential transparency -"if we wish to find the value of an expression which contains a sub-expression, the only thing we need to know about the sub-expression is its value. Any other features of the sub-expression, such as its internal structure [. . . ] are irrelevant to the value of the main expression" [START_REF] Strachey | Fundamental concepts in programming languages[END_REF] 17 .

Other subtle ingredients are present, but mostly hidden, the most important one being continuity, which is the abstract characterization of the finitary character of the operations which occur during a computation 18 . In recursive function theory, continuity was implicit in Kleene's first recursion theorem [START_REF] Stephen | Introduction to Metamathematics[END_REF], and then exploited in a beautiful set of results, whose apex are the Rice-Shapiro and Myhill-Shepherdson theorems (see [START_REF] Rogers | Theory of Recursive Functions and Effective Computability[END_REF]), of the second half of of the fifties. Programming language semantics has a problem analogous to those solved by Kleene's recursion theorem -how to give meaning to (multiple) recursive definitions. In his PhD thesis at MIT, Morris [START_REF] Morris | Lambda-calculus models of programming languages[END_REF] uses the fixed-point combinator of the λ-calculus to link recursion in programming languages to recursive function theory. He shows that the fixed-point operator, applied to a recursive definition, gives the least solution with respect to a certain operational order. It was then Dana Scott to put continuity under spotlight [START_REF] Scott | Outline of a mathematical theory of computation[END_REF], and to make it one of the cornerstone of the denotational semantics approach (also to solve those recursive equations between domains which are needed in Strachey's approach.)

One of the most important characteristics of a good semantic definition is that it allows for multiple concrete realisations ("implementations") -it must not anticipate those choices that should only be made when the language is implemented. One possible approach to the definition of a language, in fact, could be to define the meaning through a particular interpreter: "This used to be quite common: languages would be "as defined by" some particular compiler" [START_REF] Stoy | Denotational semantics: The Scott-Strachey approach to programming language theory[END_REF]. In this way, however, all the details of that "particular compiler" are needed in order to understand a program. Even more important, to what level of detail is this canonical implementation normative? Is the computation time of a program part of its definition? Is the reporting of errors? The difference between definition and implementation is crucial in the literature we have cited in the previous section. The proposed models are a possible result of the difficult quest for the happy medium between exactness and flexibility, in such a way as to remove ambiguity, still leaving room for implementation (see [START_REF] Gabbrielli | Programming Languages: Principles and Paradigms[END_REF]).

Finally, the explicit availability of models (and especially of the standard model) allows for a clear separation between specification (normative, expressed in the explicit or implicit model), and implementation (that it be abstract or concrete has little importance in this context). Programs are not only abstract mathematical objects living in the theory of computation; nor are only textual, concrete objects embodied in a processor, and thus living in the physical world. The specification defines their function 19 , while implementation realises that function -it is only in the interplay among these two aspects that programs get their ontology as technical artifacts [START_REF] Turner | Programming languages as technical artefacts[END_REF].

More Intensional Models

What we have called the standard model is in reality a plurality of abstractions, depending on the language which is modelled. They all share the fact that the numerical functions on the integers are the true arithmetical ones, and that computation happens on an (abstract) processor with unlimited resources (in storage, and time). Coping with real languages required, since the beginning, the introduction of several complications, for instance to deal with side effects (which needed environments and stores), or unrestricted jumps (which required continuations to be used). Still, much effort was in ensuring that the "internal structure" of a program didn't influence its meaning: two different algorithms for the same functions (with the same side-effects, if any), should give rise to the same semantics. This is, after all, what extensionality is about. But this is also an important simplification, or abstraction, that at some point one needs to overcome -real movement happens with friction. Moreover, the fact that the domains involved in the semantics should have "the usual mathematical properties" is something that called for a subtler investigation. One of the first questions to be tackled, was how to characterise (express, study) sequentiality, an important, intensional aspect of certain computations. For this, some notion of "event" seemed essential, to be the elementary building block to serialize. In one of

8:10

The Standard Model for Programming Languages the first papers attempting to model parallel programming, Gilles Kahn [START_REF] Kahn | The semantics of a simple language for parallel processing[END_REF] described a network of sequential processes, communicating through unbounded queues; together with Dave MacQueen, he constructed an operational model for such processes, which, in response to a request, consume data to produce output [START_REF] Kahn | Coroutines and networks of parallel processes[END_REF]. Is there a reasonable mathematical (denotational) model for such processes?

Almost at the same time, Gérard Berry studied bottom-up computations, where recursion is understood as a production of "events" [START_REF] Berry | Séquentialité de l'évaluation formelle des lambda-expressions[END_REF]; he soon discovered [START_REF] Berry | Modèles complètement adéquats et stables des lambda-calculs typés[END_REF] that computation in λ-calculus is intrinsically sequential 20 . Are there models built only with sequential functions, thus "closer" to the operational behaviour 21 ?

The answer to these questions came in a series of contributions by Kahn, Berry, Plotkin, and Pierre-Louis Curien (in several configurations as co-authors). The outcome were the notions of concrete data structure, concrete domain, and sequential algorithms. Sequential algorithms [START_REF] Berry | Sequential algorithms on concrete data structures[END_REF] are (Kahn-Plotkin [START_REF] Kahn | Concrete domains[END_REF]) sequential functions, equipped with a strategy for their computation, expressed in a demand-driven way, as in [START_REF] Kahn | Coroutines and networks of parallel processes[END_REF] 22 . The model of sequential algorithms is "intensional": there are programs with the same input-output behaviour which are separated in the model. It is not a surprise that a similar notion of intensionality is found in Glynn Winskel's event structures [START_REF] Winskell | Events in Computation[END_REF], developed almost at the same time than sequential algorithms, and which may be seen as a generalization of concrete domains (which already contains a notion of incompatibility between elements) 23 .

From there, semantics of programming languages strived to cope also with intensional phenomena, trying, at the same time, to not abandon the power and simplicity of extensional reasoning.

But telling that story would require another paper. Which I shall write for Maurizio's seventieth birthday.

  The first Computer Science department of the US was established in 1962 at Purdue University; Samuel D. Conte, first Head of that department, will recall in a 1999 Computerworld magazine interview: "Most scientists thought that using a computer was simply programming -that it didn't involve any deep scientific thought and that anyone could learn to program. So why have a degree? They thought computers were vocational vs. scientific in nature" (quoted in Conte's obituary at Purdue University, 2002). Next computer science departments to be established would be those at the University of North Carolina at Chapel Hill, in 1964, and at Stanford in 1965.

Also substitution boxes do not specify any computation; they represent a change in notation, more specifically in the relation between the internal and the external notation, a significantly different perspective from the modern use of flow charts, see[START_REF] Knuth | The early development of programming languages[END_REF].

We will come back to this duality between the specification and the implementation (in the today's terminology, of course) at the end of Section 4.

"Logical" is usually opposed to "physical", or "electronical", like in "logical design of digital circuits"; or in the very title of the series in which[START_REF] Goldstine | Planning and coding of problems for an electronic computing instrument[END_REF] appears: "mathematical and logical aspects of an electronic computing instrument."

See also[START_REF] Francis | An early program proof by Alan Turing[END_REF], for a reprint of the original paper, and a commentary.

"Suppose we have an initial type determination for the initial program", that is an assignment of types to words which assign type "order" to any instruction, and type "quantity" to any data, then the memory "word at the control location is always [scil., at any time during execution] an order"[START_REF] Haskell | On the composition of programs for automatic computing[END_REF], number 26.

By G.W. Patterson, JSL 22(01), 1957, 102-103.

Written under the direction of E. Stiefel and P. Bernays, submitted in 1952, and published in 1954[START_REF] Böhm | Calculatrices digitales. Du déchiffrage des formules logico-mathématiques par la machine même dans la conception du programme[END_REF]; see alsoKnuth's [29].Gabbrielli's Festschrift

The preliminary version is from 1961; the final 1963 version contains a new section on the "relations between mathematical logic and computation."

Note, en passant, that the word "type" is still not used in this context, for a collection of homogeneous values; see[START_REF] Martini | Several types of types in programming languages[END_REF].

Verification of a concrete system, of course, is not the same as verifying its (mathematical) model. A full literature exists on the limitations of formal verification, e.g.[21,

[START_REF] James | Program verification: The very idea[END_REF][START_REF] Millo | Social processes and proofs of theorems and programs[END_REF][START_REF] Turner | Computational Artifacts[END_REF].[START_REF] James | Program verification: The very idea[END_REF] For this use of the expression "referential transparency", Strachey quotes Quine[START_REF] Van Orman Quine | Word and Object[END_REF] (it is in §30), who in turn refers to Whitehead and Russell's Principia Mathematica.[START_REF] Floyd | Assigning meanings to programs[END_REF] See[START_REF] Cardone | Continuity in semantic theories of programming[END_REF] for a historical reconstruction of the relevance of continuity in early programming language semantics.

See, for instance,[START_REF] Kroes | Engineering and the dual nature of technical artefacts[END_REF][START_REF] Turner | The philosophy of computer science[END_REF]

Acknowledgements I am happy to thank Edgar Daylight for mentioning me Strachey's letter to the Computer Journal, and for the many critical reactions to the main thesis of this paper.

8:12

The Standard Model for Programming Languages

Funding Simone Martini: Research partially conducted while on sabbatical leave at the Collegium -Lyon Institute for Advanced Studies, 2018-2019. Partial support from French ANR project PROGRAMme.