text:
# Estimating damping factor for steel in flexural oscillation

1. Apr 4, 2013

### Engineer_Phil

I am trying to estimate the damping ratio of steel in bending. I have a situation where I need to know the dynamic response of an inverted pendulum. A picture is worth a thousand words, so here you go:

The vibration will be free; it is caused be the initial position of the system. I can calculate the stiffness of the flexural steel based on the length, cross section, and material properties.

The problem is estimating the damping. I want to know how long it takes the ocsillations to die down to a specified level.

I have done some research on google and so far I have only been able to find lengthy thesis full of differential equations and no real applicable conclusions. I am aware of the logarithmic decrement method, but I do not have the luxury of setting up a full scale model.

What I am looking for is some sort of relation between the geometry and the material properties to estimate the damping. Can someone point me in the right direction?

Thank you!

File size:
14.3 KB
Views:
1,591
2. Apr 4, 2013

### AlephZero

The amount of energy damped by the material in the steel plate itself will be very small. The main source of damping is likely to be the way the plate is fixed to the "rigid" base, and that usually defies any analysis. For example if it is clamped or bolted, tiny amounts of oil and grease in the joint can increase the damping by a surprisingly large amount (factors of 10 or more!)

The next biggest damping effect would probably be air resistance which is also hard to calculate.

If you want to do calculations with an "accurate" damping level, the best option is measure it. A reasonable ballpark figure would be about 1% or 2% of critical damping (and of that, maybe 0.1% is from the hysteresis of the steel plate as it bends, the rest is from other sources).

3. Apr 4, 2013

### Engineer_Phil

The 'fixed' end condition is based upon the flexible steel plate being welded to a massive chunck of steel. But what I called the 'rigid massless bar' is bolted to the steel plate.

1% to 2% critical damping means there will be a lot of oscillations which is not what I am looking for. What would be a good way to increase the damping?

Just to satisfy my curiousity, how would you calculate the damping effect of the steel plate?

4. Apr 4, 2013

### AlephZero

Lots of things you could think about doing:

• Bolting the "rigid bar" to the plate with some rubber washers (or a more specialized elastomer damping material) would be a start.
• Change the material of the steel plate to something like rubber.
• Replace the plate by a set of laminations that have to slide over each other with friction between them when it bends (like an old-style leaf spring).
• You can get self-adhesive sheets of damping material to apply to the surface of components that bend (like your plate) - though you might have a problem buying only a small quantity
• Add something to the structure to increase the air resistance (e.g. fix a flat plate to the rod)
• Or even immerse the whole device in a high viscosity liquid instead of air.

In real life (at least in my experience) the damping factors used in calculations are mostly based on experience and measurements of similar systems, not calculated from first principles.

5. Apr 4, 2013

### Engineer_Phil

Thanks for the help. Unfortunately this is a rare situation at our company and no one really has any experience estimating damping factors.

I find it hard to believe that everyone builds prototypes to test what their damping is, or make guesses based on prior projects. It seems like there would be a method of sometype out there to atleast get a close estimate. But maybe there are just too many factors to account for.

6. Apr 5, 2013

### timthereaper

You can use a modified form of the formulas presented in the screenshots. The tables come from the textbook System Dynamics by Palm. You can set up an ODE of the form $m\ddot{x}+c\dot{x}+kx = 0$ and specify the way you want your x(t) to act and solve for your damping constant c. You'll probably have to use a modified form for the mass of your cantilevered beam because it assumes the beam's mass is distributed across the whole length up to the concentrated mass.

Hope that helps!

File size:
59.7 KB
Views:
394
File size:
71.6 KB
Views:
339
7. Apr 5, 2013

### Engineer_Phil

I know how to evaluate what I want c or ζ to be. The problem is designing the system to give me that value.

8. Apr 5, 2013

### timthereaper

So how is your system different than the cantilevered spring with a damping coefficient? I thought that you could build the ODE and solve. Is there something I've missed?


text:
# Free Fall Formula

Freefall as the term says, is a body falling freely because of the gravitational pull of our earth.

Imagine a body with velocity (v) is falling freely from a height (h) for time (t) seconds because of gravity (g).

Free Fall Formulas are articulated as follows:

$h\,&space;=\,&space;\frac{1}{2}\,gt^{2}$
$v^{2}\,&space;=\,&space;2gh$
$v\,&space;=\,&space;gt$

Free fall is independent of the mass of the body. It depends only on the height and the duration the body is flung for.

## Freefall Related Solved Examples

Underneath are given questions on free fall which may be useful for you.

Problem 1: Calculate the body height if it has mass of kg and after 7 seconds it reaches the ground?

Given: Height h =?
Time t = 7s
We all are acquainted with the fact that free fall is independent of mass.

Hence, it is given as

$$\begin{array}{l}h = \frac{1}{2}gt^{2}\end{array}$$

h = 0.5 × 9.8 × (7)2

h = 240.1 m

Problem  2: The cotton falls after 3 s and iron falls after 5 s. Which is moving with higher velocity?

format: plain


text:
mersenneforum.org > Math Question about a mersenne-number property
 Register FAQ Search Today's Posts Mark Forums Read

2011-03-04, 16:16   #12
R.D. Silverman

"Bob Silverman"
Nov 2003
North of Boston

2·3·29·43 Posts

Quote:
 Originally Posted by R.D. Silverman You just changed your original statement. Your original statement was that x^n = x is not true when n = 2^p-1 is composite. Here x = 2^a + 2^b for a!= b This is different from x^{n-1} = 1 is not true when n = 2^p-1 is composite.
Note that 34 = 2^1 + 2^5 and 34^255 = 34 mod 255. Enough said?

Not enough? Note that 65 = 2^0 + 2^6 and 65^510 = 1 mod 511.

Still not enough? 72 = 2^3 + 2^6 and 72^510 = 1 mod 511.

I am sure that one could find additional counter-examples.

There was no reason to believe that an integer with Hamming weight 2
could not be a false witness to Mersenne numbers.

2011-03-04, 16:29   #13
sascha77

Jan 2010
germany

2·13 Posts

Quote:
 Originally Posted by mart_r Well, (211+21)2046 $\equiv$ 1 (mod 2047). a-b=10 $\not\equiv$ 11 (mod 2047)
No. This is false.

set p=11
->$n=2^{p}-1 = 2047$

for this:
$(2^{11}+2^{1})^{2046} \equiv (\;(2^{11} + 2^{1})\;mod(\;2047)\;)^{2046} \equiv 3^{2046} \equiv 1013\;(mod\; 2047)$

2011-03-04, 16:39   #14
sascha77

Jan 2010
germany

2×13 Posts

Quote:
 Originally Posted by R.D. Silverman Note that 34 = 2^1 + 2^5 and 34^255 = 34 mod 255. Enough said? Not enough? Note that 65 = 2^0 + 2^6 and 65^510 = 1 mod 511. Still not enough? 72 = 2^3 + 2^6 and 72^510 = 1 mod 511. I am sure that one could find additional counter-examples. There was no reason to believe that an integer with Hamming weight 2 could not be a false witness to Mersenne numbers.

OK. my fault. I forgotten to mention that mersenne Numbers are Numbers of the Form n = 2^{p}-1 with:
The variable p is prime !!!!!

If the mersenne number $n$ with $n=2^{p}-1$ is also prime then this
Mersenne Number is called Mersenne Prime.

Your example with mod 511 -> $511 -> 2^{9}-1$

9 is not prime. -> 511 is not a mersenne number.

And 255 = $2^{8}-1 .$

-> 8 is also not prime -> 255 is not a mersenne number

Last fiddled with by sascha77 on 2011-03-04 at 16:44

2011-03-04, 18:26   #15
R.D. Silverman

"Bob Silverman"
Nov 2003
North of Boston

2·3·29·43 Posts

Quote:
 Originally Posted by sascha77 OK. my fault. I forgotten to mention that mersenne Numbers are Numbers of the Form n = 2^{p}-1 with: The variable p is prime !!!!!
That is one definition. You will also find the definition
spread throughout the literature that a Mersenne Number is of the
form 2^n-1 for any n .

Quote:
 Your example with mod 511 -> $511 -> 2^{9}-1$
It is likely that I can find other counter-examples for the case n = prime
if I look hard enough.

It isn't worth my time.

2011-03-04, 18:52   #16
mart_r

Dec 2008
you know...around...

809 Posts

Quote:
 Originally Posted by sascha77 No. This is false. set p=11 ->$n=2^{p}-1 = 2047$ for this: $(2^{11}+2^{1})^{2046} \equiv (\;(2^{11} + 2^{1})\;mod(\;2047)\;)^{2046} \equiv 3^{2046} \equiv 1013\;(mod\; 2047)$
Oops, sorry. Messed up 1 with 21

 2011-03-04, 19:07 #17 sascha77     Jan 2010 germany 2·13 Posts I noticed that my first post in this topic was mathematically not detailled enough and I forgot to mention some assumptions. (Especially that p must always be prime) For this reason I redefine my previous post: $(2^a+2^b)^{n} \equiv 2^a+2^b\;(mod \;n)$ $n=2^{p}-1$ WITH $p$ is prime !!! $a \in N\; and\; b \in N.$ A.) let n be prime with n=2^p-1: if $n$ is prime then for every $a$ and $b$ the congruence is true. -------------------------------------------------------------------- B.) Let n be not prime with n=2^p-1 (But p is prime): B.1.) If you choose $a=b$ when the above congruence is always true. B.2.) If you choose $a$ and $b$ so that $|b-a|\equiv p\;(mod \;n)$ when the congruence is also always true. B.3) But for the other combinations of $a$ and $b$ the above congruence is always false. (A) (B.1) and (B.2) can easily be proven. But (B.3) is hard to prove. Therefore is (B.3) my conjecture. ----------------------------------------------------------------- ************************************************** Proof of A: This is trivial, because A follows directly from the "Fermatsche Satz". ************************************************** ************************************************** proof of B.1: $(2^x)^{p} \equiv 1 \;(mod\; n)$ is always true. This is because 2 has always the order $p$ in $Z/Z_{(2^{p}-1)}$ with $p$ prime. $2^p\equiv1\;(mod\;2^{p}-1)$ -> for every $x$ you have: $(2^{x})^{p}\equiv1\;mod(2^{p}-1)$ Because: $(2^{x})^{p}=(2^{p})^{x}\equiv1^{x}\equiv1\;(mod \;2^{p}-1)$ Now we look at the variable $n$: $n = 2^{p}-1 = (2*p*k+1)$ (This is because of the factorisation of the form 2^{p}-1) -> $(n-1) \equiv 0 \; (mod\; p)$ for every $x$ you have now: $(2^{x})^{n-1}\equiv1\;(mod\;n)$ --> $ (2^{x})^{n}\equiv2^{x} \;(mod\; n)$ Therefore: when you choose $a$ and $b$ so that $a=b$ then you have: ${(2^{a}+2^{a})}^{n} = {(2^{(a+1)})}^{n} \equiv 2^{a+1}\equiv 2^{a}+2^{b}\;mod\; (n)$ ************************************************** ************************************************** proof of B.2: If you choose $a$ and $b$ so that $|b-a|\equiv p\;(mod\;n)$ then $b$ is $b=(a+p*k)$ with $k\in N$. -> $(2^{a} + 2^{b})^{n}\equiv (2^{a} + 2^{(a+p*k)})^{n}\equiv ({2^{a}}+{2^{a}}*{2^{(p*k)}})^{n}\equiv (2^{a}*2^{a}*1)^{n}\equiv(2^{a+1})^{n}\equiv 2^{(a+1)} \;(mod\; n )$ ************************************************** Last fiddled with by sascha77 on 2011-03-04 at 19:50
 2011-03-04, 19:42 #18 mart_r     Dec 2008 you know...around... 32916 Posts Deployed some Pari code: forprime(p=67,83,print(p);n=2^p-1;for(a=2,999,for(b=0,a-1,x=2^a+2^b;c=x;for(i=1,p-2,c=(c^2*x)%n);c=(c^2)%n;if(c==1&&(a-b)%p<>0,print("counterexample found: a="a", b="b))))) [The forprime-range is to be set manually after every Mp=prime, e.g. next it would be forprime(p=97,103,...] No counterexample for a<1000, b
2011-03-04, 20:00   #19
sascha77

Jan 2010
germany

328 Posts

Quote:
 Originally Posted by mart_r Deployed some Pari code: forprime(p=67,83,print(p);n=2^p-1;for(a=2,999,for(b=0,a-1,x=2^a+2^b;c=x;for(i=1,p-2,c=(c^2*x)%n);c=(c^2)%n;if(c==1&&(a-b)%p<>0,print("counterexample found: a="a", b="b))))) [The forprime-range is to be set manually after every Mp=prime, e.g. next it would be forprime(p=97,103,...] No counterexample for a<1000, b

Thanks !!!
Yes it could be that there exist a counterexample.
But nobody knows this until it is found. ;-)
A hint: You only need to test a and b to the size of p.
this means: test a for a<=p and b for b<=p
Because of the modulo-operation these values of 2^a repeat after p-steps.

 2011-03-04, 20:28 #20 mart_r     Dec 2008 you know...around... 14518 Posts Fair enough. So, no counterexamples for p<=353. Stopping here. Someone with a faster PC, i.e. with more than one core, could check further.
2011-03-04, 20:53   #21
R.D. Silverman

"Bob Silverman"
Nov 2003
North of Boston

2×3×29×43 Posts

Quote:
 Originally Posted by sascha77 Thanks !!! Yes it could be that there exist a counterexample. But nobody knows this until it is found. ;-) A hint: You only need to test a and b to the size of p. this means: test a for a<=p and b for b<=p Because of the modulo-operation these values of 2^a repeat after p-steps.
You are looking at the intersection of two sparse sets (false witnesses
to 2^p-1 and integers with Hamming weight 2) and hoping that the
intersection isn't empty.

There are no analytic tools available to approach the problem because
[AFAIK] there is almost nothing known about how false witnesses
are distributed mod P. It is easy to get a sharp counting function for
weight-2 integers up to B , but their distribution is clearly not uniform.

Heuristics based on probabilistic methods are likely to fail, because
the sets involved are not uniformly distributed.

Even if the result is true, it has almost no applicability anyway. LL will
be faster.

 2011-03-07, 23:53 #22 Batalov     "Serge" Mar 2008 Phi(4,2^7658614+1)/2 26D616 Posts Unsurprisingly, there were no counterexamples up to p<1450. A modified one-liner forprime(p=2,3000,if(!isprime(n=2^p-1),print(p);for(a=1,p-1,for(b=0,a-1,x=2^a+2^b;c=x;for(i=3,p,c=(c^2*x)%n);if((c^2)%n==1,print("found: a="a", b="b)))))) can run without need to skip prime Mp's and can run forever lazily... ____ A bit faster: forprime(p=2,3000,if(!isprime(n=2^p-1),print(p);for(a=1,p-1,for(b=0,a-1,x=(2^a+2^b)%n;x2=(x^2)%n;c=x;for(i=1,p,c=(c^2)%n);if(c==x2,print("found: a="a", b="b)))))) ...Is there a better mod exponent in Pari? Mod(2^a+2^b,n)^n ? Last fiddled with by Batalov on 2011-03-08 at 00:09 Reason: (not a master of Pari, I am)

 Similar Threads Thread Thread Starter Forum Replies Last Post aketilander Operazione Doppi Mersennes 1 2012-11-09 21:16 Thiele Math 18 2010-05-23 05:35 kurtulmehtap Math 12 2010-05-03 14:02 arithmeticae Lounge 5 2008-10-27 06:15 T.Rex Math 12 2005-09-12 07:56

All times are UTC. The time now is 18:52.

Wed Oct 5 18:52:37 UTC 2022 up 48 days, 16:21, 0 users, load averages: 1.21, 1.28, 1.24


text:
Title Author Keyword ::: Volume ::: Vol. 27Vol. 26Vol. 25Vol. 24 ::: Issue ::: No. 6No. 5No. 4No. 3No. 2No. 1

Approaches to Reduce the Contact Resistance by the Formation of Covalent Contacts in Graphene Thin Film Transistors

Youngeun Naa, Jaehyun Hanb,c, and Jong-Souk Yeoa,b,c,*

aIntegrated Science and Engineering Division, Yonsei University, 162-1 Songdo-dong, Yeonsu-gu, Incheon 406-840, Republic of Korea, bSchool of Integrated Technology, Yonsei University, 162-1 Songdo-dong, Yeonsu-gu, Incheon 406-840, Republic of Korea, cYonsei Institute of Convergence Technology, Yonsei University, 162-1 Songdo-dong, Yeonsu-gu, Incheon 406-840, Republic of Korea
Correspondence to: E-mail: jongsoukyeo@yonsei.ac.kr
Received June 22, 2017; Revised July 29, 2017; Accepted July 30, 2017.
This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by-nc/4.0) which permits unrestricted non-commercial use, distribution, and reproduction in any medium, provided the original work is properly cited.
Abstract

Graphene, with a carrier mobility achieving up to 140,000 cm2/Vs at room temperature, makes it an ideal material for application in semiconductor devices. However, when the metal comes in contact with the graphene sheet, an energy barrier forms at the metal-graphene interface, resulting in a drastic reduction of the carrier mobility of graphene. In this review, the various methods of forming metal-graphene covalent contacts to lower the contact resistance are discussed. Furthermore, the graphene sheet in the area of metal contact can be cut in certain patterns, also discussed in this review, which provides a more efficient approach to forming covalent contacts, ultimately reducing the contact resistance for the realization of high-performance graphene devices.

Keywords : Graphene, Carrier mobility, Contact resistance, Covalent contacts, Patterning
I. Introduction

Ever since the discovery of the exceptional optical [13], electrical [46], mechanical [7,8], and thermal [9,10] properties of graphene, it was immediately applied to the areas such as transparent electrodes [1113], photovoltaic devices [14,15], and electrochemical sensors [16]. Also, the application areas include graphene transistors [1719] since graphene has a high carrier mobility of up to 140,000 cm2/Vs at room temperature [20]. Because of the high carrier mobility of graphene, it should ideally have exceptional device performance. However, the two-dimensional material experiences a severe drop in its carrier mobility when realized as the semiconductor channel layer because experimental graphene exhibits several problems that strays it from ideal graphene. Some of those problems are the presence of defects and impurities in the lattice [21], the presence of wrinkles in the sheet [22,23], its interaction with the substrate [24,25], and the presence of photoresist residues [26,27] from imperfect photoresist etching during device fabrication. Because already various effects exist that reduce the mobility, a further decrease should be prevented to take advantage of graphene’s exceptional transport properties.

However, the carrier mobility is further reduced during metallization, when the metal electrodes are deposited. The decrease in the mobility is due to the energy barrier that exists at the metal-graphene interface, where the metal comes in contact with the graphene. Hence, contact resistance forms at the interface, which lowers device performance. Contact resistance forms due to the presence of π-bonds in the z-direction in the graphene lattice from the sp2 hybridization of graphene, the bonds which restrict the metal from strongly binding to the semiconductor sheet during metallization. Hence, when the metal is deposited on graphene using a top-contact mechanism, the metal binds onto the underlying sheet with large coupling length via van der Waals forces because of the presence of the stable π-bonds [28]. The weak adhesion of the metal to the graphene results in the formation of an energy barrier at the interface, which limits carrier transfer and hence lowers the carrier mobility of the device, all effects of contact resistance.

Thus, to realize high-performance graphene devices, contact resistance must be reduced. Throughout the years of graphene research, researchers have discovered various methods to reduce the contact resistance, including work-function engineering [29,30], ultraviolet ozone treatment [31,32], alteration of the device geometry [33,34], and improvement of the surface roughness of graphene [35]. However, these methods are all approaches to strengthen the metal adhesion to the graphene sheet while the device is in a top-contact structure, which is still limited by the weak van der Waals forces at the metal-graphene interface. So, a better approach would be to overcome the energy barrier by eliminating those limiting forces.

That very approach is the formation of metal-graphene covalent contacts at the interface of the device. Covalent contacts are the covalent bonding of the metal to the graphene sheet, and they are made possible by removing a carbon atom from the graphene lattice, exposing dangling σ-bonds to which the metal can bind. Thus, in covalent contacts, because the metal no longer binds to the graphene through van der Waals forces as in top contacts, a shorter bonding distance with large orbital overlap results [20]. By such, the energy barrier at the metal-graphene interface is lowered, and electrons from the metal electrodes can transfer more efficiently to the graphene channel via overlapping orbitals. Consequently, the transmission efficiency (TE) of the carriers is increased, and the contact resistance (RC) is decreased, as shown in Equation 1:

$1RC=4q2h∫-∞∞dETEFT(E-μ)$

where FT is the thermal broadening function, E is the electron energy, and μ is the chemical potential [36]. The contact resistances are generally measured using a transmission line method (TLM), method, in which the channel lengths of the devices vary to obtain a TLM graph that is composed of the resistance values between each metal-semiconductor contact. The contact resistance value can be extracted from Equation 2 below:

$Rtotal=2RCW+ρL[Ω]$

where RC is the contact resistance, W is the channel width, L is the channel length, and r is the channel resistivity [28]. Hence, from the graph of the total resistance versus channel length, since the y-intercept of the graph is twice RC, the contact resistance in the unit can be calculated easily. To obtain the units of Ω·μm, the value is multiplied by the channel width.

In this review, the different methods of forming covalent contacts, from the formation of defects by particle irradiation, annealing, formation of edge contacts, to patterning, are reviewed. Additionally, since covalent contacts are crucial for the lowering of the energy barrier by providing orbital hybridization and for reducing the contact resistance at the metal-graphene interface, the resulting contact resistances gathered from the different methods are also reviewed. Finally, this review also provides the limitations of each method of forming covalent contacts.

II. Formation of Defects by Particle Irradiation

In order to create unstable dangling carbon bonds in the graphene lattice for metal-graphene covalent bonding, the carbon atoms are removed by particle irradiation, creating defect sites, or vacancies. When high-energy particles collide with the carbon atoms of graphene, they transfer energy to the target atoms, allowing them to acquire sufficient energy for their extraction from the lattice site [37,38]. Fig. 1(a) shows a graphene lattice with a missing carbon, which has been ejected by proton irradiation. This type of defect site is called an unreconstructed monovacancy [39], in which the dangling bonds do not bond with each other and remain free. Thus, with defects induced in the lattice, these free dangling bonds remain for the covalent bonding to the metals. As a result, covalent contacts can be formed at the defect sites, thereby reducing the contact resistance. The improvement in device performance has been shown by Meersha et al., where a metal-graphene contact resistance of 700 Ω·μm is obtained from a CVD-grown graphene device under Ar ion bombardment at an exposure time of 20 s [40].

Another example is the “gentle” low-power O2 plasma treatment of the device for the creation of defects on the graphene site. O2 plasma treatment is the exposure of the target to a high-energy O2 plasma, a process much similar to particle irradiation. Except, in this case, when the O2 plasma hits, the oxygen molecules bond with the carbon atoms of graphene and form CO2 molecules as a byproduct, as well as C-O bonds in the graphene sheet in place of C-C bonds. Thus, during metallization, the metals are able to chemically bond with the oxygen atoms and ultimately form C-M bonds. Consequently, covalent contacts are achieved at the metal-graphene interface. Using this mechanism, Robinson et al. found that increasing the O2 plasma treatment time up to 90 s improved the specific contact resistance due to the creation of the defect sites that lead to covalent bonding of the metal to the underlying graphene [41].

However, the downside to these techniques is the introduction of too many defects into the graphene lattice, which can occur if the sheet is exposed to the high-energy source for too long. Because defects are randomly distributed when formed by particle irradiation of the target over large areas, and because they are more likely to be generated in already-existing vacancies due to increased strain in those areas [42], there is a risk of over-generating defects in the lattice. Defects impede carrier transfer because they scatter electrons. Hence, when there are too many vacancies in the graphene site, too much scattering occurs. From the previous example, Meersha et al. also showed that with an increase in Ar ion irradiation time, an upturn in the contact resistance graph was shown, where the contact resistance first decreased and then increased; and Robinson et al. discovered that an exposure time of over 90 s resulted in a higher specific contact resistance. Ultimately, the contact resistance increases when defects dominate. Because particle irradiation leads to an upturn in the contact resistance beyond the optimal exposure time due to the eventual creation of too many defects into the graphene lattice, it is not an efficient approach to lowering the contact resistance of the device.

III. Formation of Covalent Contacts by Annealing

Annealing previously has been known to improve metal-graphene adhesion by removing surface contaminants at the interface. For instance, Lin et al. discovered that annealing the graphene surface at 200 °C for 2 h decomposed the PMMA residues that remained from imperfect PMMA etching [43]. However, it has been discovered thereafter that annealing the graphene while it is in contact with the metal results in the formation of covalent contacts by dissolving the carbon atoms in the graphene lattice. The carbon atoms can be dissolved when in contact with certain metals, like Ni, Pd, and Ti, due to chemisorption at the interface, where the metal’s d-orbitals and graphene’s π-orbitals become hybridized, resulting in a strong interaction [44]. Thus, when the graphene is annealed while in contact with the metals that allow for chemisorption, the chemical reaction of the graphene and the Ni is enhanced, so carbon atoms dissolve into the metal, leaving behind vacancies. Fig. 1(b) shows the formation of unreconstructed monovacancies from annealing the device. During metallization, covalent contacts are formed at the vacant sites, whereas top contacts are formed in the remaining areas. The phenomenon of carbon dissolution due to annealing was explained by Leong et al. in their study on the effect of annealing on metal-graphene interfaces [45]. Annealing their Ni-contacted graphene device at 300 °C for 1 h showed a much higher D-band Raman intensity than just annealed graphene and Ni-contacted graphene without anneal, which correlates to the carbon dissolution.

Additionally, Leong et al. in a prior experiment described the annealing phenomenon in terms of metal etching of the graphene [46]. As a result of annealing their Ni-contacted graphene device at 580 °C for 0.5 h, pits in the graphene sheet were etched by the Ni that became isolated into small particles. By etching the graphene, the dangling bonds became exposed at the etched sites; so, the pits became areas of covalent contacts. Fig. 1(c) shows the device schematic, where the Ni electrodes are deposited on top of the annealed structure. The newly-deposited Ni is in covalent contact with graphene in the etched areas and top contact in the others. As expected, annealing showed an improvement in the device performance, with a contact resistance of 89 Ω·μm with treatment compared to that of 294 Ω·μm without treatment.

However, both experiments by Leong et al. showed that extending the annealing time does not further reduce the contact resistance significantly. This is simply due to the nature of graphene, as defects in the sheet, as well as the area of graphene, limit the amount of dangling bonds that can be formed.

IV. Formation of Edge Contacts by O2 Plasma Treatment

So far, the formation of covalent contacts by high-energy and high-temperature means has shown to reduce the contact resistance of the graphene device, but only up to the optimal exposure time or temperature. Because finding the optimal condition in each case for device fabrication is troublesome, researchers have looked for new ways to achieve covalent contacts. Of those researchers, Wang et al. has discovered a new contact geometry, where the metals bind to the graphene just at its edge [20]. This type of contact geometry leads to a type of metal-graphene covalent contact called one-dimensional or edge contacts, where the metals are bonded to the graphene just at the edge of the graphene sheet. In order to achieve these contacts, the graphene sheet is first encapsulated in boron nitride in a BN/graphene/BN heterostructure before the plasma-etching of the edges at opposing sides; then, the metal is deposited just at the exposed edges by electron beam evaporation for the successful formation of metal-graphene edge contacts. Fig. 2 shows the device structure, where the metal electrodes are in contact with the heterostructure just at its edge. The resulting performance of this device is exceptional, with a room-temperature mobility of 140,000 cm2/Vs and a contact resistance of about 150 Ω·μm at large carrier densities, which, at its time, was about 25% lower than the value achieved by the device in traditional top-contact configuration [20].

However, because of the complexity of the heterostructure, the efficiency of this device fabrication is not great. Conversely, Yue et al. has discovered a method utilizing O2 plasma treatment to create edge contacts without the need for the complex heterostructure [28]. By etching graphene in the areas for the metals to be deposited, edge contacts can be achieved. Fig. 3 shows the schematic of etching the graphene via O2 plasma treatment for the creation of edge contacts. In Fig. 3(a), when graphene is exposed to the treatment for over 5–10 s and under 35 s, the area of the graphene that is not protected by the photoresist becomes etched, and the exposed length, Lexposed, becomes shorter; hence, if the metal were deposited, a complete edge contact would not be achieved, as there would be graphene remaining under the deposited metal. In Fig. 3(b), however, edge contacts are achieved when graphene is exposed to the treatment for over 35 s and under 45 s, since the graphene in the area for metal to be deposited is completely etched. Thus, when the metal is deposited, it covalently bonds to the graphene at its edge, resulting in orbital hybridization at the interface. Additionally, due to the faster carrier transfer from the shorter bonding distance achieved by edge contacts, the device showed its best contact resistance of 270 Ω·μm at room temperature when exposed for 45 s. Yet, since the O2 plasma treatment creates defects, as do particle irradiation, optimal exposure time must again be considered for the best device performance yield. In the aforementioned study, an exposure time over 45 s has led to over-etching of graphene, in which metal-graphene contact was decreased, and an exposure time under 5 s has led to under-etching, in which not enough covalent contacts were formed for a significant decrease in the contact resistance.

Chen et al. has expanded on this O2 plasma mechanism of creating edge contacts by etching the graphene sheet and directly growing MoS2 via CVD for the fabrication of a device geometry in which graphene acted as the electrodes [47]. Thus, by this mechanism, the interface contains graphene and another two-dimensional material rather than a three-dimensional metal. Previously, it has shown that CVD growth of MoS2 is possible on SiO2 substrate [48,49], yet this method has not been used before for the implementation of MoS2 in edge-contact geometry to graphene. To fabricate this graphene-MoS2 heterojunction-based FET device, O2 plasma treatment is used to etch away the graphene sheet only at the center before CVD-growth of MoS2. As a result, the MoS2 layer grows at the exposed center on the SiO2 and forms the channel, and the graphene at the opposite ends becomes the electrodes, as shown via optical image in Fig. 4(a) and via schematic illustration in Fig. 4(b). Although this device showed typical electrical performances of n-type devices, the field-effect mobility of only about 0.46 cm2/Vs was obtained due to the small grain size of MoS2. Even with poor device performance, this approach still has the potential for improvement since O2 plasma treatment was used for the fabrication of a more advanced device geometry that utilizes electrode-channel edge contacts.

V. Patterning the Graphene at the Device Interface

Covalent contacts can also exist under the area of metal-graphene contact, rather than only at the edges of graphene. This contact geometry is achieved by directly patterning the graphene sheet in the areas where the metal will later be deposited. Patterning is done by exposing certain areas of graphene to O2 plasma in order to etch graphene in a specific pattern for the reduction of contact resistance via covalent contacts. Although various device patterns are possible for fabrication, this review will focus on the holes, comb, rail, and snake patterns. Song et al. etched holes, or antidot arrays, of varying radii in the graphene sheet under the metal-graphene contact area using O2 plasma treatment [50]. Fig. 5(a) shows the schematic of the device, where graphene lies under the metals, except in the areas of the holes, which are etched. At the etched sites, the metal is able to covalently bond with the graphene via the dangling σ-bonds that exist at the perimeter of the holes, shown as the blue dots; at the areas outside of the holes, however, the metal binds to the graphene via van der Waals forces. Hence, both top contacts and covalent contacts exist simultaneously for patterned devices. The holes are more accurately shown in Fig. 5(b), where they are evenly-distributed at the interface of the device. Again, by etching the graphene in certain patterns, the metal is able to bind more strongly to the underlying graphene, thereby lowering the energy barrier at the patterned areas and resulting in a more efficient carrier transfer. In the study, a contact resistance of around 250 Ω·μm was obtained for the devices with holes of 0.38 μm radius, compared to around 650 Ω·μm for the devices without holes. Further, Passi et al. also etched holes in their devices using O2 plasma treatment [51]. With a stronger metal adhesion to the graphene sheet from covalent contacts at the areas of the holes, a contact resistance of 456 Ω·μm was obtained for the device with holes of 500 nm when distributed evenly under the entire contact area, an improvement from 1518 Ω·μm for the devices without holes. However, this device pattern does not provide enough areas for covalent contacts for a more significant reduction of the contact resistance. So, other device patterns that allow for more covalent contacts should be utilized.

More efficient cuts can be made using the comb pattern, shown in Fig. 6(a) and (b), where parts of the graphene sheet, shown in dark gray, is cut in one end using a similar O2 plasma etching process. Cho et al. fabricated this pattern to study the dependence of device performance on the peripheral length of graphene [52]. The peripheral length of graphene was increased by increasing the number of cuts, which yielded more dangling bonds bonds at the perimeter of graphene for the formation of covalent contacts at the interface. As the peripheral length increased from 312 mm to 792 μm, a 60% decrease in the contact resistance was shown, and a value of 0.8 kΩ·μm was obtained. This result proves that inducing more cuts improves the strength of the metal-graphene contact for a more efficient device performance.

A pattern similar to the comb geometry is the rail pattern, in which horizontal cuts, shown as light gray, are made in the middle of the graphene sheet, shown as dark gray, at the metal contact area as shown in Fig. 6(c). Hence, dangling bonds exist at the perimeter of the cuts, where the metal can bind covalently. It is notable that the cuts are not extended to the end of graphene, which would result in a comb pattern. Smith et al. fabricated the rail-patterned graphene device using different number of cuts to increase the perimeter length of graphene for their study on the device performance based on the amount of cuts made [53]. Their TLM measurements yielded a contact resistance of 125 Ω·μm post-anneal with 10 cuts under Cu contact, compared to 184 Ω·μm post-anneal without any patterns, which proves that the patterns provide a better device performance via covalent contacts. This proof is shown as the device schematic in Fig. 6(d), where covalent contacts only exist at the edge of the cut areas, providing a fast carrier injection from the metal to the underlying graphene due to a shorter bonding distance. Furthermore, their study showed that as the perimeter length increased, more areas of graphene become available for covalent contacts, and a decrease in the total resistance of the device post-anneal was first seen. Yet, as the number of cuts increased beyond 8, an upturn of the resistance was shown because extreme narrowing of the width of the graphene nanoribbons by making too many cuts had led to quantization effects that impeded carrier transfer at the interface [53]. Because this pattern works best under optimal conditions, in which the perimeter length is kept as large as possible while maintaining a large enough graphene nanoribbon width, a significant limitation exists for this device pattern.

Another type of pattern geometry is the snake pattern, where horizontal cuts are made to connect the long vertical cuts in a snake-like fashion as shown in Fig. 7(a). Park et al. fabricated this pattern on the graphene sheet at the interface of the device, and when the width of the gap between the cut graphene nanoribbons was decreased to 1 μm, a contact resistance of 484 Ω·μm under Pd contact was obtained [54], compared to 1.4 Ω·μm without patterning. Again, the reduction in the contact resistance is due to the dangling bonds that exist at the etched areas, as shown in Fig. 7(b), resulting in covalent contacts at the interface.

VI. Conclusions

This review has discussed the different methods of forming covalent contacts for the reduction of the contact resistance, essentially to realize high-performance graphene transistors. Defects in the graphene sheet created by particle irradiation provide dangling bonds for metal-graphene covalent bonding at the interface of the defect sites. Additionally, annealing enhances the chemical reaction at the chemisorption interfaces and results in the dissolution of the carbon atoms to the metal, as well as a strong orbital hybridization.

This review has also discussed the reduction of the contact resistance by altering the contact geometry of the device. By depositing the metal just at the edge of the graphene layer, edge contacts are achieved that provides covalent bonding of the metal to the graphene. Furthermore, patterning the graphene at the interface strengthens the metal adhesion through covalent contacts provided by the etched areas.

The contact resistance values obtained by the various methods of forming covalent contacts are summarized in Table 1. It is conclusive that covalent contacts are fundamental for the reduction in the contact resistance and the realization of high-performance graphene-based transistors.

Acknowledgements

This research was supported by the MSIT (Ministry of Science and ICT), Korea, under the ICT Consilience Creative program (IITP-2017-2017-0-01015) supervised by the IITP (Institute for Information & communications Technology Promotion) and also under the “Mid-career Researcher Program” (NRF-2016R1A2B2014612) supervised by the NRF (National Research Foundation).

Figures
Fig. 1. (a) Schematic representation of an unreconstructed monovacancy in the graphene lattice. (b) Vacant sites created in the graphene sheet from the dissolution of carbon atoms into the metal due to annealing. The metal is one that allows for chemisorption at the interface. (c) Ni electrodes deposited on top of the previous structure, which contains etched pits from annealing the previous Ni-graphene device. (Part a reprinted with permission from 38, copyright © 2017 Royal Society of Chemistry. Part b reprinted (adapted) with permission from 44, copyright © 2017 American Chemical Society. Part c reprinted (adapted) with permission from 45, copyright © 2017 American Chemical Society.)
Fig. 2. Edge contact of the metal to the BN/graphene/BN heterostructure. The three-dimensional metal is in contact with the two-dimensional graphene just at its edge. (Reprinted with permission from 20, copyright © 2017 The American Association for the Advancement of Science.)
Fig. 3. O2 plasma treatment of graphene to etch the material for the creation of edge contacts. Treatment times are (a) 5–10 s to 35 s, where the shortening of the exposed graphene contact length (Lexposed) is seen; and (b) 35 s to 45 s, where the exposed graphene is completely etched. (Parts a and b reprinted with permission from 46, copyright © 2017 Royal Society of Chemistry.)
Fig. 4. Graphene-MoS2 heterojunction-based, back-gate FET device shown (a) under an optical microscopy and (b) as a schematic illustration, both showing edge contacts of MoS2 channel layer to the graphene electrodes. (Parts a and b reprinted with permission from 47, copyright © 2017 Royal Society of Chemistry.)
Fig. 5. (a) Device schematic, in which the holes are etched only in the areas of metal contact. Covalent contacts are achieved at the perimeter of the holes, and top contacts exist in the remaining areas. (b) Schematic of the hole pattern of the graphene device, in which the holes are arranged evenly under the contact area. Lm is the length of the metal, W is the width of graphene, and rh is the hole radius. (Parts a and b reprinted with permission from 50, copyright © 2017 AIP Publishing LLC.)
Fig. 6. Comb pattern of the graphene device, in which the peripheral lengths are (a) 312 and (b) 472 μm, respectively. The patterns are made under the metal contact areas, where covalent contacts occur at the edges of the cuts. (c) and (d) Rail pattern of the graphene device, in which the cuts, shown as light gray in the inset, are made under the source and drain areas. Covalent contacts are achieved via dangling bonds at the perimeter of the cuts, whereas top contacts exist in the areas that have not been etched. (Parts a and b reprinted with permission from 52, copyright © 2017 AIP Publishing LLC; and parts c and d reprinted with permission from 53, copyright © 2017 American Chemical Society.)
Fig. 7. (a) Snake pattern of the graphene device, where LT_1D is the effective transfer length of the etched area, and LT_2D is the effective transfer length of the surface area. (b) Dangling bonds exist at the edges of the etched area of the graphene lattice, shown in cyan, whereas no dangling bonds exist at the surface of the graphene, shown in pink. (Parts a and b reprinted with permission from 54, copyright © 2017 John Wiley and Sons.)
Tables

Summary of the contact resistances obtained before and after using various methods per strategies for graphene-based transistors

StrategyMethodContact resistance before (O-nm)Contact resistance after (Ω·μm)Reference
DefectsAT bombardment305070040
AnnealingEtched pits2948946
Edge contactsBN/graphenc/BN heterostrucoire*15020
PatterningO2 plasma treatment476220728
Holes151845651
Comb*80052
Rail18412553
Snake140048454

The contact resistance values for the devices before the treatments were not studied.

References
1. Bonaccorso, F, Sun, Z, Hasan, T, and Ferrari, AC (2010). Nat Photon. 4, 611.
2. Nair, RR, Blake, P, Grigorenko, AN, Novoselov, KS, Booth, TJ, Stauber, T, Peres, NM, and Geim, AK (2008). Science. 320, 1308.
3. Prezzi, D, Varsano, D, Ruini, A, Marini, A, and Molinari, E (2008). Phys Rev B. 77, 041404.
4. Neto, AC, Guinea, F, Peres, NM, Novoselov, KS, and Geim, AK (2009). Rev Mod Phys. 81, 109.
5. Novoselov, KS, Morozov, SV, Mohinddin, TM, Ponomarenko, LA, Elias, DC, Yang, R, Barbolina, II, Blake, P, Booth, TJ, Jiang, D, Giesbers, J, Hill, EW, and Geim, AK (2007). Phys Status Solidi B. 244, 4106.
6. Novoselov, KS, Geim, AK, Morozov, SV, Jiang, D, Katsnelson, MI, Grigorieva, IV, Dubonos, SV, and Firsov, AA (2005). Nature. 438, 197.
7. Lee, C, Wei, X, Kysar, JW, and Hone, J (2008). Science. 321, 385.
8. Ding, F, Ji, H, Chen, Y, Herklotz, A, Dörr, K, Mei, Y, Rastelli, A, and Schmidt, OG (2010). Nano Lett. 10, 3453.
9. Ghosh, S, Calizo, I, Teweldebrhan, D, Pokatilov, EP, Nika, DL, Balandin, AA, Bao, W, Miao, F, and Lau, CN (2008). Appl Phys Lett. 92, 151911.
10. Balandin, AA, Ghosh, S, Bao, W, Calizo, I, Teweldebrhan, D, Miao, F, and Lau, CN (2008). Nano Lett. 8, 902.
11. Kim, KS, Zhao, Y, Jang, H, Lee, SY, Kim, JM, Kim, KS, Ahn, JH, Kim, P, Choi, JY, and Hong, BH (2009). Nature. 457, 706.
12. Bae, S, Kim, H, Lee, Y, Xu, X, Park, JS, Zheng, Y, Balakrishnan, J, Lei, T, Kim, HR, Song, YI, Kim, YJ, Kim, KS, Özyilmaz, B, Ahn, JH, Hong, BH, and Iijima, S (2010). Nat Nanotechnol. 5, 574.
13. Han, J, Lee, JY, and Yeo, JS (2016). Carbon. 105, 205.
14. Wang, Y, Chen, X, Zhong, Y, Zhu, F, and Loh, KP (2009). Appl Phys Lett. 95, 209.
15. Shen, J, Zhu, Y, Yang, X, and Li, C (2012). Chem Commun. 48, 3686.
16. Shao, Y, Wang, J, Wu, H, Liu, J, Aksay, IA, and Lin, Y (2010). Electroanalysis. 22, 1027.
17. Schwierz, F (2010). Nat Nanotechnol. 5, 487.
18. Meric, I, Han, MY, Young, AF, Ozyilmaz, B, Kim, P, and Shepard, KL (2008). Nat Nanotechnol. 3, 654.
19. Xia, F, Farmer, DB, Lin, Y-m, and Avouris, P (2010). Nano Lett. 10, 715.
20. Wang, L, Meric, I, Huang, PY, Gao, Q, Gao, Y, Tran, H, Taniguchi, T, Watanabe, K, Campos, LM, Muller, DA, Guo, J, Kim, P, Hone, J, Shepard, KL, and Dean, CR (2013). Science. 342, 614.
21. Carr, LD, and Lusk, MT (2010). Nature Nanotechnol. 5, 316.
22. Zheng, Q, Geng, Y, Wang, S, Li, Z, and Kim, JK (2010). Carbon. 48, 4315.
23. Wang, C, Liu, Y, Lan, L, and Tan, H (2013). Nanoscale. 5, 4454.
24. Sutter, P, Sadowski, JT, and Sutter, E (2009). Phys Rev B. 80, 245411.
25. Zhou, SY, Gweon, GH, Fedorov, A, First, P, De Heer, W, Lee, DH, Guinea, F, Neto, AC, and Lanzara, A (2007). Nat Mater. 6, 770.
26. Ishigami, M, Chen, JH, Cullen, WG, Fuhrer, MS, and Williams, ED (2007). Nano Lett. 7, 1643.
27. Pirkle, A, Chan, J, Venugopal, A, Hinojos, D, Magnuson, CW, McDonnell, S, Colombo, L, Vogel, EM, Ruoff, RS, and Wallace, RM (2011). Appl Phys Lett. 99, 122108.
28. Yue, DW, Ra, CH, Liu, XC, Lee, DY, and Yoo, WJ (2014). Nanoscale. 7, 825.
29. Giovannetti, G, Khomyakov, P, Brocks, G, Karpan, VM, van den Brink, J, and Kelly, PJ (2008). Phys Rev Lett. 101, 026803.
30. Nagashio, K, and Toriumi, A (2011). Jpn J Appl Phys. 50, 070108.
31. Chen, CW, Ren, F, Chi, GC, Hung, SC, Huang, YP, Kim, J, Kravchenko, II, and Pearton, SJ (2012). J Vac Sci Technol B. 30, 060604.
32. Li, W, Liang, Y, Yu, D, Peng, L, Pernstich, KP, Shen, T, Hight Walker, AR, Cheng, G, Hacker, CA, Richter, CA, Li, Q, Gundlach, DJ, and Liang, X (2013). Appl Phys Lett. 102, 183110.
33. Hong, SK, Song, SM, Sul, O, and Cho, BJ (2013). Carbon Lett. 14, 171.
34. Franklin, AD, Han, SJ, Bol, AA, and Perebeinos, V (2012). IEEE Electron Device Lett. 33, 17.
35. Hsu, A, Wang, H, Kim, KK, Kong, J, and Palacios, T (2011). IEEE Electron Device Lett. 32, 1008.
36. Gao, Q, and Guo, J (2014). APL Mater. 2, 056105.
37. Krasheninnikov, A, and Banhart, F (2007). Nat Mater. 6, 723.
38. Han, J, Lee, JY, Choe, J, and Yeo, JS (2016). RSC Adv. 6, 76273.
39. Lehtinen, O, Tsai, IL, Jalil, R, Nair, RR, Keinonen, J, Kaiser, U, and Grigorieva, IV (2014). Nanoscale. 6, 6569.
40. Meersha, A, Variar, HB, Bhardwaj, K, Mishra, A, Raghavan, S, Bhat, N, and Shrivastava, M (2016). IEEE IEDM, 5.3.1.
41. Robinson, JA, LaBella, M, Zhu, M, Hollander, M, Kasarda, R, Hughes, Z, Trumbull, K, Cavalero, R, and Snyder, D (2011). Appl Phys Lett. 98, 053103.
42. Banhart, F, Kotakoski, J, and Krasheninnikov, AV (2010). ACS Nano. 5, 26.
43. Lin, YC, Lu, CC, Yeh, CH, Jin, C, Suenaga, K, and Chiu, PW (2011). Nano Lett. 12, 414.
44. Gong, C, Lee, G, Shan, B, Vogel, EM, Wallace, RM, and Cho, K (2010). J Appl Phys. 108, 123711.
45. Leong, WS, Nai, CT, and Thong, JT (2014). Nano Lett. 14, 3840.
46. Leong, WS, Gong, H, and Thong, JT (2013). ACS Nano. 8, 994.
47. Chen, X, Park, YJ, Das, T, Jang, H, Lee, JB, and Ahn, JH (2016). Nanoscale. 8, 15181.
48. Lee, YH, Zhang, XQ, Zhang, W, Chang, MT, Lin, CT, Chang, KD, Yu, YC, Wang, JTW, Chang, CS, Li, LJ, and Lin, TW (2012). Adv Mater. 24, 2320.
49. Yu, Y, Li, C, Liu, Y, Su, L, Zhang, Y, and Cao, L (2013). Sci Rep. 3, 1866.
50. Song, SM, Kim, TY, Sul, OJ, Shin, WC, and Cho, BJ (2014). Appl Phys Lett. 104, 183506.
51. Passi, V, Gahoi, A, Ruhkopf, J, Kataria, S, Vaurette, F, Pallecchi, E, Happy, H, and Lemme, MC (2016). IEEE, 236.
52. Cho, C, Lee, SK, Noh, JW, Park, W, Lee, S, Lee, YG, Hwang, HJ, Kang, CG, Ham, MH, and Lee, BH (2015). Appl Phys Lett. 106, 213107.
53. Smith, JT, Franklin, AD, Farmer, DB, and Dimitrakopoulos, CD (2013). ACS Nano. 7, 3661.
54. Park, HY, Jung, WS, Kang, DH, Jeon, J, Yoo, G, Park, Y, Lee, J, Jang, YH, Lee, J, Park, S, Yu, HY, Shin, B, Lee, S, and Park, JH (2015). Adv Mater. 28, 864.

January 2018, 27 (1)
Full Text(PDF) Free

Social Network Service
Services


text:
# Factorize Factorization

We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by Hindley-Rosen result for confluence. Factorization – a simple form of standardization – is concerned with reduction strategies, i.e. how a result is computed. The technique is first developed abstractly. In particular, we isolate a simple sufficient condition (called linear swap) for lifting factorization from components to the compound system. We then closely analyze some common factorization schemas for the lambda-calculus, and show that the technique simplifies even more, reducing to the test of elementary local commutations. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno's non-deterministic lambda-calculus and – for call-by-value – Carraro and Guerrieri's shuffling calculus. For both calculi the literature contains factorization theorems. For each, we obtain a novel proof which is neat and strikingly short.

## Authors

• 17 publications
• 7 publications
• 14 publications
• ### Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)

In each variant of the lambda-calculus, factorization and normalization ...
01/20/2021 ∙ by Claudia Faggian, et al. ∙ 0

• ### Factorization and Normalization, Essentially

Lambda-calculi come with no fixed evaluation strategy. Different strateg...
08/29/2019 ∙ by Beniamino Accattoli, et al. ∙ 0

• ### Formalized Lambek Calculus in Higher Order Logic (HOL4)

In this project, a rather complete proof-theoretical formalization of La...
05/20/2017 ∙ by Chun Tian, et al. ∙ 0

• ### On Randomised Strategies in the λ-Calculus (Long Version)

In this work we introduce randomised reduction strategies, a notion alre...
05/10/2018 ∙ by Ugo Dal Lago, et al. ∙ 0

• ### A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle

An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is ...
04/28/2021 ∙ by Lawrence C. Paulson, et al. ∙ 0

• ### On reduction and normalization in the computational core

We study the reduction in a lambda-calculus derived from Moggi's computa...
04/20/2021 ∙ by Claudia Faggian, et al. ∙ 0

• ### The em-convex rewrite system

We introduce and study em (or "emergent"), a lambda calculus style rewri...
07/05/2018 ∙ by Marius Buliga, et al. ∙ 0

##### This week in AI

Get the week's most popular data science and artificial intelligence research sent straight to your inbox every Saturday.

## 1 Introduction

The -calculus is the model underling functional programming languages and, more generally, is the paradigm of higher-order computation. Through the years, more and more advanced features have enriched this paradigm, including control, non-determinism, states, probabilistic or quantum features. The well established way to proceed is to extend the -calculus with new operators. Every time, good operational properties, such as confluence, normalization, or termination, need to be proved. It is evident that the more complex and advanced is the calculus under study, the more the ability to modularize the analysis of its properties is crucial.

Techniques for modular proofs are available for termination and confluence, with a rich literature which examines under which conditions these properties lift from modules to the compound system—some representative papers are [50, 49, 51, 45, 34, 35, 36, 28, 7, 18, 16, 15, 5, 9], see Gramlich [20] for a survey. Termination and confluence concern the existence and the uniqueness of normal forms, which are the results of a computation. When the focus is on how to compute the result, that is, on identifying reduction strategies with good properties, then only few abstract techniques are currently available (we mention [19, 32, 33], [48](Ch.8), and [2])—this paper proposes a new one.

##### Factorization.

The most basic abstract property about how to compute is factorization, whose paradigmatic example is the head factorization theorem of the -calculus ([8], 11.4.6): every -reduction sequence can be re-organized/factorized so as to first reducing head redexes and then everything else—in symbols .

The study of factorization in -calculus goes back to Rosser [44]. Here, we adopt Melliès terminology [33]: factorization is sometimes referred to as semi-standardization (Mitschke in [37]), or postponement ([48]), and often simply called standardization—standardization is however a more sophisticated property (sketched below) of which factorization is a basic instance.

The content of factorization is captured well by Melliès [33]: it means that the essential part of a computation can always be separated from its junk. Let’s abstract the role of head reduction, by assuming that computations consists of steps which are in some sense essential to reach the result, and steps which are not. Factorization says that every rewrite sequence can be factorized in a sequence of essential steps, followed by inessential ones: implies .

Well known examples of essential reductions are head and leftmost-outermost reduction (see Barendregt [8]) for the -calculus, or left and weak reduction for the call-by-value -calculus (see Plotkin [40] and Paolini and Ronchi Della Rocca [43]).

Very much as confluence, factorization is a non-trivial property of -calculus; proofs require techniques such as finite developments [12, 48], labeling [31, 27], parallel reduction [47].

##### Uses of Factorization.

Factorization is commonly used as the building block in proving more sophisticated properties of the how-to-compute kind. It is often the main ingredient in proofs of normalization theorems [8, 47, 25, 52, 3], stating that a reduction strategy reaches a normal form whenever one exists. Leftmost normalization is a well known example.

Another property, standardization

, generalizes factorization: reduction sequences can be organized with respect to an order on redexes, not just with respect to the distinction essential/inessential. It is an early result that factorization can be used to prove standardization: iterated head factorizations provides what is probably the simplest way to prove Curry and Feis’ left-to-right standardization theorem, via Mitschke’s argument

[37].

Additionally, the independence of some computational tasks, such as garbage collection, can also be modeled as a factorization theorem. In calculi where -reduction is decomposed in smaller, micro steps, there is often a rule for garbage collection. The fact that garbage collection is an orthogonal task, managed by the system, can sometimes be expressed as factorization property: implies , where is made of all the evaluation rules but the garbage collecting one.

##### This Paper.

Here we present a method for proving factorization theorems for compound systems in a modular way. The approach can be seen as an analogous for factorization of the classical technique based on Hindley-Rosen lemma, which we discuss in the next paragraph. To use a similar technique also for factorization is natural, yet to our knowledge this has never been proposed before.

Crucially to make the method usable and useful, we craft a simple condition that—quite surprisingly—suffices to handle with ease a variety of interesting cases. In particular, we apply our method to two diverse extensions of the -calculus in the literature, which do not fit into easily manageable categories of rewriting systems. In both cases, we obtain a novel proof which is neat, simpler than the original, as well as strikingly short.

##### Confluence via Hindley-Rosen.

Let us consider confluence. The simplest possible modular technique to establish it is based on Hindley-Rosen lemma, which states that the union of two confluent reductions and is itself confluent if and satisfy a commutation property. See for example the classical proof of confluence of in [8] (Thm. 3.3.9 therein); Barendregt explicitly points out how the resulting proof is simpler than the original one by Curry and Feys.

While the result is basic—even elementary—Hindley-Rosen lemma provides a powerful tool to prove confluence of complex systems, as those obtained when extending the -calculus with advanced features. We mention for instance its use in the linear-algebraic -calculus [6], the probabilistic -calculus [17], the -calculus [46], the shuffling calculus [11], the -calculus extended with lists [42]

[10]. It is worth to spell-out the gain. Confluence is often a non-trivial property to establish—when higher-order is involved, the proof of confluence requires sophisticated techniques. The difficulty compounds when extending the -calculus with new constructs. Still, the problem is often originated by the -reduction itself, which encapsulates the higher-order features of the computation. By using Hindley-Rosen lemma, we rely on the fact that the -calculus is confluent, and do not need to prove that again. We use confluence of as a black box.

##### Modular Factorization, Abstractly.

In this paper, we present a similar approach to factorization. First, we study the question abstractly, with no assumptions on the structure of the object involved in the reduction. The starting point is an analog of Hindley-Rosen lemma for factorization: if and factorize separately and satisfy a property of commutation then the union also factorizes. Such a statement alone is of little use, because the commutation condition is in general non-trivial verifying – it may be as difficult as the general problem. However, we identify a simple and sufficient linear swap condition which, remarkably, is satisfied by several interesting examples, making it a rather powerful tool.

A key point here is that we assume the modules to be factorizing, therefore we can use their factorization—that may require a non-trivial proof via parallel reductions or finite developments—as a black box. Instead, to test the linear swap condition is combinatorial in nature, and local, in the sense that only single steps (rather than sequences of steps) need to be manipulated. This holds true even when the modules are not confluent, or non-terminating.

##### Modular Factorization, Concretely.

Next, we focus on oru target, which are extensions of the -calculus and discover a further striking gain: for common factorization schemas such as head or weak factorization, to verify the linear swap condition reduces to checking a single case, together with the fact that the new rule behaves well with respect to substitution.

We illustrate our method by providing several examples, chosen to stress the independence of the technique from other rewriting properties. In particular, we revisit two results from the literature. The first is head factorization for the non-deterministic -calculus by de’ Liguoro and Piperno [14], that extends the -calculus with a choice operator. It is a non confluent calculus, and it is representative of the class of -calculi extended with a commutative effect, such as probabilistic choice; indeed, most features and all issues are already present there, see [13] for a thorough discussion.

The second result is factorization for the shuffling calculus—a refinement of the call-by-value -calculus due to Carraro and Guerrieri [11], whose left factorization is proved by Guerrieri, Paolini, and Ronchi della Rocca in [21]. In this case the -calculus is extended with extra rules, but they are not associated to a new operator, very much like -reduction.

In both cases, we obtain a neat, and conceptually clear proof, which is remarkably short (versus several pages for the originals).

Summing up, we provide a simple method, based on testing a sufficient condition—the (root) linear swap—for testing common factorization schemes of enriched -calculi. Our technique is combinatorial and local. This fact makes it easy to use, and a convenient tool for the analysis of complex calculi. Additionally, it makes the technique suitable for automated proofs or to certify proofs of factorization, in the same spirit propounded by Hirokawa, Middeldorp, and Moser in [25].

#### Related work

To our knowledge, the only result in the literature about modular techniques for factorization is Accattoli’s technique for calculi with explicit substitutions [2], which relies on termination hypotheses. Our linear swap condition (page Linear Swap) is technically the same as his diagonal-swap condition. One of the observations at the inception of this work is exactly that termination in [2] is used only to establish factorization of each single module, but not when combining them. Here we assume modules to be factorizing, therefore avoiding termination requirements, and obtaining a more widely applicable technique.

A divide-and-conquer approach is well-studied for termination. The key point is finding conditions which guarantee that the union of terminating relations is terminating. Several have been studied [7, 18]; the weakest such condition, namely , is introduced by Doornbos and von Karger [16], and then studied by Dershowitz [15], under the name of lazy commutation, and by van Oostrom and Zantema [53]. Interestingly, lazy commutation has a similar flavor as the linear swap condition.

Finally, we mention a somehow orthogonal approach to study extensions of a rewriting system, which is to identify syntactical classes of term rewriting systems, which satisfy a property. While confluence is again the most studied property (e.g., [48], Ch 10.4), factorization and standardization are also investigated. Notably, if all rules which compose a system are left-normal, the system admits left-to-right standardization ([48], Ch. 8.5.7).

## 2 Preliminaries

In this section we start by recalling some standard definitions and notations in rewriting theory (see e.g. [48]); we provide an overview of confluence, commutation, and factorization.

##### Basics.

An abstract rewriting system (ARS) (see [48], Ch.2) is a pair consisting of a set and a binary relation on whose pairs are written and called steps. We denote (resp. ) the transitive-reflexive (resp. reflexive) closure of . We write to denote the ARS where . We use freely the fact that the transitive-reflexive closure of a relation is a closure operator, i.e. satisfies

 →⊆→∗,(→∗)∗ = →∗,→1 ⊆ →2 % implies →∗1 ⊆ →∗2. (Closure)

The following property is an immediate consequence:

 (→1∪→2)∗ = (→∗1∪→∗2)∗. (TR)

We shall also use the following easy property.

implies .

##### Commutation.

Two relations and on commute if and imply that there exists such that and . Confluence and factorization, discussed in the next subsections, are both forms of commutations.

##### Local vs Global Properties.

In rewriting theory it is common to distinguish between local and global properties. A property of term is local if it is quantified over only one-step reductions from ; it is global if it is quantified over all rewrite sequences from . Local properties are usually easy to test. Global properties instead are more delicate. Note however that the difference between global and local is also a matter of perspective (and relation choice). A paradigmatic example is confluence (global) vs. diamond (local), as we recall below.

### 2.1 Confluence

##### The heart of Confluence is a Diamond.

A relation on is

• Confluent if and implies that there exists such that and ;

• Diamond: if , implies that there exists such that and ;

Observe that confluence can be formulated as a diamond property:

is confluent if and only if is diamond

It is well known that the diamond property implies confluence. The diamond property, however, can rarely be used directly, because most relations of interest–e.g. -reduction of -calculus–do not satisfy it. Nonetheless, the diamond is at the heart of to two fundamental techniques for proving confluence: Hindley-Rosen Lemma and the Parallel Reduction method of Tait and Martin-Löf. Both techniques rely the following easy property, which introduces a mediating relation . Observe that the diamond does not hold for , but for the mediating relation.

[Characterization] is confluent if and only if there exists a relation such that

1. Same closure: ,

2. Diamond: is diamond.

##### Hindley-Rosen.

A classic result to modularize the proof of confluence is Hindley-Rosen lemma. Confluence of two relations and does not in general imply confluence of , however it does if and commute.

###### Lemma (Hindley-Rosen).

Let and be relations on the set . If and are confluent and commute with each other, then is confluent.

The proof of Hindley-Rosen looks at confluence and commutation as expressing the diamond property of . The diamond property lends itself, indeed, to easy modularization. We shall follow a similar path to modularize factorization.

### 2.2 Factorization

We now recall basic facts on the rewriting property at the center of this paper, factorization. Like for confluence, we shall focus on the local vs global perspective.

###### Definition (Factorization).

Let be an ARS. The relation satisfies -factorization, written , if the following holds

.

The following equivalent formulations of -factorization are all well known111Factorization can also be formulated in terms of commutation, and viceversa, as postpones after if and only if and commute.. The following are equivalent (for any two relations )

1. Semi-local postponement 1: .

2. Semi-local postponement 2: .

3. Postponement: .

4. Factorization: .

##### The heart of Factorization is Local Postponement.

Hindley first noted that a local property implies factorization [24].

###### Definition (Local Postponement).

We say that locally postpones after if

[Hindley [24]] Given , implies .

We observe that a property similar to Lemma 2.1 holds for factorization.

[Characterization] Let be an ARS. Factorization holds if and only if there exists such that:

1. Same closure: .

2. Local Postponement: holds.

###### Proof.

If. By Lemma 2.2, implies . By and property (TR) (page TR), holds. Only if. Observe that instantiating , condition (a) is trivially satisfied and (b) holds because implies case (2) of Lemma 1. ∎

The content of Lemma 2.2 may be familiar. In the -calculus, the role of a mediating relation is typically played by parallel reduction, both for confluence and for factorization. The core of Takahashi’s method for factorization [47] is to introduce a mediating relation , called internal parallel reduction, which verifies the hypotheses of Lemma 2.2.

Similarly to the diamond property for confluence, local postponement can rarely be used directly, because interesting reductions do not often satisfy it. However, we claim that it is the core of factorization; indeed, local postponement is at the heart of Takahashi’s Parallel Reduction method to prove Factorization [47] , and it will be the cornerstone of our approach to modularity.

In the next section, we first deal modularly with local postponement, and then lift the result to factorization by using a mediating relation.

##### Factorization vs. Confluence.

Note that factorization and confluence are independent properties. In Sect. 5 we shall apply our modular factorization technique to a non-confluent calculus. Conversely, is a confluent reduction, which does not admit neither head nor leftmost factorization—interestingly and do verify head and leftmost factorization separately.

## 3 Modularizing Factorization

A natural way of modularizing factorization is to find conditions to make local postponement modular. We capture them in the following definition.

[LOcal Postponement Pair (LOPP)] A pair and of ARS form a LOPP if the following conditions hold, where

Local Postponement of : implies
Local Postponement of : implies ,
Swap of after : implies ,
Swap of after : implies .

Note in the right-hand side of the swap conditions. The four conditions essentially say that postpones after both and , and similarly for .

The four conditions above can be unified in following compact condition:

implies for all .

The condition, and the result below, easily extends to the union of any number of relations

[] If and form a LOPP, then their union satisfies local postponement , where and .

###### Proof.

It is immediate that implies , because the 4 combinations of () exactly correspond to the 4 conditions. ∎

We now lift the result from local postponement to the global property, factorization.

[Modular factorization, mediated] Let and be two ARS. Their union satisfies factorization , where and , if there exist such that

1. Same closures: and .

2. LOPP: and form a LOPP.

###### Proof.

We use Lemma 2.2, where we instantiate . Note that

1. , by assumption (A.) and property TR (page TR).

2. holds, by assumption (B.) and Lemma 3.

### 3.1 Union of Factorizing Relations

We formulated Theorem 3 in full generality; this allows for to be any mediating relation we need, for example a parallel reduction. We now focus on a specific choice and provide a simple local diagram implying the swap conditions.

Since we want to study under which conditions the union of factorizing relations satisfies factorization, the most natural choice is to take directly and . Assuming that and factorize separately, by Theorem 3, we have that the following are sufficient conditions to guarantee that factorizes (note that local postponement of and is given by Lemma 2.2):

Swap of after :      and    Swap of after :    .

These conditions are rather strong, because global, hence difficult to verify. Perhaps surprisingly, the following easy-to-check condition, which is local and linear in , suffices, and holds in a large variety of cases. Note in the right-hand side. We say that linearly swaps with if

 (Linear Swap)

[Linear Swap] and (Swap of after ).

###### Proof.

implies , by Property 2. By factorization of , we obtain . ∎

By Theorem 3 and Lemma 3.1, we obtain that the union of two factorizing relations , is factorizing if two elementary conditions are verified.

###### Corollary (Modular Factorization, linearly).

Let and be -factorizing relations, such that

and   .

Then their union satisfies where , and .

##### Linear Postponement.

The idea behind the linear swap condition also applies to local postponement. The following will simplify the proof of factorization in several of our case studies.

[Linear postponement] Let

1. (.

2. (.

## 4 Enriched λ-Calculi and Head Factorization

We now consider factorization theorems for extensions of the -calculus. We start with head factorization, which is by far the most important and common factorization scheme in -calculus.

We show that our method lends a simple, neat test to prove head factorization of compound systems which enrich the -calculus with extra rules. In particular, the linear swap conditions reduce to an even simpler version, where the extra relation is tested only at its root rule. This property of head factorization holds for all rules, independently from their specific form.

### 4.1 The (applied) λ-Calculus

Since in the next sections we shall extend the -calculus with new operators, such as a non-deterministic choice or a fix-point , we include in the syntax of the -calculus a set of constants, meant to represent such operators. So, for instance, in Sect. 5 we shall see as a constant. This way one can see factorization results with respect to -reduction as holding also in the -calculus with extended syntax; this is absolutely harmless.

Note that despite the fact that the classic Barendregt’s book [8] defines the -calculus without constants, other classic references such as Hindley and Seldin’s book [23] or Plotkin [40] do endow it with constants—therefore, there is nothing exotic in the approach adopted here.

##### The syntax.

-terms and contexts are generated by

where ranges over a countable set of variables, over a disjoint (finite, infinite or empty) set of constants. Variables and constants are atoms, a term of shape is an application, and an abstraction. If the constants are , the set of terms is sometimes indicated as . Following [23] (page 3), when the set of constants is empty, the calculus is called pure, otherwise applied.

The plugging of a term into a context is the operation replacing the only occurrence of in with , potentially capturing free variables of .

A reduction step is defined as the contextual closure of a root relation on ,which is called a rule. Explicitly, given a rule , then holds if and , for some context . The term is called a -redex. Given two (or more) rules on , the relation is , which can equivalently be defined as the contextual closure of .

The -calculus is , the set of terms together with -reduction , defined as the contextual closure of the -rule: where denotes capture-avoiding substitution. We silently work modulo -equivalence.

##### Properties of Contextual Closure.

Here we collect a few basic properties about contextual closures and substitution, preparing the ground for the root swap condition studied next.

A relation on terms is substitutive if implies . An obvious induction on the shape of shows the following ([8] pag. 54).

###### Property (Substitutive).

Let be the contextual closure of .

1. If is substitutive then is substitutive:   implies .

2. If then .

We also point out a basic but key property which holds for all internal reductions we study.

###### Property (Shape Preservation).

Assume with . is an application (resp. an abstraction) if and only if is.

The consequences of Property 4.1 are spelled-out in Property A.1 and A.2 in the Appendix.

Head contexts are defined as follows:

where and . Note that if and only if . A non-head context is a context which is not head.

A head step (resp. non-head step ) is defined as the closure under head contexts (resp. non-head contexts) of rule . Obviously, .

Since the empty context is a head context, observe two basic but useful facts:
(i.) , and (ii.) Property 4.1 always applies to non-head steps.

Head factorization is of great importance for the -calculus. In this case, our method simplifies even more, in two ways. First, each linear swap condition can be tested by considering for the head step only the root relation i.e., only the closure of under empty context, which is a head step by definition. This is expressed in the following lemma, where we include also a variation on the same property, that shall be useful later on. [Root Linear Swaps]Let be root relations on . If then . Moreover, the same is true if one replaces with . Note that Lemma 4.2 gives either a proof that the swap conditions hold, or a counter-example—at the end of the section we give an example of this use.

Second, in practice, we study systems of the form , i.e. the -calculus is enriched with a new relation. In such a case, linearly swaps after as soon as is substitutive. [Swap with ] If is substitutive, holds. The easy proof of these two lemmas is in Appendix A.1.1.

Summing up, since head factorization for is known, we obtain the following compact test for head factorization for enriched -calculi.

###### Proposition (A Test for Head Factorization).

Let be -reduction and be the contextual closure of . Their union satisfies head factorization if:

1. Head factorization of : .

2. Substitutivity: is substitutive.

3. Root linear swap: .

Note that none of the properties concerns alone, whose head factorization is used as a black box, as we already know that head factorization of holds.

In Sect. 5 we shall use our test (Proposition 4.2) to prove head factorization for the non-deterministic -calculus. The full proof is only a few lines long.

##### An Example of Counter-Example, βη.

Let us show how the test of Proposition 4.2 can provide a counter-example to head factorization when it fails. Let’s instatiate with , that is, the contextual closure of rule if . Now, consider the root linear swap:

,     where .

Note that has no step, and so the two steps cannot be swapped. In fact, the reduction sequence above is easily seen to be a counter-example to both head and leftmost factorization for : if we start with the head redex (which is also the leftmost-outermost redex) . From , there is no way to reach . We recall that somewhat surprisingly, still satisfies leftmost normalization. The proof is non-trivial, see [27, 47, 52, 26].

## 5 The Non-Deterministic λ-Calculus Λ⊕

De’ Liguoro and Piperno’s non-deterministic -calculus is defined in [14] by extending the -calculus with a new operator whose rule models non-deterministic choice. Intuitively, non-deterministically rewrites to either or . Notably, is not confluent, hence it is a good example of the fact that confluence and factorization are independent properties. The work by de’ Liguoro and Piperno has been ground-breaking; indeed many key features and all issues appearing in the more complex setting of the -calculus with probabilistic choice are already present—see Dal Lago and Zorzi [13] for a thorough discussion.

We briefly present the syntax of and its features, and then use our technique to give a novel and neat proof of de’ Liguoro and Piperno’s head factorization result (Cor. 2.10 in [14]).

##### Syntax.

We slightly depart from the presentation in [14], as we consider as a constant, and write rather than , working as usual for -calculus with constants (see e.g., Hindley and Seldin [23], or Barendregt [8], Sec. 15.3). Terms and contexts are generated by:

 \footnotesizet,p,q,r::=x∣⊕∣λx.t∣tp(terms Λ⊕)C::=⟨ ⟩∣tC∣Ct∣λx.C(contexts)

As before, denotes -reduction, while the rewrite step is the contextual closure of the following non-deterministic rule:

.

Note that there is no loss with respect to the syntax in [14], where always comes with two arguments, because such a constraint defines a sub-system which is closed under reduction.

##### Subtleties.

The calculus is highly non trivial. Of course, is not confluent. Moreover, the following examples from [14] show that to permute -steps and -steps is delicate.

• creates -redexes: for instance, , hence the -step cannot be postponed after .

• Choice Duplication. Postponing after is also problematic, because -steps may multiply choices, introducing new results: flipping a coin and duplicating the result is not equivalent to duplicating the coin and then flipping twice. For instance, let and consider  vs   (we cannot reach !).

These examples are significant as the same issues impact any calculus with choice effects.

The head (resp. non-head) rewrite steps and (resp. and ) are defined as the closure by head (resp. non-head) contexts of rules and , respectively222Non-head steps are called internal () in [14].. We also set and .

De’ Liguoro and Piperno prove that despite the failure of confluence, satisfies head factorization. They prove this result via standardization, following Klop’s technique [27].

###### Theorem (Head Factorization, Cor. 2.10 in [14]).

holds in the non-deterministic -calculus .

##### A New Proof, Modularly.

We give a novel, strikingly simple proof of , simply by proving that and satisfy the hypotheses of the test for head factorization (Proposition 4.2). All the ingredients we need are given by the following easy lemma. [Roots]

1. implies .

2. implies .

###### Proof.
1. Let , and assume (the case is similar). Assume . By Property 4.1 (as spelled-out in Property A.1), has shape , with . Therefore, either or , from which .

2. The proof is the same as above, just put in place of .∎

We have because we have:

2. Substitutivity:   is substitutive.

3. Root linear swap:   .

###### Proof.

We prove the hypotheses of Proposition 4.2:

1. Because linearly postpones after . Indeed from Lemma 5.2, we use Lemma 4.2 with , and obtain that . We conclude by Lemma 3.1.2.

2. By definition of substitution .

3. This is exactly Lemma 5.1.∎

##### Standardization and Leftmost Normalization.

From head factorization, standardization and leftmost normalization easily follow, via Mitschke argument [37, 8], see Appendix A.1.2.

## 6 Call-by-Value λ-calculus

Plotkin’s call-by-value (CbV) -calculus [40] is the restriction of the -calculus where


text:
Video Lectures

Results on abundance of global surfaces of section

Umberto Hryniewicz

Modularity and Heights of CM cycles on Kuga-Sato varieties

Congling Qiu

We study CM cycles on Kuga-Sato varieties over X(N) via theta lifting and relative trace formula. Our first result is the modularity of CM cycles, in the sense that the Hecke modules they generate are semisimple whose irreducible components are...

Recent progress in query complexity I & II Part 2

The query model is one of the most basic computational models.  In contrast to the Turing machine model, fundamental questions regarding the power of randomness and quantum computing are relatively well-understood.  For example, it is well-known...

Tropical Lagrangian sections and Looijenga pairs

Andrew Hanlon

We will discuss the first steps in an approach to proving homological mirror symmetry for Looijenga pairs through tropical Lagrangian sections. Namely, we will see how to construct these Lagrangian sections from tropical data corresponding to line...

What is the h-principle?

The honest answer to the question is that I actually do not know. I will therefore rather talk about several famous examples that are widely called "h-principle results" and try to explain some of the ideas behind the ones I am most familiar with.

...

Alexandros Hollender

We consider the problem of computing a Gradient Descent solution of a continuously differentiable function f on a bounded convex domain, i.e., finding a "point where Gradient Descent terminates". Equivalently, this corresponds to computing a so...

Cabling of knots in overtwisted contact manifolds

Rima Chatterjee

Knots associated to overtwisted manifolds are less explored. There are two types of knots in an overtwisted manifold – loose and non-loose. Non-loose knots are knots with tight complements whereas loose knots have overtwisted complements. While we...

Cylindrical contact homology of links of simple singularities

Leo Digiosia

In this talk we consider the links of simple singularities, which are contactomoprhic to S3/G for finite subgroups G of SU(2,C). We explain how to compute the cylindrical contact homology of S3/G by means of perturbing the canonical contact form by...

Convergence and Riemannian bounds on Lagrangian submanifolds

Jean-Philippe Chassé

Recent years have seen the appearance of a plethora of possible metrics on spaces of Lagrangian submanifolds. Indeed, on top of the better-known Lagrangian Hofer metric and spectral norm, Biran, Cornea, and Shelukhin have constructed families of so...


text:
# Linear Equations in One Variable

Linear equation in one variable is the equation with standard form color(purple)(mx+b=0).

m and b are some numbers and x is a variable.

Examples of linear equations are:

• 4x+2=0
• -2a-3=0
• 3/2 m-5/3=0

Using equivalence of equations, we can convert some other equations into the standard form:

• 2x=5 is equivalent to 2x-5=0 (subtract 5 from both sides of equation)
• 3/2x=5-2/3x becomes 13/6x-5=0 (move everything to the left and combine like terms)
• sqrt(2)x-5=x+2 becomes (sqrt(2)-1)x-7=0 (move everything to the left and combine like terms)
• 1/y=2 becomes -2y+1=0 (multiply both sides by y and move everything to the left)

Equation is linear, when it is written in standard form and variable is raised to the first power only.

Following are NOT linear equations:

• 2x^2+3=0 (variable raised to the second power)
• 2y-3=3/2y^2 (there is variable, raised to the second power)
• 1/y+y=2 (if we multiply both sides by y, then we will get 1+y^2=2y, which is not quadratic)

Exercise 1. Determine, whether 2x=-5 is linear and write it in standard form if it is.

Answer: yes; 2x+5=0.

Exercise 2. Determine, whether 1=2/3 a is linear and write it in standard form if it is.

Answer: yes; 2/3a-1=0.

Exercise 3. Determine, whether x^2=7 is linear and write it in standard form if it is.

Exercise 4. Determine, whether 1/x+5=x is linear and write it in standard form if it is.
Answer: no. Multiplying both sides by x gives 1+5x=x^2.
Exercise 5. Determine, whether 3/x=7/3 is linear and write it in standard form.
Answer: yes; 7/3x-3=0.