Specular reflections and refractive distortions are complex image properties of solid transparent objects, but despite this complexity, we readily perceive the 3D shapes of these objects. We have found in past work that relevant sources of scene complexity have differential effects on 3D shape perception, with specular reflections increasing perceived thickness, and refractive distortions decreasing perceived thickness. In an object with both elements, such as glass, the two optical properties may complement each other to support reliable perception of 3D shape. (...) We investigated the relative dominance of specular reflection and refractive distortions in the perception of shape. Surprisingly, the ratio of specular reflection to refractive component was almost equal to that of ordinary glass and ice, which promote correct percepts of 3D shape. The results were also explained by the variance in local RMS contrast in stimulus images but may depend on overall luminance and contrast of the surrounding light field. (shrink)

The discovery of the signal peptides that direct proteins to localize at the nucleolus is described here. The nucleolar targeting signal termed the NOS consists of clustered basic amino acids organized such that a portion also functions as the nuclear transporting signal. Although a NOS has been identified within the regulatory genes of human retroviruses, HTLV‐I and HIV‐I, signals of similar function in cellular proteins – such as heat shock proteins – may be induced through the configurational change of protein (...) structure by heat or stress. (shrink)

The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...) affirmative. The first to prove this was E. P. Martin by a semantical method. In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λ x.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style. (shrink)

A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a -calculus with a new constant P (()). It is shown that all terms with the same type are equivalent with respect to -reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for P-reduction. Weak normalization is shown for P-reduction with another (...) reduction rule which simplifies of (( ) ) into an atomic type. (shrink)

A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment to (...) another -term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW--terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general -terms and BCIW--terms. (shrink)

The syntactic structure of the system of pure implicational relevant logic P - W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linear λ-terms, and a translation of such λ-terms M to BB'I-combinators (...) M + is introduced. It is shown that a formula α is provable in P - W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P - W. Errol Martin (1982) proved that no formula with form α → α is provable in P - W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λ x.x if the translated BB'I-combinator M + contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λ x.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P - W is determined. (shrink)

The syntactic structure of the system of pure implicational relevant logic $P - W$ is investigated. This system is defined by the axioms $B = (b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c, B' = (a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow a \rightarrow c, I = a \rightarrow a$, and the rules of substitution and modus ponens. A class of $\lambda$-terms, the closed hereditary right-maximal linear $\lambda$-terms, and a translation of such $\lambda$-terms $M$ to $BB'I$-combinators (...) $M^+$ is introduced. It is shown that a formula $\alpha$ is provable in $P - W$ if and only if $\alpha$ is a type of some $\lambda$-term in this class. Hence these $\lambda$-terms represent proof figures in the Natural Deduction version of $P - W$. Errol Martin (1982) proved that no formula with form $\alpha \rightarrow \alpha$ is provable in $P - W$ without using the axiom $I$. We show that a $\beta$-normal form $\lambda$-term $M$ in the class is $\eta$ reducible to $\lambda x.x$ if the translated $BB'I$-combinator $M^+$ contains $I$. Using this theorem and Martin's result, we prove that a $\lambda$-term in the class is $\beta\eta$-reducible to $\lambda x.x$ if the $\lambda$-term has a type $\alpha \rightarrow \alpha$. Hence the structure of proofs of $\alpha \rightarrow \alpha$ in $P - W$ is determined. (shrink)

The mental fatigue elicited by working and studying consumed mental resources, thereby eliciting a declined performance and an increased mental stress. The long-term continuous work and study, which is typical for modern workers and students, can increase mental fatigue and health risks. Previous studies reported that the natural environment has a restorative of mental resources and reducing stress. However, it is difficult for urban workers and students to take sufficient breaks in real natural environment. We conducted an experiment to examine (...) whether brief and indirect exposure to the natural environment elicits a restorative of attention and reducing stress. Twenty-five undergraduate and graduate students from the university of modern city participated in the experiment. The experiment involved measuring the changes in the task performance of the participants and the subjective mental workload, while the attention restoration was indexed from physiological response over time. The participants had two types of resting periods in the middle of the task, i.e., by looking at a blank display or by watching a nature video having scenes of, e.g., a forest, small waterfall, and rustling leaves. The results indicate that the natural environment indirectly depicted through the nature videos does not affect the task performance and the subjective mental workload but decreases the SCL. The results of the physiological response suggest that having rest periods depicting the natural environment, even if indirectly and briefly, can restore the directed attention for the task. This experiment revealed a useful method of resting for urban workers and students to restore their attention to a task. (shrink)